Theorem uzindOLD 6164

Description: Induction on the upper integers that start at an integer B. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction hypothesis.

Warning: The HTML proof page is 3/4 megabyte in size. An attempt to shorten it is on my to-do list.

Hypotheses

Ref	Expression
uzindOLD.1	|- (x = B -> (ph <-> ps))
uzindOLD.2	|- (x = y -> (ph <-> ch))
uzindOLD.3	|- (x = (y + 1) -> (ph <-> th))
uzindOLD.4	|- (x = A -> (ph <-> ta))
uzindOLD.5	|- ps
uzindOLD.6	|- (((y e. ZZ /\ B e. ZZ) /\ B <_ y) -> (ch -> th))

Assertion

Ref	Expression
uzindOLD	|- (((A e. ZZ /\ B e. ZZ) /\ B <_ A) -> ta)

Distinct variable groups:   x,A   ps,x   ch,x   th,x   ta,x   ph,y   x,y,B

Proof of Theorem uzindOLD

Step	Hyp	Ref	Expression
1		subge0t 5655	. . . . 5 |- ((A e. RR /\ B e. RR) -> (0 <_ (A - B) <-> B <_ A))
2		resubclt 5418	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> (A - B) e. RR)
3		0re 5420	. . . . . . . 8 |- 0 e. RR
4		1re 5415	. . . . . . . 8 |- 1 e. RR
5		leadd1t 5607	. . . . . . . 8 |- ((0 e. RR /\ (A - B) e. RR /\ 1 e. RR) -> (0 <_ (A - B) <-> (0 + 1) <_ ((A - B) + 1)))
6	3, 4, 5	mp3an13 905	. . . . . . 7 |- ((A - B) e. RR -> (0 <_ (A - B) <-> (0 + 1) <_ ((A - B) + 1)))
7	2, 6	syl 10	. . . . . 6 |- ((A e. RR /\ B e. RR) -> (0 <_ (A - B) <-> (0 + 1) <_ ((A - B) + 1)))
8		ax1cn 5249	. . . . . . . 8 |- 1 e. CC
9	8	addid2 5311	. . . . . . 7 |- (0 + 1) = 1
10	9	breq1i 2621	. . . . . 6 |- ((0 + 1) <_ ((A - B) + 1) <-> 1 <_ ((A - B) + 1))
11	7, 10	syl6bb 535	. . . . 5 |- ((A e. RR /\ B e. RR) -> (0 <_ (A - B) <-> 1 <_ ((A - B) + 1)))
12	1, 11	bitr3d 529	. . . 4 |- ((A e. RR /\ B e. RR) -> (B <_ A <-> 1 <_ ((A - B) + 1)))
13		zret 6094	. . . 4 |- (A e. ZZ -> A e. RR)
14		zret 6094	. . . 4 |- (B e. ZZ -> B e. RR)
15	12, 13, 14	syl2an 454	. . 3 |- ((A e. ZZ /\ B e. ZZ) -> (B <_ A <-> 1 <_ ((A - B) + 1)))
16		zsubclt 6123	. . . . 5 |- ((A e. ZZ /\ B e. ZZ) -> (A - B) e. ZZ)
17	16	peano2zd 6122	. . . 4 |- ((A e. ZZ /\ B e. ZZ) -> ((A - B) + 1) e. ZZ)
18		elnnz1 6110	. . . . . . . 8 |- (((A - B) + 1) e. NN <-> (((A - B) + 1) e. ZZ /\ 1 <_ ((A - B) + 1)))
19		eleq1 1531	. . . . . . . . . 10 |- (z = 1 -> (z e. ZZ <-> 1 e. ZZ))
20		oprex 3974	. . . . . . . . . . . . . . 15 |- ((z - 1) + B) e. V
21	20	isseti 1811	. . . . . . . . . . . . . 14 |- E.x x = ((z - 1) + B)
22		ax-17 969	. . . . . . . . . . . . . . . 16 |- ((z = 1 /\ B e. ZZ) -> A.x(z = 1 /\ B e. ZZ))
23	20	hbsbc1v 1946	. . . . . . . . . . . . . . . . 17 |- ([((z - 1) + B) / x]ph -> A.x[((z - 1) + B) / x]ph)
24		ax-17 969	. . . . . . . . . . . . . . . . 17 |- (ps -> A.xps)
25	23, 24	hbbi 1008	. . . . . . . . . . . . . . . 16 |- (([((z - 1) + B) / x]ph <-> ps) -> A.x([((z - 1) + B) / x]ph <-> ps))
26	22, 25	hbim 1005	. . . . . . . . . . . . . . 15 |- (((z = 1 /\ B e. ZZ) -> ([((z - 1) + B) / x]ph <-> ps)) -> A.x((z = 1 /\ B e. ZZ) -> ([((z - 1) + B) / x]ph <-> ps)))
27		sbceq1a 1940	. . . . . . . . . . . . . . . . . 18 |- (x = ((z - 1) + B) -> (ph <-> [((z - 1) + B) / x]ph))
28	27	adantr 389	. . . . . . . . . . . . . . . . 17 |- ((x = ((z - 1) + B) /\ (z = 1 /\ B e. ZZ)) -> (ph <-> [((z - 1) + B) / x]ph))
29		eqtrt 1489	. . . . . . . . . . . . . . . . . . 19 |- ((x = ((z - 1) + B) /\ ((z - 1) + B) = B) -> x = B)
30		opreq1 3959	. . . . . . . . . . . . . . . . . . . . 21 |- (z = 1 -> (z - 1) = (1 - 1))
31	30	opreq1d 3966	. . . . . . . . . . . . . . . . . . . 20 |- (z = 1 -> ((z - 1) + B) = ((1 - 1) + B))
32		zcnt 6095	. . . . . . . . . . . . . . . . . . . . . 22 |- (B e. ZZ -> B e. CC)
33		addid2t 5309	. . . . . . . . . . . . . . . . . . . . . 22 |- (B e. CC -> (0 + B) = B)
34	32, 33	syl 10	. . . . . . . . . . . . . . . . . . . . 21 |- (B e. ZZ -> (0 + B) = B)
35	8	subid 5371	. . . . . . . . . . . . . . . . . . . . . 22 |- (1 - 1) = 0
36	35	opreq1i 3962	. . . . . . . . . . . . . . . . . . . . 21 |- ((1 - 1) + B) = (0 + B)
37	34, 36	syl5eq 1516	. . . . . . . . . . . . . . . . . . . 20 |- (B e. ZZ -> ((1 - 1) + B) = B)
38	31, 37	sylan9eq 1524	. . . . . . . . . . . . . . . . . . 19 |- ((z = 1 /\ B e. ZZ) -> ((z - 1) + B) = B)
39	29, 38	sylan2 451	. . . . . . . . . . . . . . . . . 18 |- ((x = ((z - 1) + B) /\ (z = 1 /\ B e. ZZ)) -> x = B)
40		uzindOLD.1	. . . . . . . . . . . . . . . . . 18 |- (x = B -> (ph <-> ps))
41	39, 40	syl 10	. . . . . . . . . . . . . . . . 17 |- ((x = ((z - 1) + B) /\ (z = 1 /\ B e. ZZ)) -> (ph <-> ps))
42	28, 41	bitr3d 529	. . . . . . . . . . . . . . . 16 |- ((x = ((z - 1) + B) /\ (z = 1 /\ B e. ZZ)) -> ([((z - 1) + B) / x]ph <-> ps))
43	42	ex 373	. . . . . . . . . . . . . . 15 |- (x = ((z - 1) + B) -> ((z = 1 /\ B e. ZZ) -> ([((z - 1) + B) / x]ph <-> ps)))
44	26, 43	19.23ai 1062	. . . . . . . . . . . . . 14 |- (E.x x = ((z - 1) + B) -> ((z = 1 /\ B e. ZZ) -> ([((z - 1) + B) / x]ph <-> ps)))
45	21, 44	ax-mp 7	. . . . . . . . . . . . 13 |- ((z = 1 /\ B e. ZZ) -> ([((z - 1) + B) / x]ph <-> ps))
46	45	ex 373	. . . . . . . . . . . 12 |- (z = 1 -> (B e. ZZ -> ([((z - 1) + B) / x]ph <-> ps)))
47	46	adantld 390	. . . . . . . . . . 11 |- (z = 1 -> ((A e. ZZ /\ B e. ZZ) -> ([((z - 1) + B) / x]ph <-> ps)))
48	47	pm5.74d 584	. . . . . . . . . 10 |- (z = 1 -> (((A e. ZZ /\ B e. ZZ) -> [((z - 1) + B) / x]ph) <-> ((A e. ZZ /\ B e. ZZ) -> ps)))
49	19, 48	imbi12d 625	. . . . . . . . 9 |- (z = 1 -> ((z e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> [((z - 1) + B) / x]ph)) <-> (1 e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> ps))))
50		eleq1 1531	. . . . . . . . . 10 |- (z = w -> (z e. ZZ <-> w e. ZZ))
51		oprex 3974	. . . . . . . . . . . . 13 |- ((w - 1) + B) e. V
52	51	isseti 1811	. . . . . . . . . . . 12 |- E.y y = ((w - 1) + B)
53		eeanv 1321	. . . . . . . . . . . . 13 |- (E.xE.y(x = ((z - 1) + B) /\ y = ((w - 1) + B)) <-> (E.x x = ((z - 1) + B) /\ E.y y = ((w - 1) + B)))
54		ax-17 969	. . . . . . . . . . . . . . 15 |- (z = w -> A.x z = w)
55		ax-17 969	. . . . . . . . . . . . . . . 16 |- ([((w - 1) + B) / y]ch -> A.x[((w - 1) + B) / y]ch)
56	23, 55	hbbi 1008	. . . . . . . . . . . . . . 15 |- (([((z - 1) + B) / x]ph <-> [((w - 1) + B) / y]ch) -> A.x([((z - 1) + B) / x]ph <-> [((w - 1) + B) / y]ch))
57	54, 56	hbim 1005	. . . . . . . . . . . . . 14 |- ((z = w -> ([((z - 1) + B) / x]ph <-> [((w - 1) + B) / y]ch)) -> A.x(z = w -> ([((z - 1) + B) / x]ph <-> [((w - 1) + B) / y]ch)))
58		ax-17 969	. . . . . . . . . . . . . . . 16 |- (z = w -> A.y z = w)
59		ax-17 969	. . . . . . . . . . . . . . . . 17 |- ([((z - 1) + B) / x]ph -> A.y[((z - 1) + B) / x]ph)
60	51	hbsbc1v 1946	. . . . . . . . . . . . . . . . 17 |- ([((w - 1) + B) / y]ch -> A.y[((w - 1) + B) / y]ch)
61	59, 60	hbbi 1008	. . . . . . . . . . . . . . . 16 |- (([((z - 1) + B) / x]ph <-> [((w - 1) + B) / y]ch) -> A.y([((z - 1) + B) / x]ph <-> [((w - 1) + B) / y]ch))
62	58, 61	hbim 1005	. . . . . . . . . . . . . . 15 |- ((z = w -> ([((z - 1) + B) / x]ph <-> [((w - 1) + B) / y]ch)) -> A.y(z = w -> ([((z - 1) + B) / x]ph <-> [((w - 1) + B) / y]ch)))
63		eqeq12 1484	. . . . . . . . . . . . . . . . . 18 |- ((x = ((z - 1) + B) /\ y = (