Theorem uzind 4603

Description: Induction on the upper partition of ZZ that starts 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
uzind.1	|- (x = B -> (ph <-> ps))
uzind.2	|- (x = y -> (ph <-> ch))
uzind.3	|- (x = (y + 1) -> (ph <-> th))
uzind.4	|- (x = A -> (ph <-> ta ))
uzind.5	|- ps
uzind.6	|- (((y e. ZZ /\ B e. ZZ) /\ B <_ y) -> (ch -> th))

Assertion

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

Distinct variable group(s):   x,A   ps,x   ch,x   th,x   ta ,x   ph,y   x,y,B

Proof of Theorem uzind

Step	Hyp	Ref	Expression
1		leadd2t 4351	. . . . . 6 |- ((1 e. RR /\ ((A - B) + 1) e. RR /\ (B - 1) e. RR) -> (1 <_ ((A - B) + 1) <-> ((B - 1) + 1) <_ ((B - 1) + ((A - B) + 1))))
2		ax1re 4064	. . . . . . 7 |- 1 e. RR
3	2	a1i 7	. . . . . 6 |- ((A e. RR /\ B e. RR) -> 1 e. RR)
4		resubclt 4173	. . . . . . . 8 |- ((A e. RR /\ B e. RR) -> (A - B) e. RR)
5	4, 2	jctir 241	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> ((A - B) e. RR /\ 1 e. RR))
6		axaddrcl 4067	. . . . . . 7 |- (((A - B) e. RR /\ 1 e. RR) -> ((A - B) + 1) e. RR)
7	5, 6	syl 12	. . . . . 6 |- ((A e. RR /\ B e. RR) -> ((A - B) + 1) e. RR)
8		resubclt 4173	. . . . . . . 8 |- ((B e. RR /\ 1 e. RR) -> (B - 1) e. RR)
9	2, 8	mpan2 519	. . . . . . 7 |- (B e. RR -> (B - 1) e. RR)
10	9	adantl 305	. . . . . 6 |- ((A e. RR /\ B e. RR) -> (B - 1) e. RR)
11	1, 3, 7, 10	syl3anc 629	. . . . 5 |- ((A e. RR /\ B e. RR) -> (1 <_ ((A - B) + 1) <-> ((B - 1) + 1) <_ ((B - 1) + ((A - B) + 1))))
12		1cn 4101	. . . . . . . . 9 |- 1 e. CC
13		npcant 4162	. . . . . . . . 9 |- ((B e. CC /\ 1 e. CC) -> ((B - 1) + 1) = B)
14	12, 13	mpan2 519	. . . . . . . 8 |- (B e. CC -> ((B - 1) + 1) = B)
15	14	adantl 305	. . . . . . 7 |- ((A e. CC /\ B e. CC) -> ((B - 1) + 1) = B)
16		add12t 4125	. . . . . . . . 9 |- (((B - 1) e. CC /\ (A - B) e. CC /\ 1 e. CC) -> ((B - 1) + ((A - B) + 1)) = ((A - B) + ((B - 1) + 1)))
17		subclt 4140	. . . . . . . . . . 11 |- ((B e. CC /\ 1 e. CC) -> (B - 1) e. CC)
18	12, 17	mpan2 519	. . . . . . . . . 10 |- (B e. CC -> (B - 1) e. CC)
19	18	adantl 305	. . . . . . . . 9 |- ((A e. CC /\ B e. CC) -> (B - 1) e. CC)
20		subclt 4140	. . . . . . . . 9 |- ((A e. CC /\ B e. CC) -> (A - B) e. CC)
21	12	a1i 7	. . . . . . . . 9 |- ((A e. CC /\ B e. CC) -> 1 e. CC)
22	16, 19, 20, 21	syl3anc 629	. . . . . . . 8 |- ((A e. CC /\ B e. CC) -> ((B - 1) + ((A - B) + 1)) = ((A - B) + ((B - 1) + 1)))
23	14	opreq2d 3013	. . . . . . . . 9 |- (B e. CC -> ((A - B) + ((B - 1) + 1)) = ((A - B) + B))
24	23	adantl 305	. . . . . . . 8 |- ((A e. CC /\ B e. CC) -> ((A - B) + ((B - 1) + 1)) = ((A - B) + B))
25		npcant 4162	. . . . . . . 8 |- ((A e. CC /\ B e. CC) -> ((A - B) + B) = A)
26	22, 24, 25	3eqtrd 1132	. . . . . . 7 |- ((A e. CC /\ B e. CC) -> ((B - 1) + ((A - B) + 1)) = A)
27	15, 26	breq12d 2073	. . . . . 6 |- ((A e. CC /\ B e. CC) -> (((B - 1) + 1) <_ ((B - 1) + ((A - B) + 1)) <-> B <_ A))
28		recnt 4097	. . . . . 6 |- (A e. RR -> A e. CC)
29		recnt 4097	. . . . . 6 |- (B e. RR -> B e. CC)
30	27, 28, 29	syl2an 349	. . . . 5 |- ((A e. RR /\ B e. RR) -> (((B - 1) + 1) <_ ((B - 1) + ((A - B) + 1)) <-> B <_ A))
31	11, 30	bitr2d 407	. . . 4 |- ((A e. RR /\ B e. RR) -> (B <_ A <-> 1 <_ ((A - B) + 1)))
32		zret 4567	. . . 4 |- (A e. ZZ -> A e. RR)
33		zret 4567	. . . 4 |- (B e. ZZ -> B e. RR)
34	31, 32, 33	syl2an 349	. . 3 |- ((A e. ZZ /\ B e. ZZ) -> (B <_ A <-> 1 <_ ((A - B) + 1)))
35		zsubclt 4591	. . . . 5 |- ((A e. ZZ /\ B e. ZZ) -> (A - B) e. ZZ)
36		1z 4584	. . . . . 6 |- 1 e. ZZ
37		zaddclt 4590	. . . . . 6 |- (((A - B) e. ZZ /\ 1 e. ZZ) -> ((A - B) + 1) e. ZZ)
38	36, 37	mpan2 519	. . . . 5 |- ((A - B) e. ZZ -> ((A - B) + 1) e. ZZ)
39	35, 38	syl 12	. . . 4 |- ((A e. ZZ /\ B e. ZZ) -> ((A - B) + 1) e. ZZ)
40		elnnz1 4581	. . . . . . . 8 |- (((A - B) + 1) e. NN <-> (((A - B) + 1) e. ZZ /\ 1 <_ ((A - B) + 1)))
41		eleq1 1149	. . . . . . . . . 10 |- (z = 1 -> (z e. ZZ <-> 1 e. ZZ))
42		oprex 3018	. . . . . . . . . . . . . . 15 |- ((z - 1) + B) e. V
43	42	isseti 1352	. . . . . . . . . . . . . 14 |- E.x x = ((z - 1) + B)
44		ax-17 925	. . . . . . . . . . . . . . . 16 |- ((z = 1 /\ B e. ZZ) -> A.x(z = 1 /\ B e. ZZ))
45	42	hbsbcv 1447	. . . . . . . . . . . . . . . . 17 |- ([((z - 1) + B) / x]ph -> A.x[((z - 1) + B) / x]ph)
46		ax-17 925	. . . . . . . . . . . . . . . . 17 |- (ps -> A.xps)
47	45, 46	hbbi 705	. . . . . . . . . . . . . . . 16 |- (([((z - 1) + B) / x]ph <-> ps) -> A.x([((z - 1) + B) / x]ph <-> ps))
48	44, 47	hbim 702	. . . . . . . . . . . . . . 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)))
49		sbceq1 1443	. . . . . . . . . . . . . . . . . 18 |- (x = ((z - 1) + B) -> (ph <-> [((z - 1) + B) / x]ph))
50	49	adantr 306	. . . . . . . . . . . . . . . . 17 |- ((x = ((z - 1) + B) /\ (z = 1 /\ B e. ZZ)) -> (ph <-> [((z - 1) + B) / x]ph))
51		cleqtr 1118	. . . . . . . . . . . . . . . . . . 19 |- ((x = ((z - 1) + B) /\ ((z - 1) + B) = B) -> x = B)
52		opreq1 3006	. . . . . . . . . . . . . . . . . . . . 21 |- (z = 1 -> (z - 1) = (1 - 1))
53	52	opreq1d 3012	. . . . . . . . . . . . . . . . . . . 20 |- (z = 1 -> ((z - 1) + B) = ((1 - 1) + B))
54		zcnt 4568	. . . . . . . . . . . . . . . . . . . . . 22 |- (B e. ZZ -> B e. CC)
55		addid2t 4132	. . . . . . . . . . . . . . . . . . . . . 22 |- (B e. CC -> (0 + B) = B)
56	54, 55	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (B e. ZZ -> (0 + B) = B)
57	12	subid 4155	. . . . . . . . . . . . . . . . . . . . . 22 |- (1 - 1) = 0
58	57	opreq1i 3009	. . . . . . . . . . . . . . . . . . . . 21 |- ((1 - 1) + B) = (0 + B)
59	56, 58	syl5eq 1136	. . . . . . . . . . . . . . . . . . . 20 |- (B e. ZZ -> ((1 - 1) + B) = B)
60	53, 59	sylan9eq 1144	. . . . . . . . . . . . . . . . . . 19 |- ((z = 1 /\ B e. ZZ) -> ((z - 1) + B) = B)
61	51, 60	sylan2 346	. . . . . . . . . . . . . . . . . 18 |- ((x = ((z - 1) + B) /\ (z = 1 /\ B e. ZZ)) -> x = B)
62		uzind.1	. . . . . . . . . . . . . . . . . 18 |- (x = B -> (ph <-> ps))
63	61, 62	syl 12	. . . . . . . . . . . . . . . . 17 |- ((x = ((z - 1) + B) /\ (z = 1 /\ B e. ZZ)) -> (ph <-> ps))
64	50, 63	bitr3d 408	. . . . . . . . . . . . . . . 16 |- ((x = ((z - 1) + B) /\ (z = 1 /\ B e. ZZ)) -> ([((z - 1) + B) / x]ph <-> ps))
65	64	exp 291	. . . . . . . . . . . . . . 15 |- (x = ((z - 1) + B) -> ((z = 1 /\ B e. ZZ) -> ([((z - 1) + B) / x]ph <-> ps)))
66	48, 65	19.23ai 746	. . . . . . . . . . . . . 14 |- (E.x x = ((z - 1) + B) -> ((z = 1 /\ B e. ZZ) -> ([((z - 1) + B) / x]ph <-> ps)))
67	43, 66	ax-mp 6	. . . . . . . . . . . . 13 |- ((z = 1 /\ B e. ZZ) -> ([((z - 1) + B) / x]ph <-> ps))
68	67	exp 291	. . . . . . . . . . . 12 |- (z = 1 -> (B e. ZZ -> ([((z - 1) + B) / x]ph <-> ps)))
69	68	adantld 307	. . . . . . . . . . 11 |- (z = 1 -> ((A e. ZZ /\ B e. ZZ) -> ([((z - 1) + B) / x]ph <-> ps)))
70	69	pm5.74d 444	. . . . . . . . . 10 |- (z = 1 -> (((A e. ZZ /\ B e. ZZ) -> [((z - 1) + B) / x]ph) <-> ((A e. ZZ /\ B e. ZZ) -> ps)))
71	41, 70	imbi12d 474	. . . . . . . . 9 |- (z = 1 -> ((z e. ZZ -> ((A e. ZZ /\ B e. ZZ) -> [((z - 1) + B) / x]ph)) <-> (1 e. ZZ -> ((