Theorem uzindOLD 7420

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 6863	. . . . 5 |- ((A e. RR /\ B e. RR) -> (0 <_ (A - B) <-> B <_ A))
2		resubcl 6601	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> (A - B) e. RR)
3		0re 6603	. . . . . . . 8 |- 0 e. RR
4		1re 6598	. . . . . . . 8 |- 1 e. RR
5		leadd1 6808	. . . . . . . 8 |- ((0 e. RR /\ (A - B) e. RR /\ 1 e. RR) -> (0 <_ (A - B) <-> (0 + 1) <_ ((A - B) + 1)))
6	3, 4, 5	mp3an13 1182	. . . . . . 7 |- ((A - B) e. RR -> (0 <_ (A - B) <-> (0 + 1) <_ ((A - B) + 1)))
7	2, 6	syl 12	. . . . . 6 |- ((A e. RR /\ B e. RR) -> (0 <_ (A - B) <-> (0 + 1) <_ ((A - B) + 1)))
8		ax1cn 6422	. . . . . . . 8 |- 1 e. CC
9	8	addid2i 6484	. . . . . . 7 |- (0 + 1) = 1
10	9	breq1i 3345	. . . . . 6 |- ((0 + 1) <_ ((A - B) + 1) <-> 1 <_ ((A - B) + 1))
11	7, 10	syl6bb 595	. . . . 5 |- ((A e. RR /\ B e. RR) -> (0 <_ (A - B) <-> 1 <_ ((A - B) + 1)))
12	1, 11	bitr3d 589	. . . 4 |- ((A e. RR /\ B e. RR) -> (B <_ A <-> 1 <_ ((A - B) + 1)))
13		zre 7348	. . . 4 |- (A e. ZZ -> A e. RR)
14		zre 7348	. . . 4 |- (B e. ZZ -> B e. RR)
15	12, 13, 14	syl2an 503	. . 3 |- ((A e. ZZ /\ B e. ZZ) -> (B <_ A <-> 1 <_ ((A - B) + 1)))
16		zsubcl 7377	. . . . 5 |- ((A e. ZZ /\ B e. ZZ) -> (A - B) e. ZZ)
17	16	peano2zdi 7376	. . . 4 |- ((A e. ZZ /\ B e. ZZ) -> ((A - B) + 1) e. ZZ)
18		elnnz1 7364	. . . . . . . 8 |- (((A - B) + 1) e. NN <-> (((A - B) + 1) e. ZZ /\ 1 <_ ((A - B) + 1)))
19		eleq1 1957	. . . . . . . . . 10 |- (z = 1 -> (z e. ZZ <-> 1 e. ZZ))
20		oprex 4907	. . . . . . . . . . . . . . 15 |- ((z - 1) + B) e. _V
21	20	isseti 2297	. . . . . . . . . . . . . 14 |- E.x x = ((z - 1) + B)
22		ax-17 1317	. . . . . . . . . . . . . . . 16 |- ((z = 1 /\ B e. ZZ) -> A.x(z = 1 /\ B e. ZZ))
23	20	hbsbc1v 2464	. . . . . . . . . . . . . . . . 17 |- ([((z - 1) + B) / x]ph -> A.x[((z - 1) + B) / x]ph)
24		ax-17 1317	. . . . . . . . . . . . . . . . 17 |- (ps -> A.xps)
25	23, 24	hbbi 1357	. . . . . . . . . . . . . . . 16 |- (([((z - 1) + B) / x]ph <-> ps) -> A.x([((z - 1) + B) / x]ph <-> ps))
26	22, 25	hbim 1354	. . . . . . . . . . . . . . 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 2456	. . . . . . . . . . . . . . . . . 18 |- (x = ((z - 1) + B) -> (ph <-> [((z - 1) + B) / x]ph))
28	27	adantr 425	. . . . . . . . . . . . . . . . 17 |- ((x = ((z - 1) + B) /\ (z = 1 /\ B e. ZZ)) -> (ph <-> [((z - 1) + B) / x]ph))
29		eqtr 1904	. . . . . . . . . . . . . . . . . . 19 |- ((x = ((z - 1) + B) /\ ((z - 1) + B) = B) -> x = B)
30		opreq1 4889	. . . . . . . . . . . . . . . . . . . . 21 |- (z = 1 -> (z - 1) = (1 - 1))
31	30	opreq1d 4897	. . . . . . . . . . . . . . . . . . . 20 |- (z = 1 -> ((z - 1) + B) = ((1 - 1) + B))
32		zcn 7349	. . . . . . . . . . . . . . . . . . . . . 22 |- (B e. ZZ -> B e. CC)
33		addid2 6482	. . . . . . . . . . . . . . . . . . . . . 22 |- (B e. CC -> (0 + B) = B)
34	32, 33	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (B e. ZZ -> (0 + B) = B)
35	8	subidi 6551	. . . . . . . . . . . . . . . . . . . . . 22 |- (1 - 1) = 0
36	35	opreq1i 4892	. . . . . . . . . . . . . . . . . . . . 21 |- ((1 - 1) + B) = (0 + B)
37	34, 36	syl5eq 1940	. . . . . . . . . . . . . . . . . . . 20 |- (B e. ZZ -> ((1 - 1) + B) = B)
38	31, 37	sylan9eq 1948	. . . . . . . . . . . . . . . . . . 19 |- ((z = 1 /\ B e. ZZ) -> ((z - 1) + B) = B)
39	29, 38	sylan2 500	. . . . . . . . . . . . . . . . . 18 |- ((x = ((z - 1) + B) /\ (z = 1 /\ B e. ZZ)) -> x = B)
40		uzindOLD.1	. . . . . . . . . . . . . . . . . 18 |- (x = B -> (ph <-> ps))
41	39, 40	syl 12	. . . . . . . . . . . . . . . . 17 |- ((x = ((z - 1) + B) /\ (z = 1 /\ B e. ZZ)) -> (ph <-> ps))
42	28, 41	bitr3d 589	. . . . . . . . . . . . . . . 16 |- ((x = ((z - 1) + B) /\ (z = 1 /\ B e. ZZ)) -> ([((z - 1) + B) / x]ph <-> ps))
43	42	ex 402	. . . . . . . . . . . . . . 15 |- (x = ((z - 1) + B) -> ((z = 1 /\ B e. ZZ) -> ([((z - 1) + B) / x]ph <-> ps)))
44	26, 43	19.23ai 1412	. . . . . . . . . . . . . 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 402	. . . . . . . . . . . 12 |- (z = 1 -> (B e. ZZ -> ([((z - 1) + B) / x]ph <-> ps)))
47	46	adantld 426	. . . . . . . . . . 11 |- (z = 1 -> ((A e. ZZ /\ B e. ZZ) -> ([((z - 1) + B) / x]ph <-> ps)))
48	47	pm5.74d 645	. . . . . . . . . 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 688	. . . . . . . . 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 1957	. . . . . . . . . 10 |- (z = w -> (z e. ZZ <-> w e. ZZ))
51		oprex 4907	. . . . . . . . . . . . 13 |- ((w - 1) + B) e. _V
52	51	isseti 2297	. . . . . . . . . . . 12 |- E.y y = ((w - 1) + B)
53		eeanv 1707	. . . . . . . . . . . . 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 1317	. . . . . . . . . . . . . . 15 |- (z = w -> A.x z = w)
55		ax-17 1317	. . . . . . . . . . . . . . . 16 |- ([((w - 1) + B) / y]ch -> A.x[((w - 1) + B) / y]ch)
56	23, 55	hbbi 1357	. . . . . . . . . . . . . . 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 1354	. . . . . . . . . . . . . 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 1317	. . . . . . . . . . . . . . . 16 |- (z = w -> A.y z = w)
59		ax-17 1317	. . . . . . . . . . . . . . . . 17 |- ([((z - 1) + B) / x]ph -> A.y[((z - 1) + B) / x]ph)
60	51	hbsbc1v 2464	. . . . . . . . . . . . . . . . 17 |- ([((w - 1) + B) / y]ch -> A.y[((w - 1) + B) / y]ch)
61	59, 60	hbbi 1357	. . . . . . . . . . . . . . . 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 1354	. . . . . . . . . . . . . . 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 1896	. . . . . . . . . . . . . . . . . 18 |- ((x = ((z - 1) + B) /\ y = ((w - 1) + B)) -> (x = y <-> ((z - 1) + B) = ((w - 1) + B)))
64		opreq1 4889	. . . . . . . . . . . . . . . . . . 19 |- (z = w -> (z - 1) = (w - 1))
65	64	opreq1d 4897	. . . . . . . . . . . . . . . . . 18 |- (z = w -> ((z - 1) + B) = ((w - 1) + B))
66	63, 65	syl5bir 227	. . . . . . . . . . . . . . . . 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 25	. . . . . . . . . . . . . . . 16 |- ((x = ((z - 1) + B) /\ y = ((w - 1) + B)) -> (z = w -> (ph <-> ch)))
69		sbceq1a 2456	. . . . . . . . . . . . . . . . 17 |- (y = ((w - 1) + B) -> (ch <-> [((w - 1) + B) / y]ch))
70	27, 69	bi2bian9 696	. . . . . . . . . . . . . . . 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 219	. . . . . . . . . . . . . . 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 1412	. . . . . . . . . . . . . 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 1412	. . . . . . . . . . . . 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 218	. . . . . . . . . . . 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 761	. . . . . . . . . . 11 |- (z = w -> ([((z - 1) + B) / x]ph <-> [((w - 1) + B) / y]ch))
76	75	imbi2d 674	. . . . . . . . . 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 688	. . . . . . . . 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 1957	. . . . . . . . . . 11 |- (z = (w + 1) -> (z e. ZZ <-> (w + 1) e. ZZ))
79		oprex 4907	. . . . . . . . . . . . . 14 |- ((((z - 1) + B) - 1) + 1) e. _V
80	79	isseti 2297	. . . . . . . . . . . . 13 |- E.x x = ((((z - 1) + B) - 1) + 1)
81		oprex 4907	. . . . . . . . . . . . . 14 |- ((((w + 1) - 1) + B) - 1) e. _V
82	81	isseti 2297	. . . . . . . . . . . . 13 |- E.y y = ((((w + 1) - 1) + B) - 1)
83		eeanv 1707	. . . . . . . . . . . . . 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 1317	. . . . . . . . . . . . . . . 16 |- (z = (w + 1) -> A.x z = (w + 1))
85	79	hbsbc1v 2464	. . . . . . . . . . . . . . . . 17 |- ([((((z - 1) + B) - 1) + 1) / x]ph -> A.x[((((z - 1) + B) - 1) + 1) / x]ph)
86		ax-17 1317	. . . . . . . . . . . . . . . . 17 |- ([((((w + 1) - 1) + B) - 1) / y]th -> A.x[((((w + 1) - 1) + B) - 1) / y]th)
87	85, 86	hbbi 1357	. . . . . . . . . . . . . . . 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 1354	. . . . . . . . . . . . . . 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 1317	. . . . . . . . . . . . . . . . 17 |- (z = (w + 1) -> A.y z = (w + 1))
90		ax-17 1317	. . . . . . . . . . . . . . . . . 18 |- ([((((z - 1) + B) - 1) + 1) / x]ph -> A.y[((((z - 1) + B) - 1) + 1) / x]ph)
91	81	hbsbc1v 2464	. . . . . . . . . . . . . . . . . 18 |- ([((((w + 1) - 1) + B) - 1) / y]th -> A.y[((((w + 1) - 1) + B) - 1) / y]th)
92	90, 91	hbbi 1357	. . . . . . . . . . . . . . . . 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 1354	. . . . . . . . . . . . . . . 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 1896	. . . . . . . . . . . . . . . . . . . 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 4889	. . . . . . . . . . . . . . . . . . . 20 |- (y = ((((w + 1) - 1) + B) - 1) -> (y + 1) = (((((w + 1) - 1) + B) - 1) + 1))
96	94, 95	sylan2 500	. . . . . . . . . . . . . . . . . . 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 4889	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = (w + 1) -> (z - 1) = ((w + 1) - 1))
98	97	opreq1d 4897	. . . . . . . . . . . . . . . . . . . . 21 |- (z = (w + 1) -> ((z - 1) + B) = (((w + 1) - 1) + B))
99	98	opreq1d 4897	. . . . . . . . . . . . . . . . . . . 20 |- (z = (w + 1) -> (((z - 1) + B) - 1) = ((((w + 1) - 1) + B) - 1))
100	99	opreq1d 4897	. . . . . . . . . . . . . . . . . . 19 |- (z = (w + 1) -> ((((z - 1) + B) - 1) + 1) = (((((w + 1) - 1) + B) - 1) + 1))
101	96, 100	syl5bir 227	. . . . . . . . . . . . . . . . . 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 25	. . . . . . . . . . . . . . . . 17 |- ((x = ((((z - 1) + B) - 1) + 1) /\ y = ((((w + 1) - 1) + B) - 1)) -> (z = (w + 1) -> (ph <-> th)))
104		sbceq1a 2456	. . . . . . . . . . . . . . . . . 18 |- (x = ((((z - 1) + B) - 1) + 1) -> (ph <-> [((((z - 1) + B) - 1) + 1) / x]ph))
105		sbceq1a 2456	. . . . . . . . . . . . . . . . . 18 |- (y = ((((w + 1) - 1) + B) - 1) -> (th <-> [((((w + 1) - 1) + B) - 1) / y]th))
106	104, 105	bi2bian9 696	. . . . . . . . . . . . . . . . 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 219	. . . . . . . . . . . . . . . 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 1412	. . . . . . . . . . . . . . 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 1412	. . . . . . . . . . . . . 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 218	. . . . . . . . . . . . 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 761	. . . . . . . . . . . 12 |- (z = (w + 1) -> ([((((z - 1) + B) - 1) + 1) / x]ph <-> [((((w + 1) - 1) + B) - 1) / y]th))
112	111	imbi2d 674	. . . . . . . . . . 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 688	. . . . . . . . . 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		npcan 6559	. . . . . . . . . . . . . . . . 17 |- ((((z - 1) + B) e. CC /\ 1 e. CC) -> ((((z - 1) + B) - 1) + 1) = ((z - 1) + B))
115		addcl 6454	. . . . . . . . . . . . . . . . . 18 |- (((z - 1) e. CC /\ B e. CC) -> ((z - 1) + B) e. CC)
116		subcl 6524	. . . . . . . . . . . . . . . . . . 19 |- ((z e. CC /\ 1 e. CC) -> (z - 1) e. CC)
117	8, 116	mpan2 760	. . . . . . . . . . . . . . . . . 18 |- (z e. CC -> (z - 1) e. CC)
118	115, 117	sylan 497	. . . . . . . . . . . . . . . . 17 |- ((z e. CC /\ B e. CC) -> ((z - 1) + B) e. CC)
119	114, 118, 8	sylancl 525	. . . . . . . . . . . . . . . 16 |- ((z e. CC /\ B e. CC) -> ((((z - 1) + B) - 1) + 1) = ((z - 1) + B))
120		zcn 7349	. . . . . . . . . . . . . . . 16 |- (z e. ZZ -> z e. CC)
121	119, 120, 32	syl2an 503	. . . . . . . . . . . . . . 15 |- ((z e. ZZ /\ B e. ZZ) -> ((((z - 1) + B) - 1) + 1) = ((z - 1) + B))
122	121	ex 402	. . . . . . . . . . . . . 14 |- (z e. ZZ -> (B e. ZZ -> ((((z - 1) + B) - 1) + 1) = ((z - 1) + B)))
123	122	adantld 426	. . . . . . . . . . . . 13 |- (z e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> ((((z - 1) + B) - 1) + 1) = ((z - 1) + B)))
124		dfsbcq 2455	. . . . . . . . . . . . 13 |- (((((z - 1) + B) - 1) + 1) = ((z - 1) + B) -> ([((((z - 1) + B) - 1) + 1) / x]ph <-> [((z - 1) + B) / x]ph))
125	123, 124	syl6 25	. . . . . . . . . . . 12 |- (z e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> ([((((z - 1) + B) - 1) + 1) / x]ph <-> [((z - 1) + B) / x]ph)))
126	125	pm5.74d 645	. . . . . . . . . . 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)))
127	126	pm5.74i 644	. . . . . . . . . 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)))
128	113, 127	syl5bbr 593	. . . . . . . . 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))))
129		eleq1 1957	. . . . . . . . . 10 |- (z = ((A - B) + 1) -> (z e. ZZ <-> ((A - B) + 1) e. ZZ))
130		ax-17 1317	. . . . . . . . . . . . . 14 |- ((z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ)) -> A.x(z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ)))
131		ax-17 1317	. . . . . . . . . . . . . . 15 |- (ta -> A.xta)
132	23, 131	hbbi 1357	. . . . . . . . . . . . . 14 |- (([((z - 1) + B) / x]ph <-> ta) -> A.x([((z - 1) + B) / x]ph <-> ta))
133	130, 132	hbim 1354	. . . . . . . . . . . . 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)))
134	27	adantr 425	. . . . . . . . . . . . . . 15 |- ((x = ((z - 1) + B) /\ (z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ))) -> (ph <-> [((z - 1) + B) / x]ph))
135		eqtr 1904	. . . . . . . . . . . . . . . . . . 19 |- ((x = ((z - 1) + B) /\ ((z - 1) + B) = ((((A - B) + 1) - 1) + B)) -> x = ((((A - B) + 1) - 1) + B))
136		opreq1 4889	. . . . . . . . . . . . . . . . . . . 20 |- (z = ((A - B) + 1) -> (z - 1) = (((A - B) + 1) - 1))
137	136	opreq1d 4897	. . . . . . . . . . . . . . . . . . 19 |- (z = ((A - B) + 1) -> ((z - 1) + B) = ((((A - B) + 1) - 1) + B))
138	135, 137	sylan2 500	. . . . . . . . . . . . . . . . . 18 |- ((x = ((z - 1) + B) /\ z = ((A - B) + 1)) -> x = ((((A - B) + 1) - 1) + B))
139		subcl 6524	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. CC /\ B e. CC) -> (A - B) e. CC)
140	8	a1i 8	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. CC /\ B e. CC) -> 1 e. CC)
141		simpr 350	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. CC /\ B e. CC) -> B e. CC)
142		add23 6490	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((A - B) e. CC /\ 1 e. CC /\ B e. CC) -> (((A - B) + 1) + B) = (((A - B) + B) + 1))
143	139, 140, 141, 142	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. CC /\ B e. CC) -> (((A - B) + 1) + B) = (((A - B) + B) + 1))
144		npcan 6559	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. CC /\ B e. CC) -> ((A - B) + B) = A)
145	144	opreq1d 4897	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. CC /\ B e. CC) -> (((A - B) + B) + 1) = (A + 1))
146	143, 145	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. CC /\ B e. CC) -> (((A - B) + 1) + B) = (A + 1))
147	146	opreq1d 4897	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. CC /\ B e. CC) -> ((((A - B) + 1) + B) - 1) = ((A + 1) - 1))
148		peano2cn 6498	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A - B) e. CC -> ((A - B) + 1) e. CC)
149	139, 148	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. CC /\ B e. CC) -> ((A - B) + 1) e. CC)
150		addsub 6542	. . . . . . . . . . . . . . . . . . . . 21 |- ((((A - B) + 1) e. CC /\ B e. CC /\ 1 e. CC) -> ((((A - B) + 1) + B) - 1) = ((((A - B) + 1) - 1) + B))
151	149, 141, 140, 150	syl111anc 1100	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. CC /\ B e. CC) -> ((((A - B) + 1) + B) - 1) = ((((A - B) + 1) - 1) + B))
152		pncan 6557	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. CC /\ 1 e. CC) -> ((A + 1) - 1) = A)
153	8, 152	mpan2 760	. . . . . . . . . . . . . . . . . . . . 21 |- (A e. CC -> ((A + 1) - 1) = A)
154	153	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. CC /\ B e. CC) -> ((A + 1) - 1) = A)
155	147, 151, 154	3eqtr3d 1934	. . . . . . . . . . . . . . . . . . 19 |- ((A e. CC /\ B e. CC) -> ((((A - B) + 1) - 1) + B) = A)
156		zcn 7349	. . . . . . . . . . . . . . . . . . 19 |- (A e. ZZ -> A e. CC)
157	155, 156, 32	syl2an 503	. . . . . . . . . . . . . . . . . 18 |- ((A e. ZZ /\ B e. ZZ) -> ((((A - B) + 1) - 1) + B) = A)
158	138, 157	sylan9eq 1948	. . . . . . . . . . . . . . . . 17 |- (((x = ((z - 1) + B) /\ z = ((A - B) + 1)) /\ (A e. ZZ /\ B e. ZZ)) -> x = A)
159	158	anasss 488	. . . . . . . . . . . . . . . 16 |- ((x = ((z - 1) + B) /\ (z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ))) -> x = A)
160		uzindOLD.4	. . . . . . . . . . . . . . . 16 |- (x = A -> (ph <-> ta))
161	159, 160	syl 12	. . . . . . . . . . . . . . 15 |- ((x = ((z - 1) + B) /\ (z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ))) -> (ph <-> ta))
162	134, 161	bitr3d 589	. . . . . . . . . . . . . 14 |- ((x = ((z - 1) + B) /\ (z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ))) -> ([((z - 1) + B) / x]ph <-> ta))
163	162	ex 402	. . . . . . . . . . . . 13 |- (x = ((z - 1) + B) -> ((z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ)) -> ([((z - 1) + B) / x]ph <-> ta)))
164	133, 163	19.23ai 1412	. . . . . . . . . . . 12 |- (E.x x = ((z - 1) + B) -> ((z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ)) -> ([((z - 1) + B) / x]ph <-> ta)))
165	21, 164	ax-mp 7	. . . . . . . . . . 11 |- ((z = ((A - B) + 1) /\ (A e. ZZ /\ B e. ZZ)) -> ([((z - 1) + B) / x]ph <-> ta))
166	165	pm5.74da 646	. . . . . . . . . 10 |- (z = ((A - B) + 1) -> (((A e. ZZ /\ B e. ZZ) -> [((z - 1) + B) / x]ph) <-> ((A e. ZZ /\ B e. ZZ) -> ta)))
167	129, 166	imbi12d 688	. . . . . . . . 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))))
168		uzindOLD.5	. . . . . . . . . 10 |- ps
169	168	a1i12 9	. . . . . . . . 9 |- (1 e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> ps))
170		nnz 7362	. . . . . . . . . . 11 |- (w e. NN -> w e. ZZ)
171	170	a1d 15	. . . . . . . . . 10 |- (w e. NN -> ((w + 1) e. ZZ -> w e. ZZ))
172		ax-17 1317	. . . . . . . . . . . . . . . . 17 |- ((w e. NN /\ B e. ZZ) -> A.y(w e. NN /\ B e. ZZ))
173	51	hbsbc1v 2464	. . . . . . . . . . . . . . . . . 18 |- ([((w - 1) + B) / y]th -> A.y[((w - 1) + B) / y]th)
174	60, 173	hbim 1354	. . . . . . . . . . . . . . . . 17 |- (([((w - 1) + B) / y]ch -> [((w - 1) + B) / y]th) -> A.y([((w - 1) + B) / y]ch -> [((w - 1) + B) / y]th))
175	172, 174	hbim 1354	. . . . . . . . . . . . . . . 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)))
176		uzindOLD.6	. . . . . . . . . . . . . . . . 17 |- (((y e. ZZ /\ B e. ZZ) /\ B <_ y) -> (ch -> th))
177		eleq1 1957	. . . . . . . . . . . . . . . . . . . . 21 |- (y = ((w - 1) + B) -> (y e. ZZ <-> ((w - 1) + B) e. ZZ))
178	177	anbi1d 679	. . . . . . . . . . . . . . . . . . . 20 |- (y = ((w - 1) + B) -> ((y e. ZZ /\ B e. ZZ) <-> (((w - 1) + B) e. ZZ /\ B e. ZZ)))
179		breq2 3342	. . . . . . . . . . . . . . . . . . . 20 |- (y = ((w - 1) + B) -> (B <_ y <-> B <_ ((w - 1) + B)))
180	178, 179	anbi12d 690	. . . . . . . . . . . . . . . . . . 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))))
181		zaddcl 7374	. . . . . . . . . . . . . . . . . . . . . 22 |- (((w - 1) e. ZZ /\ B e. ZZ) -> ((w - 1) + B) e. ZZ)
182		peano2zm 7378	. . . . . . . . . . . . . . . . . . . . . 22 |- (w e. ZZ -> (w - 1) e. ZZ)
183	181, 182	sylan 497	. . . . . . . . . . . . . . . . . . . . 21 |- ((w e. ZZ /\ B e. ZZ) -> ((w - 1) + B) e. ZZ)
184	183, 170	sylan 497	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. NN /\ B e. ZZ) -> ((w - 1) + B) e. ZZ)
185		simpr 350	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. NN /\ B e. ZZ) -> B e. ZZ)
186		simpr 350	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. RR /\ B e. RR) -> B e. RR)
187		readdcl 6455	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((w - 1) e. RR /\ B e. RR) -> ((w - 1) + B) e. RR)
188		peano2rem 6605	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w e. RR -> (w - 1) e. RR)
189	187, 188	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. RR /\ B e. RR) -> ((w - 1) + B) e. RR)
190		peano2rem 6605	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (B e. RR -> (B - 1) e. RR)
191	190	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. RR /\ B e. RR) -> (B - 1) e. RR)
192		lesub1 6849	. . . . . . . . . . . . . . . . . . . . . . . . . 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))))
193	186, 189, 191, 192	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((w e. RR /\ B e. RR) -> (B <_ ((w - 1) + B) <-> (B - (B - 1)) <_ (((w - 1) + B) - (B - 1))))
194		subsub 6627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((B e. CC /\ B e. CC /\ 1 e. CC) -> (B - (B - 1)) = ((B - B) + 1))
195	8, 194	mp3an3 1180	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((B e. CC /\ B e. CC) -> (B - (B - 1)) = ((B - B) + 1))
196	195	anidms 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (B e. CC -> (B - (B - 1)) = ((B - B) + 1))
197		subid 6555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (B e. CC -> (B - B) = 0)
198	197	opreq1d 4897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (B e. CC -> ((B - B) + 1) = (0 + 1))
199	198, 9	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (B e. CC -> ((B - B) + 1) = 1)
200	196, 199	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (B e. CC -> (B - (B - 1)) = 1)
201	200	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((w e. CC /\ B e. CC) -> (B - (B - 1)) = 1)
202		addcl 6454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((w - 1) e. CC /\ B e. CC) -> ((w - 1) + B) e. CC)
203		subcl 6524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((w e. CC /\ 1 e. CC) -> (w - 1) e. CC)
204	8, 203	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (w e. CC -> (w - 1) e. CC)
205	202, 204	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((w e. CC /\ B e. CC) -> ((w - 1) + B) e. CC)
206		subsub 6627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((w - 1) + B) e. CC /\ B e. CC /\ 1 e. CC) -> (((w - 1) + B) - (B - 1)) = ((((w - 1) + B) - B) + 1))
207	8, 206	mp3an3 1180	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((w - 1) + B) e. CC /\ B e. CC) -> (((w - 1) + B) - (B - 1)) = ((((w - 1) + B) - B) + 1))
208	205, 207	sylancom 531	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((w e. CC /\ B e. CC) -> (((w - 1) + B) - (B - 1)) = ((((w - 1) + B) - B) + 1))
209		pncan 6557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((w - 1) e. CC /\ B e. CC) -> (((w - 1) + B) - B) = (w - 1))
210	209, 204	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((w e. CC /\ B e. CC) -> (((w - 1) + B) - B) = (w - 1))
211	210	opreq1d 4897	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((w e. CC /\ B e. CC) -> ((((w - 1) + B) - B) + 1) = ((w - 1) + 1))
212		npcan 6559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((w e. CC /\ 1 e. CC) -> ((w - 1) + 1) = w)
213	8, 212	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w e. CC -> ((w - 1) + 1) = w)
214	213	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((w e. CC /\ B e. CC) -> ((w - 1) + 1) = w)
215	208, 211, 214	3eqtrd 1929	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((w e. CC /\ B e. CC) -> (((w - 1) + B) - (B - 1)) = w)
216	201, 215	breq12d 3351	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. CC /\ B e. CC) -> ((B - (B - 1)) <_ (((w - 1) + B) - (B - 1)) <-> 1 <_ w))
217		recn 6466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w e. RR -> w e. CC)
218		recn 6466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (B e. RR -> B e. CC)
219	216, 217, 218	syl2an 503	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((w e. RR /\ B e. RR) -> ((B - (B - 1)) <_ (((w - 1) + B) - (B - 1)) <-> 1 <_ w))
220	193, 219	bitrd 587	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((w e. RR /\ B e. RR) -> (B <_ ((w - 1) + B) <-> 1 <_ w))
221		zre 7348	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w e. ZZ -> w e. RR)
222	220, 221, 14	syl2an 503	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((w e. ZZ /\ B e. ZZ) -> (B <_ ((w - 1) + B) <-> 1 <_ w))
223	222	biimpar 461	. . . . . . . . . . . . . . . . . . . . . 22 |- (((w e. ZZ /\ B e. ZZ) /\ 1 <_ w) -> B <_ ((w - 1) + B))
224	223	an1rs 547	. . . . . . . . . . . . . . . . . . . . 21 |- (((w e. ZZ /\ 1 <_ w) /\ B e. ZZ) -> B <_ ((w - 1) + B))
225		elnnz1 7364	. . . . . . . . . . . . . . . . . . . . 21 |- (w e. NN <-> (w e. ZZ /\ 1 <_ w))
226	224, 225	sylanb 498	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. NN /\ B e. ZZ) -> B <_ ((w - 1) + B))
227	184, 185, 226	jca31 311	. . . . . . . . . . . . . . . . . . 19 |- ((w e. NN /\ B e. ZZ) -> ((((w - 1) + B) e. ZZ /\ B e. ZZ) /\ B <_ ((w - 1) + B)))
228	180, 227	syl5bir 227	. . . . . . . . . . . . . . . . . 18 |- (y = ((w - 1) + B) -> ((w e. NN /\ B e. ZZ) -> ((y e. ZZ /\ B e. ZZ) /\ B <_ y)))
229		sbceq1a 2456	. . . . . . . . . . . . . . . . . . . 20 |- (y = ((w - 1) + B) -> (th <-> [((w - 1) + B) / y]th))
230	69, 229	imbi12d 688	. . . . . . . . . . . . . . . . . . 19 |- (y = ((w - 1) + B) -> ((ch -> th) <-> ([((w - 1) + B) / y]ch -> [((w - 1) + B) / y]th)))
231	230	biimpd 170	. . . . . . . . . . . . . . . . . 18 |- (y = ((w - 1) + B) -> ((ch -> th) -> ([((w - 1) + B) / y]ch -> [((w - 1) + B) / y]th)))
232	228, 231	imim12d 69	. . . . . . . . . . . . . . . . 17 |- (y = ((w - 1) + B) -> ((((y e. ZZ /\ B e. ZZ) /\ B <_ y) -> (ch -> th)) -> ((w e. NN /\ B e. ZZ) -> ([((w - 1) + B) / y]ch -> [((w - 1) + B) / y]th))))
233	176, 232	mpi 55	. . . . . . . . . . . . . . . 16 |- (y = ((w - 1) + B) -> ((w e. NN /\ B e. ZZ) -> ([((w - 1) + B) / y]ch -> [((w - 1) + B) / y]th)))
234	175, 233	19.23ai 1412	. . . . . . . . . . . . . . 15 |- (E.y y = ((w - 1) + B) -> ((w e. NN /\ B e. ZZ) -> ([((w - 1) + B) / y]ch -> [((w - 1) + B) / y]th)))
235	52, 234	ax-mp 7	. . . . . . . . . . . . . 14 |- ((w e. NN /\ B e. ZZ) -> ([((w - 1) + B) / y]ch -> [((w - 1) + B) / y]th))
236		addsub 6542	. . . . . . . . . . . . . . . . . . 19 |- ((((w + 1) - 1) e. CC /\ B e. CC /\ 1 e. CC) -> ((((w + 1) - 1) + B) - 1) = ((((w + 1) - 1) - 1) + B))
237	8, 236	mp3an3 1180	. . . . . . . . . . . . . . . . . 18 |- ((((w + 1) - 1) e. CC /\ B e. CC) -> ((((w + 1) - 1) + B) - 1) = ((((w + 1) - 1) - 1) + B))
238		subcl 6524	. . . . . . . . . . . . . . . . . . 19 |- (((w + 1) e. CC /\ 1 e. CC) -> ((w + 1) - 1) e. CC)
239		peano2cn 6498	. . . . . . . . . . . . . . . . . . 19 |- (w e. CC -> (w + 1) e. CC)
240	238, 239, 8	sylancl 525	. . . . . . . . . . . . . . . . . 18 |- (w e. CC -> ((w + 1) - 1) e. CC)
241	237, 240	sylan 497	. . . . . . . . . . . . . . . . 17 |- ((w e. CC /\ B e. CC) -> ((((w + 1) - 1) + B) - 1) = ((((w + 1) - 1) - 1) + B))
242		pncan 6557	. . . . . . . . . . . . . . . . . . . . 21 |- ((w e. CC /\ 1 e. CC) -> ((w + 1) - 1) = w)
243	8, 242	mpan2 760	. . . . . . . . . . . . . . . . . . . 20 |- (w e. CC -> ((w + 1) - 1) = w)
244	243	opreq1d 4897	. . . . . . . . . . . . . . . . . . 19 |- (w e. CC -> (((w + 1) - 1) - 1) = (w - 1))
245	244	opreq1d 4897	. . . . . . . . . . . . . . . . . 18 |- (w e. CC -> ((((w + 1) - 1) - 1) + B) = ((w - 1) + B))
246	245	adantr 425	. . . . . . . . . . . . . . . . 17 |- ((w e. CC /\ B e. CC) -> ((((w + 1) - 1) - 1) + B) = ((w - 1) + B))
247	241, 246	eqtrd 1925	. . . . . . . . . . . . . . . 16 |- ((w e. CC /\ B e. CC) -> ((((w + 1) - 1) + B) - 1) = ((w - 1) + B))
248		nncn 7113	. . . . . . . . . . . . . . . 16 |- (w e. NN -> w e. CC)
249	247, 248, 32	syl2an 503	. . . . . . . . . . . . . . 15 |- ((w e. NN /\ B e. ZZ) -> ((((w + 1) - 1) + B) - 1) = ((w - 1) + B))
250		dfsbcq 2455	. . . . . . . . . . . . . . 15 |- (((((w + 1) - 1) + B) - 1) = ((w - 1) + B) -> ([((((w + 1) - 1) + B) - 1) / y]th <-> [((w - 1) + B) / y]th))
251	249, 250	syl 12	. . . . . . . . . . . . . 14 |- ((w e. NN /\ B e. ZZ) -> ([((((w + 1) - 1) + B) - 1) / y]th <-> [((w - 1) + B) / y]th))
252	235, 251	sylibrd 221	. . . . . . . . . . . . 13 |- ((w e. NN /\ B e. ZZ) -> ([((w - 1) + B) / y]ch -> [((((w + 1) - 1) + B) - 1) / y]th))
253	252	ex 402	. . . . . . . . . . . 12 |- (w e. NN -> (B e. ZZ -> ([((w - 1) + B) / y]ch -> [((((w + 1) - 1) + B) - 1) / y]th)))
254	253	adantld 426	. . . . . . . . . . 11 |- (w e. NN -> ((A e. ZZ /\ B e. ZZ) -> ([((w - 1) + B) / y]ch -> [((((w + 1) - 1) + B) - 1) / y]th)))
255	254	a2d 16	. . . . . . . . . 10 |- (w e. NN -> (((A e. ZZ /\ B e. ZZ) -> [((w - 1) + B) / y]ch) -> ((A e. ZZ /\ B e. ZZ) -> [((((w + 1) - 1) + B) - 1) / y]th)))
256	171, 255	imim12d 69	. . . . . . . . 9 |- (w e. NN -> ((w e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> [((w - 1) + B) / y]ch)) -> ((w + 1) e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> [((((w + 1) - 1) + B) - 1) / y]th))))
257	49, 77, 128, 167, 169, 256	nnind 7120	. . . . . . . 8 |- (((A - B) + 1) e. NN -> (((A - B) + 1) e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> ta)))
258	18, 257	sylbir 218	. . . . . . 7 |- ((((A - B) + 1) e. ZZ /\ 1 <_ ((A - B) + 1)) -> (((A - B) + 1) e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> ta)))
259	258	ex 402	. . . . . 6 |- (((A - B) + 1) e. ZZ -> (1 <_ ((A - B) + 1) -> (((A - B) + 1) e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> ta))))
260	259	pm2.43a 80	. . . . 5 |- (((A - B) + 1) e. ZZ -> (1 <_ ((A - B) + 1) -> ((A e. ZZ /\ B e. ZZ) -> ta)))
261	260	com23 36	. . . 4 |- (((A - B) + 1) e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> (1 <_ ((A - B) + 1) -> ta)))
262	17, 261	mpcom 60	. . 3 |- ((A e. ZZ /\ B e. ZZ) -> (1 <_ ((A - B) + 1) -> ta))
263	15, 262	sylbid 220	. 2 |- ((A e. ZZ /\ B e. ZZ) -> (B <_ A -> ta))
264	263	imp 377	1 |- (((A e. ZZ /\ B e. ZZ) /\ B <_ A) -> ta)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  [wsbc 1534   class class class wbr 3338  (class class class)co 4884  CCcc 6384  RRcr 6385  0cc0 6386  1c1 6387   + caddc 6389   - cmin 6445   <_ cle 6448  NNcn 6449  ZZcz 6451

This theorem is referenced by:  uzind3OLD 7421

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-n 7108  df-n0 7309  df-z 7345

Copyright terms: Public domain