Theorem climcmplem 7081

Description: Lemma for climcmp 7082.

Hypotheses

Ref	Expression
climcmplem.1	|- F e. V
climcmplem.2	|- G e. V
climcmplem.3	|- A e. V
climcmplem.4	|- B e. V
climcmplem.5	|- H = {<.j, y>. | (j e. (ZZ>` M) /\ y = ((G` j) - (F` j)))}
climcmplem.6	|- (ph <-> ((F` k) e. RR /\ (G` k) e. RR /\ (F` k) <_ (G` k)))
climcmplem.7	|- (ps <-> (H` k) = ((G` k) - (F` k)))
climcmplem.8	|- (ch <-> (F ~~> A /\ G ~~> B))

Assertion

Ref	Expression
climcmplem	|- ((ch /\ (M e. ZZ /\ A.k e. (ZZ>` M)ph)) -> A <_ B)

Distinct variable groups:   j,F,k,y   j,G,k,y   k,H   j,M,k,y

Proof of Theorem climcmplem

Step	Hyp	Ref	Expression
1		fveq2 3715	. . . . . . . . . . . . . . . 16 |- (j = k -> (G` j) = (G` k))
2		fveq2 3715	. . . . . . . . . . . . . . . 16 |- (j = k -> (F` j) = (F` k))
3	1, 2	opreq12d 3969	. . . . . . . . . . . . . . 15 |- (j = k -> ((G` j) - (F` j)) = ((G` k) - (F` k)))
4		climcmplem.5	. . . . . . . . . . . . . . 15 |- H = {<.j, y>. | (j e. (ZZ>` M) /\ y = ((G` j) - (F` j)))}
5		oprex 3974	. . . . . . . . . . . . . . 15 |- ((G` k) - (F` k)) e. V
6	3, 4, 5	fvopab4 3771	. . . . . . . . . . . . . 14 |- (k e. (ZZ>` M) -> (H` k) = ((G` k) - (F` k)))
7		climcmplem.7	. . . . . . . . . . . . . 14 |- (ps <-> (H` k) = ((G` k) - (F` k)))
8	6, 7	sylibr 200	. . . . . . . . . . . . 13 |- (k e. (ZZ>` M) -> ps)
9	8	a1d 12	. . . . . . . . . . . 12 |- (k e. (ZZ>` M) -> (ph -> ps))
10	9	ancld 298	. . . . . . . . . . 11 |- (k e. (ZZ>` M) -> (ph -> (ph /\ ps)))
11	10	r19.20i 1701	. . . . . . . . . 10 |- (A.k e. (ZZ>` M)ph -> A.k e. (ZZ>` M)(ph /\ ps))
12		recnt 5293	. . . . . . . . . . . . . . 15 |- ((G` k) e. RR -> (G` k) e. CC)
13		recnt 5293	. . . . . . . . . . . . . . 15 |- ((F` k) e. RR -> (F` k) e. CC)
14	12, 13	anim12i 333	. . . . . . . . . . . . . 14 |- (((G` k) e. RR /\ (F` k) e. RR) -> ((G` k) e. CC /\ (F` k) e. CC))
15		climcmplem.6	. . . . . . . . . . . . . . 15 |- (ph <-> ((F` k) e. RR /\ (G` k) e. RR /\ (F` k) <_ (G` k)))
16		3simp2 788	. . . . . . . . . . . . . . 15 |- (((F` k) e. RR /\ (G` k) e. RR /\ (F` k) <_ (G` k)) -> (G` k) e. RR)
17	15, 16	sylbi 199	. . . . . . . . . . . . . 14 |- (ph -> (G` k) e. RR)
18		3simp1 787	. . . . . . . . . . . . . . 15 |- (((F` k) e. RR /\ (G` k) e. RR /\ (F` k) <_ (G` k)) -> (F` k) e. RR)
19	15, 18	sylbi 199	. . . . . . . . . . . . . 14 |- (ph -> (F` k) e. RR)
20	14, 17, 19	sylanc 471	. . . . . . . . . . . . 13 |- (ph -> ((G` k) e. CC /\ (F` k) e. CC))
21	20	anim1i 334	. . . . . . . . . . . 12 |- ((ph /\ (H` k) = ((G` k) - (F` k))) -> (((G` k) e. CC /\ (F` k) e. CC) /\ (H` k) = ((G` k) - (F` k))))
22	7	anbi2i 480	. . . . . . . . . . . 12 |- ((ph /\ ps) <-> (ph /\ (H` k) = ((G` k) - (F` k))))
23		df-3an 776	. . . . . . . . . . . 12 |- (((G` k) e. CC /\ (F` k) e. CC /\ (H` k) = ((G` k) - (F` k))) <-> (((G` k) e. CC /\ (F` k) e. CC) /\ (H` k) = ((G` k) - (F` k))))
24	21, 22, 23	3imtr4 219	. . . . . . . . . . 11 |- ((ph /\ ps) -> ((G` k) e. CC /\ (F` k) e. CC /\ (H` k) = ((G` k) - (F` k))))
25	24	r19.20si 1703	. . . . . . . . . 10 |- (A.k e. (ZZ>` M)(ph /\ ps) -> A.k e. (ZZ>` M)((G` k) e. CC /\ (F` k) e. CC /\ (H` k) = ((G` k) - (F` k))))
26	11, 25	syl 10	. . . . . . . . 9 |- (A.k e. (ZZ>` M)ph -> A.k e. (ZZ>` M)((G` k) e. CC /\ (F` k) e. CC /\ (H` k) = ((G` k) - (F` k))))
27	26	anim2i 335	. . . . . . . 8 |- ((M e. ZZ /\ A.k e. (ZZ>` M)ph) -> (M e. ZZ /\ A.k e. (ZZ>` M)((G` k) e. CC /\ (F` k) e. CC /\ (H` k) = ((G` k) - (F` k)))))
28	27	anim2i 335	. . . . . . 7 |- (((F ~~> A /\ G ~~> B) /\ (M e. ZZ /\ A.k e. (ZZ>` M)ph)) -> ((F ~~> A /\ G ~~> B) /\ (M e. ZZ /\ A.k e. (ZZ>` M)((G` k) e. CC /\ (F` k) e. CC /\ (H` k) = ((G` k) - (F` k))))))
29		climcmplem.8	. . . . . . 7 |- (ch <-> (F ~~> A /\ G ~~> B))
30	28, 29	sylanb 449	. . . . . 6 |- ((ch /\ (M e. ZZ /\ A.k e. (ZZ>` M)ph)) -> ((F ~~> A /\ G ~~> B) /\ (M e. ZZ /\ A.k e. (ZZ>` M)((G` k) e. CC /\ (F` k) e. CC /\ (H` k) = ((G` k) - (F` k))))))
31		climcmplem.2	. . . . . . . 8 |- G e. V
32		climcmplem.1	. . . . . . . 8 |- F e. V
33		fvex 3723	. . . . . . . . 9 |- (ZZ>` M) e. V
34	33, 4	fopabex2 3604	. . . . . . . 8 |- H e. V
35		climcmplem.4	. . . . . . . 8 |- B e. V
36		climcmplem.3	. . . . . . . 8 |- A e. V
37	31, 32, 34, 35, 36	climsub 7074	. . . . . . 7 |- (((G ~~> B /\ F ~~> A) /\ (M e. ZZ /\ A.k e. (ZZ>` M)((G` k) e. CC /\ (F` k) e. CC /\ (H` k) = ((G` k) - (F` k))))) -> H ~~> (B - A))
38	37	ancom1s 490	. . . . . 6 |- (((F ~~> A /\ G ~~> B) /\ (M e. ZZ /\ A.k e. (ZZ>` M)((G` k) e. CC /\ (F` k) e. CC /\ (H` k) = ((G` k) - (F` k))))) -> H ~~> (B - A))
39		3ancoma 781	. . . . . . . . 9 |- ((M e. ZZ /\ H ~~> (B - A) /\ A.k e. (ZZ>` M)ph) <-> (H ~~> (B - A) /\ M e. ZZ /\ A.k e. (ZZ>` M)ph))
40		df-3an 776	. . . . . . . . 9 |- ((M e. ZZ /\ H ~~> (B - A) /\ A.k e. (ZZ>` M)ph) <-> ((M e. ZZ /\ H ~~> (B - A)) /\ A.k e. (ZZ>` M)ph))
41		3anass 778	. . . . . . . . 9 |- ((H ~~> (B - A) /\ M e. ZZ /\ A.k e. (ZZ>` M)ph) <-> (H ~~> (B - A) /\ (M e. ZZ /\ A.k e. (ZZ>` M)ph)))
42	39, 40, 41	3bitr3 181	. . . . . . . 8 |- (((M e. ZZ /\ H ~~> (B - A)) /\ A.k e. (ZZ>` M)ph) <-> (H ~~> (B - A) /\ (M e. ZZ /\ A.k e. (ZZ>` M)ph)))
43		eleq1 1531	. . . . . . . . . . . . . . . . 17 |- ((H` k) = ((G` k) - (F` k)) -> ((H` k) e. RR <-> ((G` k) - (F` k)) e. RR))
44	7, 43	sylbi 199	. . . . . . . . . . . . . . . 16 |- (ps -> ((H` k) e. RR <-> ((G` k) - (F` k)) e. RR))
45		resubclt 5418	. . . . . . . . . . . . . . . . 17 |- (((G` k) e. RR /\ (F` k) e. RR) -> ((G` k) - (F` k)) e. RR)
46	45, 17, 19	sylanc 471	. . . . . . . . . . . . . . . 16 |- (ph -> ((G` k) - (F` k)) e. RR)
47	44, 46	syl5bir 210	. . . . . . . . . . . . . . 15 |- (ps -> (ph -> (H` k) e. RR))
48	47	impcom 351	. . . . . . . . . . . . . 14 |- ((ph /\ ps) -> (H` k) e. RR)
49		3simp3 789	. . . . . . . . . . . . . . . . . 18 |- (((F` k) e. RR /\ (G` k) e. RR /\ (F` k) <_ (G` k)) -> (F` k) <_ (G` k))
50	15, 49	sylbi 199	. . . . . . . . . . . . . . . . 17 |- (ph -> (F` k) <_ (G` k))
51		subge0t 5655	. . . . . . . . . . . . . . . . . 18 |- (((G` k) e. RR /\ (F` k) e. RR) -> (0 <_ ((G` k) - (F` k)) <-> (F` k) <_ (G` k)))
52	51, 17, 19	sylanc 471	. . . . . . . . . . . . . . . . 17 |- (ph -> (0 <_ ((G` k) - (F` k)) <-> (F` k) <_ (G` k)))
53	50, 52	mpbird 196	. . . . . . . . . . . . . . . 16 |- (ph -> 0 <_ ((G` k) - (F` k)))
54	53	adantr 389	. . . . . . . . . . . . . . 15 |- ((ph /\ ps) -> 0 <_ ((G` k) - (F` k)))
55		breq2 2618	. . . . . . . . . . . . . . . . 17 |- ((H` k) = ((G` k) - (F` k))