Theorem uzindOLD 6379

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		subge0 5828	. . . . 5 |- ((A e. RR /\ B e. RR) -> (0 <_ (A - B) <-> B <_ A))
2		resubcl 5592	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> (A - B) e. RR)
3		0re 5594	. . . . . . . 8 |- 0 e. RR
4		1re 5589	. . . . . . . 8 |- 1 e. RR
5		leadd1 5779	. . . . . . . 8 |- ((0 e. RR /\ (A - B) e. RR /\ 1 e. RR) -> (0 <_ (A - B) <-> (0 + 1) <_ ((A - B) + 1)))
6	3, 4, 5	mp3an13 913	. . . . . . 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 5423	. . . . . . . 8 |- 1 e. CC
9	8	addid2i 5485	. . . . . . 7 |- (0 + 1) = 1
10	9	breq1i 2699	. . . . . 6 |- ((0 + 1) <_ ((A - B) + 1) <-> 1 <_ ((A - B) + 1))
11	7, 10	syl6bb 539	. . . . 5 |- ((A e. RR /\ B e. RR) -> (0 <_ (A - B) <-> 1 <_ ((A - B) + 1)))
12	1, 11	bitr3d 533	. . . 4 |- ((A e. RR /\ B e. RR) -> (B <_ A <-> 1 <_ ((A - B) + 1)))
13		zre 6307	. . . 4 |- (A e. ZZ -> A e. RR)
14		zre 6307	. . . 4 |- (B e. ZZ -> B e. RR)
15	12, 13, 14	syl2an 456	. . 3 |- ((A e. ZZ /\ B e. ZZ) -> (B <_ A <-> 1 <_ ((A - B) + 1)))
16		zsubcl 6336	. . . . 5 |- ((A e. ZZ /\ B e. ZZ) -> (A - B) e. ZZ)
17	16	peano2zdi 6335	. . . 4 |- ((A e. ZZ /\ B e. ZZ) -> ((A - B) + 1) e. ZZ)
18		elnnz1 6323	. . . . . . . 8 |- (((A - B) + 1) e. NN <-> (((A - B) + 1) e. ZZ /\ 1 <_ ((A - B) + 1)))
19		eleq1 1577	. . . . . . . . . 10 |- (z = 1 -> (z e. ZZ <-> 1 e. ZZ))
20		oprex 4041	. . . . . . . . . . . . . . 15 |- ((z - 1) + B) e. V
21	20	isseti 1861	. . . . . . . . . . . . . 14 |- E.x x = ((z - 1) + B)
22		ax-17 1007	. . . . . . . . . . . . . . . 16 |- ((z = 1 /\ B e. ZZ) -> A.x(z = 1 /\ B e. ZZ))
23	20	hbsbc1v 1995	. . . . . . . . . . . . . . . . 17 |- ([((z - 1) + B) / x]ph -> A.x[((z - 1) + B) / x]ph)
24		ax-17 1007	. . . . . . . . . . . . . . . . 17 |- (ps -> A.xps)
25	23, 24	hbbi 1046	. . . . . . . . . . . . . . . 16 |- (([((z - 1) + B) / x]ph <-> ps) -> A.x([((z - 1) + B) / x]ph <-> ps))
26	22, 25	hbim 1043	. . . . . . . . . . . . . . 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 1989	. . . . . . . . . . . . . . . . . 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		eqtr 1535	. . . . . . . . . . . . . . . . . . 19 |- ((x = ((z - 1) + B) /\ ((z - 1) + B) = B) -> x = B)
30		opreq1 4026	. . . . . . . . . . . . . . . . . . . . 21 |- (z = 1 -> (z - 1) = (1 - 1))
31	30	opreq1d 4033	. . . . . . . . . . . . . . . . . . . 20 |- (z = 1 -> ((z - 1) + B) = ((1 - 1) + B))
32		zcn 6308	. . . . . . . . . . . . . . . . . . . . . 22 |- (B e. ZZ -> B e. CC)
33		addid2 5483	. . . . . . . . . . . . . . . . . . . . . 22 |- (B e. CC -> (0 + B) = B)
34	32, 33	syl 10	. . . . . . . . . . . . . . . . . . . . 21 |- (B e. ZZ -> (0 + B) = B)
35	8	subidi 5545	. . . . . . . . . . . . . . . . . . . . . 22 |- (1 - 1) = 0
36	35	opreq1i 4029	. . . . . . . . . . . . . . . . . . . . 21 |- ((1 - 1) + B) = (0 + B)
37	34, 36	syl5eq 1562	. . . . . . . . . . . . . . . . . . . 20 |- (B e. ZZ -> ((1 - 1) + B) = B)
38	31, 37	sylan9eq 1570	. . . . . . . . . . . . . . . . . . 19 |- ((z = 1 /\ B e. ZZ) -> ((z - 1) + B) = B)
39	29, 38	sylan2 453	. . . . . . . . . . . . . . . . . 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 533	. . . . . . . . . . . . . . . 16 |- ((x = ((z - 1) + B) /\ (z = 1 /\ B e. ZZ)) -> ([((z - 1) + B) / x]ph <-> ps))
43	42	ex 371	. . . . . . . . . . . . . . 15 |- (x = ((z - 1) + B) -> ((z = 1 /\ B e. ZZ) -> ([((z - 1) + B) / x]ph <-> ps)))
44	26, 43	19.23ai 1100	. . . . . . . . . . . . . 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 371	. . . . . . . . . . . 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 588	. . . . . . . . . 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 629	. . . . . . . . 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 1577	. . . . . . . . . 10 |- (z = w -> (z e. ZZ <-> w e. ZZ))
51		oprex 4041	. . . . . . . . . . . . 13 |- ((w - 1) + B) e. V
52	51	isseti 1861	. . . . . . . . . . . 12 |- E.y y = ((w - 1) + B)
53		eeanv 1361	. . . . . . . . . . . . 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 1007	. . . . . . . . . . . . . . 15 |- (z = w -> A.x z = w)
55		ax-17 1007	. . . . . . . . . . . . . . . 16 |- ([((w - 1) + B) / y]ch -> A.x[((w - 1) + B) / y]ch)
56	23, 55	hbbi 1046	. . . . . . . . . . . . . . 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 1043	. . . . . . . . . . . . . 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 1007	. . . . . . . . . . . . . . . 16 |- (z = w -> A.y z = w)
59		ax-17 1007	. . . . . . . . . . . . . . . . 17 |- ([((z - 1) + B) / x]ph -> A.y[((z - 1) + B) / x]ph)
60	51	hbsbc1v 1995	. . . . . . . . . . . . . . . . 17 |- ([((w - 1) + B) / y]ch -> A.y[((w - 1) + B) / y]ch)
61	59, 60	hbbi 1046	. . . . . . . . . . . . . . . 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 1043	. . . . . . . . . . . . . . 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 1530	. . . . . . . . . . . . . . . . . 18 |- ((x = ((z - 1) + B) /\ y = ((w - 1) + B)) -> (x = y <-> ((z - 1) + B) = ((w - 1) + B)))
64		opreq1 4026	. . . . . . . . . . . . . . . . . . 19 |- (z = w -> (z - 1) = (w - 1))
65	64	opreq1d 4033	. . . . . . . . . . . . . . . . . 18 |- (z = w -> ((z - 1) + B) = ((w - 1) + B))
66	63, 65	syl5bir 208	. . . . . . . . . . . . . . . . 17 |- ((x = ((z - 1) + B) /\ y = ((w - 1) + B)) -> (z = w -> x = y))
67		uzindOLD.2	. . . . . . . . . . . . . . . . 17 |- (x = y -> (ph <-> ch))
68	66, 67	syl6 22	. . . . . . . . . . . . . . . 16 |- ((x = ((z - 1) + B) /\ y = ((w - 1) + B)) -> (z = w -> (ph <-> ch)))
69		sbceq1a 1989	. . . . . . . . . . . . . . . . 17 |- (y = ((w - 1) + B) -> (ch <-> [((w - 1) + B) / y]ch))
70	27, 69	bi2bian9 637	. . . . . . . . . . . . . . . 16 |- ((x = ((z - 1) + B) /\ y = ((w - 1) + B)) -> ((ph <-> ch) <-> ([((z - 1) + B) / x]ph <-> [((w - 1) + B) / y]ch)))
71	68, 70	sylibd 200	. . . . . . . . . . . . . . 15 |- ((x = ((z - 1) + B) /\ y = ((w - 1) + B)) -> (z = w -> ([((z - 1) + B) / x]ph <-> [((w - 1) + B) / y]ch)))
72	62, 71	19.23ai 1100	. . . . . . . . . . . . . 14 |- (E.y(x = ((z - 1) + B) /\ y = ((w - 1) + B)) -> (z = w -> ([((z - 1) + B) / x]ph <-> [((w - 1) + B) / y]ch)))
73	57, 72	19.23ai 1100	. . . . . . . . . . . . 13 |- (E.xE.y(x = ((z - 1) + B) /\ y = ((w - 1) + B)) -> (z = w -> ([((z - 1) + B) / x]ph <-> [((w - 1) + B) / y]ch)))
74	53, 73	sylbir 199	. . . . . . . . . . . 12 |- ((E.x x = ((z - 1) + B) /\ E.y y = ((w - 1) + B)) -> (z = w -> ([((z - 1) + B) / x]ph <-> [((w - 1) + B) / y]ch)))
75	21, 52, 74	mp2an 701	. . . . . . . . . . 11 |- (z = w -> ([((z - 1) + B) / x]ph <-> [((w - 1) + B) / y]ch))
76	75	imbi2d 615	. . . . . . . . . 10 |- (z = w -> (((A e. ZZ /\ B e. ZZ) -> [((z - 1) + B) / x]ph) <-> ((A e. ZZ /\ B e. ZZ) -> [((w - 1) + B) / y]ch)))
77	50, 76	imbi12d 629	. . . . . . . . 9 |- (z = w -> ((z e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> [((z - 1) + B) / x]ph)) <-> (w e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> [((w - 1) + B) / y]ch))))
78		eleq1 1577	. . . . . . . . . . 11 |- (z = (w + 1) -> (z e. ZZ <-> (w + 1) e. ZZ))
79		oprex 4041	. . . . . . . . . . . . . 14 |- ((((z - 1) + B) - 1) + 1) e. V
80	79	isseti 1861	. . . . . . . . . . . . 13 |- E.x x = ((((z - 1) + B) - 1) + 1)
81		oprex 4041	. . . . . . . . . . . . . 14 |- ((((w + 1) - 1) + B) - 1) e. V
82	81	isseti 1861	. . . . . . . . . . . . 13 |- E.y y = ((((w + 1) - 1) + B) - 1)
83		eeanv 1361	. . . . . . . . . . . . . 14 |- (E.xE.y(x = ((((z - 1) + B) - 1) + 1) /\ y = ((((w + 1) - 1) + B) - 1)) <-> (E.x x = ((((z - 1) + B) - 1) + 1) /\ E.y y = ((((w + 1) - 1) + B) - 1)))
84		ax-17 1007	. . . . . . . . . . . . . . . 16 |- (z = (w + 1) -> A.x z = (w + 1))
85	79	hbsbc1v 1995	. . . . . . . . . . . . . . . . 17 |- ([((((z - 1) + B) - 1) + 1) / x]ph -> A.x[((((z - 1) + B) - 1) + 1) / x]ph)
86		ax-17 1007	. . . . . . . . . . . . . . . . 17 |- ([((((w + 1) - 1) + B) - 1) / y]th -> A.x[((((w + 1) - 1) + B) - 1) / y]th)
87	85, 86	hbbi 1046	. . . . . . . . . . . . . . . 16 |- (([((((z - 1) + B) - 1) + 1) / x]ph <-> [((((w + 1) - 1) + B) - 1) / y]th) -> A.x([((((z - 1) + B) - 1) + 1) / x]ph <-> [((((w + 1) - 1) + B) - 1) / y]th))
88	84, 87	hbim 1043	. . . . . . . . . . . . . . 15 |- ((z = (w + 1) -> ([((((z - 1) + B) - 1) + 1) / x]ph <-> [((((w + 1) - 1) + B) - 1) / y]th)) -> A.x(z = (w + 1) -> ([((((z - 1) + B) - 1) + 1) / x]ph <-> [((((w + 1) - 1) + B) - 1) / y]th)))
89		ax-17 1007	. . . . . . . . . . . . . . . . 17 |- (z = (w + 1) -> A.y z = (w + 1))
90		ax-17 1007	. . . . . . . . . . . . . . . . . 18 |- ([((((z - 1) + B) - 1) + 1) / x]ph -> A.y[((((z - 1) + B) - 1) + 1) / x]ph)
91	81	hbsbc1v 1995	. . . . . . . . . . . . . . . . . 18 |- ([((((w + 1) - 1) + B) - 1) / y]th -> A.y[((((w + 1) - 1) + B) - 1) / y]th)
92	90, 91	hbbi 1046	. . . . . . . . . . . . . . . . 17 |- (([((((z - 1) + B) - 1) + 1) / x]ph <-> [((((w + 1) - 1) + B) - 1) / y]th) -> A.y([((((z - 1) + B) - 1) + 1) / x]ph <-> [((((w + 1) - 1) + B) - 1) / y]th))
93	89, 92	hbim 1043	. . . . . . . . . . . . . . . 16 |- ((z = (w + 1) -> ([((((z - 1) + B) - 1) + 1) / x]ph <-> [((((w + 1) - 1) + B) - 1) / y]th)) -> A.y(z = (w + 1) -> ([((((z - 1) + B) - 1) + 1) / x]ph <-> [((((w + 1) - 1) + B) - 1) / y]th)))
94		eqeq12 1530	. . . . . . . . . . . . . . . . . . . 20 |- ((x = ((((z - 1) + B) - 1) + 1) /\ (y + 1) = (((((w + 1) - 1) + B) - 1) + 1)) -> (x = (y + 1) <-> ((((z - 1) + B) - 1) + 1) = (((((w + 1) - 1) + B) - 1) + 1)))
95		opreq1 4026	. . . . . . . . . . . . . . . . . . . 20 |- (y = ((((w + 1) - 1) + B) - 1) -> (y + 1) = (((((w + 1) - 1) + B) - 1) + 1))
96	94, 95	sylan2 453	. . . . . . . . . . . . . . . . . . 19 |- ((x = ((((z - 1) + B) - 1) + 1) /\ y = ((((w + 1) - 1) + B) - 1)) -> (x = (y + 1) <-> ((((z - 1) + B) - 1) + 1) = (((((w + 1) - 1) + B) - 1) + 1)))
97		opreq1 4026	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = (w + 1) -> (z - 1) = ((w + 1) - 1))
98	97	opreq1d 4033	. . . . . . . . . . . . . . . . . . . . 21 |- (z = (w + 1) -> ((z - 1) + B) = (((w + 1) - 1) + B))
99	98	opreq1d 4033	. . . . . . . . . . . . . . . . . . . 20 |- (z = (w + 1) -> (((z - 1) + B) - 1) = ((((w + 1) - 1) + B) - 1))
100	99	opreq1d 4033	. . . . . . . . . . . . . . . . . . 19 |- (z = (w + 1) -> ((((z - 1) + B) - 1) + 1) = (((((w + 1) - 1) + B) - 1) + 1))
101	96, 100	syl5bir 208	. . . . . . . . . . . . . . . . . 18 |- ((x = ((((z - 1) + B) - 1) + 1) /\ y = ((((w + 1) - 1) + B) - 1)) -> (z = (w + 1) -> x = (y + 1)))
102		uzindOLD.3	. . . . . . . . . . . . . . . . . 18 |- (x = (y + 1) -> (ph <-> th))
103	101, 102	syl6 22	. . . . . . . . . . . . . . . . 17 |- ((x = ((((z - 1) + B) - 1) + 1) /\ y = ((((w + 1) - 1) + B) - 1)) -> (z = (w + 1) -> (ph <-> th)))
104		sbceq1a 1989	. . . . . . . . . . . . . . . . . 18 |- (x = ((((z - 1) + B) - 1) + 1) -> (ph <-> [((((z - 1) + B) - 1) + 1) / x]ph))
105		sbceq1a 1989	. . . . . . . . . . . . . . . . . 18 |- (y = ((((w + 1) - 1) + B) - 1) -> (th <-> [((((w + 1) - 1) + B) - 1) / y]th))
106	104, 105	bi2bian9 637	. . . . . . . . . . . . . . . . 17 |- ((x = ((((z - 1) + B) - 1) + 1) /\ y = ((((w + 1) - 1) + B) - 1)) -> ((ph <-> th) <-> ([((((z - 1) + B) - 1) + 1) / x]ph <-> [((((w + 1) - 1) + B) - 1) / y]th)))
107	103, 106	sylibd 200	. . . . . . . . . . . . . . . 16 |- ((x = ((((z - 1) + B) - 1) + 1) /\ y = ((((w + 1) - 1) + B) - 1)) -> (z = (w + 1) -> ([((((z - 1) + B) - 1) + 1) / x]ph <-> [((((w + 1) - 1) + B) - 1) / y]th)))
108	93, 107	19.23ai 1100	. . . . . . . . . . . . . . 15 |- (E.y(x = ((((z - 1) + B) - 1) + 1) /\ y = ((((w + 1) - 1) + B) - 1)) -> (z = (w + 1) -> ([((((z - 1) + B) - 1) + 1) / x]ph <-> [((((w + 1) - 1) + B) - 1) / y]th)))
109	88, 108	19.23ai 1100	. . . . . . . . . . . . . 14 |- (E.xE.y(x = ((((z - 1) + B) - 1) + 1) /\ y = ((((w + 1) - 1) + B) - 1)) -> (z = (w + 1) -> ([((((z - 1) + B) - 1) + 1) / x]ph <-> [((((w + 1) - 1) + B) - 1) / y]th)))
110	83, 109	sylbir 199	. . . . . . . . . . . . 13 |- ((E.x x = ((((z - 1) + B) - 1) + 1) /\ E.y y = ((((w + 1) - 1) + B) - 1)) -> (z = (w + 1) -> ([((((z - 1) + B) - 1) + 1) / x]ph <-> [((((w + 1) - 1) + B) - 1) / y]th)))
111	80, 82, 110	mp2an 701	. . . . . . . . . . . 12 |- (z = (w + 1) -> ([((((z - 1) + B) - 1) + 1) / x]ph <-> [((((w + 1) - 1) + B) - 1) / y]th))
112	111	imbi2d 615	. . . . . . . . . . 11 |- (z = (w + 1) -> (((A e. ZZ /\ B e. ZZ) -> [((((z - 1) + B) - 1) + 1) / x]ph) <-> ((A e. ZZ /\ B e. ZZ) -> [((((w + 1) - 1) + B) - 1) / y]th)))
113	78, 112	imbi12d 629	. . . . . . . . . 10 |- (z = (w + 1) -> ((z e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> [((((z - 1) + B) - 1) + 1) / x]ph)) <-> ((w + 1) e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> [((((w + 1) - 1) + B) - 1) / y]th))))
114		addcl 5455	. . . . . . . . . . . . . . . . . 18 |- (((z - 1) e. CC /\ B e. CC) -> ((z - 1) + B) e. CC)
115		subcl 5521	. . . . . . . . . . . . . . . . . . 19 |- ((z e. CC /\ 1 e. CC) -> (z - 1) e. CC)
116	8, 115	mpan2 700	. . . . . . . . . . . . . . . . . 18 |- (z e. CC -> (z - 1) e. CC)
117	114, 116	sylan 450	. . . . . . . . . . . . . . . . 17 |- ((z e. CC /\ B e. CC) -> ((z - 1) + B) e. CC)
118		npcan 5553	. . . . . . . . . . . . . . . . . 18 |- ((((z - 1) + B) e. CC /\ 1 e. CC) -> ((((z - 1) + B) - 1) + 1) = ((z - 1) + B))
119	8, 118	mpan2 700	. . . . . . . . . . . . . . . . 17 |- (((z - 1) + B) e. CC -> ((((z - 1) + B) - 1) + 1) = ((z - 1) + B))
120	117, 119	syl 10	. . . . . . . . . . . . . . . 16 |- ((z e. CC /\ B e. CC) -> ((((z - 1) + B) - 1) + 1) = ((z - 1) + B))
121		zcn 6308	. . . . . . . . . . . . . . . 16 |- (z e. ZZ -> z e. CC)
122	120, 121, 32	syl2an 456	. . . . . . . . . . . . . . 15 |- ((z e. ZZ /\ B e. ZZ) -> ((((z - 1) + B) - 1) + 1) = ((z - 1) + B))
123	122	ex 371	. . . . . . . . . . . . . 14 |- (z e. ZZ -> (B e. ZZ -> ((((z - 1) + B) - 1) + 1) = ((z - 1) + B)))
124	123	adantld 390	. . . . . . . . . . . . 13 |- (z e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> ((((z - 1) + B) - 1) + 1) = ((z - 1) + B)))
125		dfsbcq 1988	. . . . . . . . . . . . 13 |- (((((z - 1) + B) - 1) + 1) = ((z - 1) + B) -> ([((((z - 1) + B) - 1) + 1) / x]ph <-> [((z - 1) + B) / x]ph))
126	124, 125	syl6 22	. . . . . . . . . . . 12 |- (z e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> ([((((z - 1) + B) - 1) + 1) / x]ph <-> [((z - 1) + B) / x]ph)))
127	126	pm5.74d 588	. . . . . . . . . . 11 |- (z e. ZZ -> (((A e. ZZ /\ B e. ZZ) -> [((((z - 1) + B) - 1) + 1) / x]ph) <-> ((A e. ZZ /\ B e. ZZ) -> [((z - 1) + B) / x]ph)))
128	127	pm5.74i 587	. . . . . . . . . 10 |- ((z e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> [((((z - 1) + B) - 1) + 1) / x]ph)) <-> (z e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> [((z - 1) + B) / x]ph)))
129	113, 128	syl5bbr 537	. . . . . . . . 9 |- (z = (w + 1) -> ((z e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> [((z - 1) + B) / x]ph)) <-> ((w + 1) e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> [((((w + 1) - 1) + B) - 1) / y]th))))
130		eleq1 1577	. . . . . . . . . 10 |- (z = ((A - B) + 1) -> (z e. ZZ <-> ((A - B) + 1) e. ZZ))
131		ax-17 1007	. . . . . . . . . . . . . 14 |- ((z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ)) -> A.x(z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ)))
132		ax-17 1007	. . . . . . . . . . . . . . 15 |- (ta -> A.xta)
133	23, 132	hbbi 1046	. . . . . . . . . . . . . 14 |- (([((z - 1) + B) / x]ph <-> ta) -> A.x([((z - 1) + B) / x]ph <-> ta))
134	131, 133	hbim 1043	. . . . . . . . . . . . 13 |- (((z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ)) -> ([((z - 1) + B) / x]ph <-> ta)) -> A.x((z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ)) -> ([((z - 1) + B) / x]ph <-> ta)))
135	27	adantr 389	. . . . . . . . . . . . . . 15 |- ((x = ((z - 1) + B) /\ (z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ))) -> (ph <-> [((z - 1) + B) / x]ph))
136		eqtr 1535	. . . . . . . . . . . . . . . . . . 19 |- ((x = ((z - 1) + B) /\ ((z - 1) + B) = ((((A - B) + 1) - 1) + B)) -> x = ((((A - B) + 1) - 1) + B))
137		opreq1 4026	. . . . . . . . . . . . . . . . . . . 20 |- (z = ((A - B) + 1) -> (z - 1) = (((A - B) + 1) - 1))
138	137	opreq1d 4033	. . . . . . . . . . . . . . . . . . 19 |- (z = ((A - B) + 1) -> ((z - 1) + B) = ((((A - B) + 1) - 1) + B))
139	136, 138	sylan2 453	. . . . . . . . . . . . . . . . . 18 |- ((x = ((z - 1) + B) /\ z = ((A - B) + 1)) -> x = ((((A - B) + 1) - 1) + B))
140		add23 5491	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((A - B) e. CC /\ 1 e. CC /\ B e. CC) -> (((A - B) + 1) + B) = (((A - B) + B) + 1))
141		subcl 5521	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. CC /\ B e. CC) -> (A - B) e. CC)
142	8	a1i 8	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. CC /\ B e. CC) -> 1 e. CC)
143		pm3.27 321	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. CC /\ B e. CC) -> B e. CC)
144	140, 141, 142, 143	syl3anc 864	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. CC /\ B e. CC) -> (((A - B) + 1) + B) = (((A - B) + B) + 1))
145		npcan 5553	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. CC /\ B e. CC) -> ((A - B) + B) = A)
146	145	opreq1d 4033	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. CC /\ B e. CC) -> (((A - B) + B) + 1) = (A + 1))
147	144, 146	eqtrd 1550	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. CC /\ B e. CC) -> (((A - B) + 1) + B) = (A + 1))
148	147	opreq1d 4033	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. CC /\ B e. CC) -> ((((A - B) + 1) + B) - 1) = ((A + 1) - 1))
149		addsub 5538	. . . . . . . . . . . . . . . . . . . . 21 |- ((((A - B) + 1) e. CC /\ B e. CC /\ 1 e. CC) -> ((((A - B) + 1) + B) - 1) = ((((A - B) + 1) - 1) + B))
150		peano2cn 5498	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A - B) e. CC -> ((A - B) + 1) e. CC)
151	141, 150	syl 10	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. CC /\ B e. CC) -> ((A - B) + 1) e. CC)
152	149, 151, 143, 142	syl3anc 864	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. CC /\ B e. CC) -> ((((A - B) + 1) + B) - 1) = ((((A - B) + 1) - 1) + B))
153		pncan 5551	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. CC /\ 1 e. CC) -> ((A + 1) - 1) = A)
154	8, 153	mpan2 700	. . . . . . . . . . . . . . . . . . . . 21 |- (A e. CC -> ((A + 1) - 1) = A)
155	154	adantr 389	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. CC /\ B e. CC) -> ((A + 1) - 1) = A)
156	148, 152, 155	3eqtr3d 1558	. . . . . . . . . . . . . . . . . . 19 |- ((A e. CC /\ B e. CC) -> ((((A - B) + 1) - 1) + B) = A)
157		zcn 6308	. . . . . . . . . . . . . . . . . . 19 |- (A e. ZZ -> A e. CC)
158	156, 157, 32	syl2an 456	. . . . . . . . . . . . . . . . . 18 |- ((A e. ZZ /\ B e. ZZ) -> ((((A - B) + 1) - 1) + B) = A)
159	139, 158	sylan9eq 1570	. . . . . . . . . . . . . . . . 17 |- (((x = ((z - 1) + B) /\ z = ((A - B) + 1)) /\ (A e. ZZ /\ B e. ZZ)) -> x = A)
160	159	anasss 442	. . . . . . . . . . . . . . . 16 |- ((x = ((z - 1) + B) /\ (z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ))) -> x = A)
161		uzindOLD.4	. . . . . . . . . . . . . . . 16 |- (x = A -> (ph <-> ta))
162	160, 161	syl 10	. . . . . . . . . . . . . . 15 |- ((x = ((z - 1) + B) /\ (z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ))) -> (ph <-> ta))
163	135, 162	bitr3d 533	. . . . . . . . . . . . . 14 |- ((x = ((z - 1) + B) /\ (z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ))) -> ([((z - 1) + B) / x]ph <-> ta))
164	163	ex 371	. . . . . . . . . . . . 13 |- (x = ((z - 1) + B) -> ((z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ)) -> ([((z - 1) + B) / x]ph <-> ta)))
165	134, 164	19.23ai 1100	. . . . . . . . . . . 12 |- (E.x x = ((z - 1) + B) -> ((z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ)) -> ([((z - 1) + B) / x]ph <-> ta)))
166	21, 165	ax-mp 7	. . . . . . . . . . 11 |- ((z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ)) -> ([((z - 1) + B) / x]ph <-> ta))
167	166	pm5.74da 589	. . . . . . . . . 10 |- (z = ((A - B) + 1) -> (((A e. ZZ /\ B e. ZZ) -> [((z - 1) + B) / x]ph) <-> ((A e. ZZ /\ B e. ZZ) -> ta)))
168	130, 167	imbi12d 629	. . . . . . . . 9 |- (z = ((A - B) + 1) -> ((z e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> [((z - 1) + B) / x]ph)) <-> (((A - B) + 1) e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> ta))))
169		uzindOLD.5	. . . . . . . . . . 11 |- ps
170	169	a1i 8	. . . . . . . . . 10 |- ((A e. ZZ /\ B e. ZZ) -> ps)
171	170	a1i 8	. . . . . . . . 9 |- (1 e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> ps))
172		nnz 6321	. . . . . . . . . . 11 |- (w e. NN -> w e. ZZ)
173	172	a1d 12	. . . . . . . . . 10 |- (w e. NN -> ((w + 1) e. ZZ -> w e. ZZ))
174		ax-17 1007	. . . . . . . . . . . . . . . . 17 |- ((w e. NN /\ B e. ZZ) -> A.y(w e. NN /\ B e. ZZ))
175	51	hbsbc1v 1995	. . . . . . . . . . . . . . . . . 18 |- ([((w - 1) + B) / y]th -> A.y[((w - 1) + B) / y]th)
176	60, 175	hbim 1043	. . . . . . . . . . . . . . . . 17 |- (([((w - 1) + B) / y]ch -> [((w - 1) + B) / y]th) -> A.y([((w - 1) + B) / y]ch -> [((w - 1) + B) / y]th))
177	174, 176	hbim 1043	. . . . . . . . . . . . . . . 16 |- (((w e. NN /\ B e. ZZ) -> ([((w - 1) + B) / y]ch -> [((w - 1) + B) / y]th)) -> A.y((w e. NN /\ B e. ZZ) -> ([((w - 1) + B) / y]ch -> [((w - 1) + B) / y]th)))
178		uzindOLD.6	. . . . . . . . . . . . . . . . 17 |- (((y e. ZZ /\ B e. ZZ) /\ B <_ y) -> (ch -> th))
179		eleq1 1577	. . . . . . . . . . . . . . . . . . . . 21 |- (y = ((w - 1) + B) -> (y e. ZZ <-> ((w - 1) + B) e. ZZ))
180	179	anbi1d 620	. . . . . . . . . . . . . . . . . . . 20 |- (y = ((w - 1) + B) -> ((y e. ZZ /\ B e. ZZ) <-> (((w - 1) + B) e. ZZ /\ B e. ZZ)))
181		breq2 2696	. . . . . . . . . . . . . . . . . . . 20 |- (y = ((w - 1) + B) -> (B <_ y <-> B <_ ((w - 1) + B)))
182	180, 181	anbi12d 631	. . . . . . . . . . . . . . . . . . 19 |- (y = ((w - 1) + B) -> (((y e. ZZ /\ B e. ZZ) /\ B <_ y) <-> ((((w - 1) + B) e. ZZ /\ B e. ZZ) /\ B <_ ((w - 1) + B))))
183		zaddcl 6333	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((w - 1) e. ZZ /\ B e. ZZ) -> ((w - 1) + B) e. ZZ)
184		peano2zm 6337	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w e. ZZ -> (w - 1) e. ZZ)
185	183, 184	sylan 450	. . . . . . . . . . . . . . . . . . . . . 22 |- ((w e. ZZ /\ B e. ZZ) -> ((w - 1) + B) e. ZZ)
186	185, 172	sylan 450	. . . . . . . . . . . . . . . . . . . . 21 |- ((w e. NN /\ B e. ZZ) -> ((w - 1) + B) e. ZZ)
187		pm3.27 321	. . . . . . . . . . . . . . . . . . . . 21 |- ((w e. NN /\ B e. ZZ) -> B e. ZZ)
188	186, 187	jca 286	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. NN /\ B e. ZZ) -> (((w - 1) + B) e. ZZ /\ B e. ZZ))
189		lesub1 5814	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B e. RR /\ ((w - 1) + B) e. RR /\ (B - 1) e. RR) -> (B <_ ((w - 1) + B) <-> (B - (B - 1)) <_ (((w - 1) + B) - (B - 1))))
190		pm3.27 321	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. RR /\ B e. RR) -> B e. RR)
191		readdcl 5456	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((w - 1) e. RR /\ B e. RR) -> ((w - 1) + B) e. RR)
192		peano2rem 5596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w e. RR -> (w - 1) e. RR)
193	191, 192	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. RR /\ B e. RR) -> ((w - 1) + B) e. RR)
194		peano2rem 5596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (B e. RR -> (B - 1) e. RR)
195	194	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. RR /\ B e. RR) -> (B - 1) e. RR)
196	189, 190, 193, 195	syl3anc 864	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((w e. RR /\ B e. RR) -> (B <_ ((w - 1) + B) <-> (B - (B - 1)) <_ (((w - 1) + B) - (B - 1))))
197		subsub 5616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((B e. CC /\ B e. CC /\ 1 e. CC) -> (B - (B - 1)) = ((B - B) + 1))
198	8, 197	mp3an3 911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((B e. CC /\ B e. CC) -> (B - (B - 1)) = ((B - B) + 1))
199	198	anidms 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (B e. CC -> (B - (B - 1)) = ((B - B) + 1))
200		subid 5549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (B e. CC -> (B - B) = 0)
201	200	opreq1d 4033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (B e. CC -> ((B - B) + 1) = (0 + 1))
202	201, 9	syl6eq 1566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (B e. CC -> ((B - B) + 1) = 1)
203	199, 202	eqtrd 1550	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (B e. CC -> (B - (B - 1)) = 1)
204	203	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((w e. CC /\ B e. CC) -> (B - (B - 1)) = 1)
205		addcl 5455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((w - 1) e. CC /\ B e. CC) -> ((w - 1) +