Theorem climcmplem 8793

Description: Lemma for climcmp 8794.

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		climcmplem.8	. . . . . . 7 |- (ch <-> (F ~~> A /\ G ~~> B))
2		fveq2 4765	. . . . . . . . . . . . . . . 16 |- (j = k -> (G` j) = (G` k))
3		fveq2 4765	. . . . . . . . . . . . . . . 16 |- (j = k -> (F` j) = (F` k))
4	2, 3	opreq12d 4996	. . . . . . . . . . . . . . 15 |- (j = k -> ((G` j) - (F` j)) = ((G` k) - (F` k)))
5		climcmplem.5	. . . . . . . . . . . . . . 15 |- H = {<.j, y>. | (j e. (ZZ>=` M) /\ y = ((G` j) - (F` j)))}
6		oprex 5003	. . . . . . . . . . . . . . 15 |- ((G` k) - (F` k)) e. _V
7	4, 5, 6	fvopab4 4829	. . . . . . . . . . . . . 14 |- (k e. (ZZ>=` M) -> (H` k) = ((G` k) - (F` k)))
8		climcmplem.7	. . . . . . . . . . . . . 14 |- (ps <-> (H` k) = ((G` k) - (F` k)))
9	7, 8	sylibr 243	. . . . . . . . . . . . 13 |- (k e. (ZZ>=` M) -> ps)
10	9	a1d 18	. . . . . . . . . . . 12 |- (k e. (ZZ>=` M) -> (ph -> ps))
11	10	ancld 513	. . . . . . . . . . 11 |- (k e. (ZZ>=` M) -> (ph -> (ph /\ ps)))
12	11	ralimia 2416	. . . . . . . . . 10 |- (A.k e. (ZZ>=` M)ph -> A.k e. (ZZ>=` M)(ph /\ ps))
13		climcmplem.6	. . . . . . . . . . . . . . 15 |- (ph <-> ((F` k) e. RR /\ (G` k) e. RR /\ (F` k) <_ (G` k)))
14	13	simp2bi 1136	. . . . . . . . . . . . . 14 |- (ph -> (G` k) e. RR)
15	13	simp1bi 1135	. . . . . . . . . . . . . 14 |- (ph -> (F` k) e. RR)
16		recn 6817	. . . . . . . . . . . . . . 15 |- ((G` k) e. RR -> (G` k) e. CC)
17		recn 6817	. . . . . . . . . . . . . . 15 |- ((F` k) e. RR -> (F` k) e. CC)
18	16, 17	anim12i 536	. . . . . . . . . . . . . 14 |- (((G` k) e. RR /\ (F` k) e. RR) -> ((G` k) e. CC /\ (F` k) e. CC))
19	14, 15, 18	syl11anc 659	. . . . . . . . . . . . 13 |- (ph -> ((G` k) e. CC /\ (F` k) e. CC))
20	19	anim1i 538	. . . . . . . . . . . 12 |- ((ph /\ (H` k) = ((G` k) - (F` k))) -> (((G` k) e. CC /\ (F` k) e. CC) /\ (H` k) = ((G` k) - (F` k))))
21	8	anbi2i 708	. . . . . . . . . . . 12 |- ((ph /\ ps) <-> (ph /\ (H` k) = ((G` k) - (F` k))))
22		df-3an 1104	. . . . . . . . . . . 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))))
23	20, 21, 22	3imtr4i 328	. . . . . . . . . . 11 |- ((ph /\ ps) -> ((G` k) e. CC /\ (F` k) e. CC /\ (H` k) = ((G` k) - (F` k))))
24	23	ralimi 2418	. . . . . . . . . 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))))
25	12, 24	syl 13	. . . . . . . . 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))))
26	25	anim2i 539	. . . . . . . 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)))))
27	26	anim2i 539	. . . . . . 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))))))
28	1, 27	sylanb 598	. . . . . 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))))))
29		climcmplem.2	. . . . . . . 8 |- G e. _V
30		climcmplem.1	. . . . . . . 8 |- F e. _V
31		fvex 4778	. . . . . . . . 9 |- (ZZ>=` M) e. _V
32	31, 5	fopabex2 4638	. . . . . . . 8 |- H e. _V
33		climcmplem.4	. . . . . . . 8 |- B e. _V
34		climcmplem.3	. . . . . . . 8 |- A e. _V
35	29, 30, 32, 33, 34	climsub 8786	. . . . . . 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))
36	35	ancom1s 856	. . . . . 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))
37		3ancoma 1109	. . . . . . . . 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))
38		df-3an 1104	. . . . . . . . 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))
39		3anass 1106	. . . . . . . . 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)))
40	37, 38, 39	3bitr3i 293	. . . . . . . 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)))
41		resubcl 7078	. . . . . . . . . . . . . . . . 17 |- (((G` k) e. RR /\ (F` k) e. RR) -> ((G` k) - (F` k)) e. RR)
42	14, 15, 41	syl11anc 659	. . . . . . . . . . . . . . . 16 |- (ph -> ((G` k) - (F` k)) e. RR)
43		eleq1 2204	. . . . . . . . . . . . . . . . 17 |- ((H` k) = ((G` k) - (F` k)) -> ((H` k) e. RR <-> ((G` k) - (F` k)) e. RR))
44	8, 43	sylbi 225	. . . . . . . . . . . . . . . 16 |- (ps -> ((H` k) e. RR <-> ((G` k) - (F` k)) e. RR))
45	42, 44	syl5ibr 257	. . . . . . . . . . . . . . 15 |- (ps -> (ph -> (H` k) e. RR))
46	45	impcom 394	. . . . . . . . . . . . . 14 |- ((ph /\ ps) -> (H` k) e. RR)
47	13	simp3bi 1137	. . . . . . . . . . . . . . . . 17 |- (ph -> (F` k) <_ (G` k))
48		subge0 7196	. . . . . . . . . . . . . . . . . 18 |- (((G` k) e. RR /\ (F` k) e. RR) -> (0 <_ ((G` k) - (F` k)) <-> (F` k) <_ (G` k)))
49	14, 15, 48	syl11anc 659	. . . . . . . . . . . . . . . . 17 |- (ph -> (0 <_ ((G` k) - (F` k)) <-> (F` k) <_ (G` k)))
50	47, 49	mpbird 318	. . . . . . . . . . . . . . . 16 |- (ph -> 0 <_ ((G` k) - (F` k)))
51	50	adantr 447	. . . . . . . . . . . . . . 15 |- ((ph /\ ps) -> 0 <_ ((G` k) - (F` k)))
52		breq2 3511	. . . . . . . . . . . . . . . . 17 |- ((H` k) = ((G` k) - (F` k)) -> (0 <_ (H` k) <-> 0 <_ ((G` k) - (F` k))))
53	8, 52	sylbi 225	. . . . . . . . . . . . . . . 16 |- (ps -> (0 <_ (H` k) <-> 0 <_ ((G` k) - (F` k))))
54	53	adantl 448	. . . . . . . . . . . . . . 15 |- ((ph /\ ps) -> (0 <_ (H` k) <-> 0 <_ ((G` k) - (F` k))))
55	51, 54	mpbird 318	. . . . . . . . . . . . . 14 |- ((ph /\ ps) -> 0 <_ (H` k))
56	46, 55	jca 494	. . . . . . . . . . . . 13 |- ((ph /\ ps) -> ((H` k) e. RR /\ 0 <_ (H` k)))
57	56	ralimi 2418	. . . . . . . . . . . 12 |- (A.k e. (ZZ>=` M)(ph /\ ps) -> A.k e. (ZZ>=` M)((H` k) e. RR /\ 0 <_ (H` k)))
58	12, 57	syl 13	. . . . . . . . . . 11 |- (A.k e. (ZZ>=` M)ph -> A.k e. (ZZ>=` M)((H` k) e. RR /\ 0 <_ (H` k)))
59	58	anim2i 539	. . . . . . . . . 10 |- (((M e. ZZ /\ H ~~> (B - A)) /\ A.k e. (ZZ>=` M)ph) -> ((M e. ZZ /\ H ~~> (B - A)) /\ A.k e. (ZZ>=` M)((H` k) e. RR /\ 0 <_ (H` k))))
60		df-3an 1104	. . . . . . . . . 10 |- ((M e. ZZ /\ H ~~> (B - A) /\ A.k e. (ZZ>=` M)((H` k) e. RR /\ 0 <_ (H` k))) <-> ((M e. ZZ /\ H ~~> (B - A)) /\ A.k e. (ZZ>=` M)((H` k) e. RR /\ 0 <_ (H` k))))
61	59, 60	sylibr 243	. . . . . . . . 9 |- (((M e. ZZ /\ H ~~> (B - A)) /\ A.k e. (ZZ>=` M)ph) -> (M e. ZZ /\ H ~~> (B - A) /\ A.k e. (ZZ>=` M)((H` k) e. RR /\ 0 <_ (H` k))))
62		oprex 5003	. . . . . . . . . 10 |- (B - A) e. _V
63	62	climge0 8768	. . . . . . . . 9 |- ((M e. ZZ /\ H ~~> (B - A) /\ A.k e. (ZZ>=` M)((H` k) e. RR /\ 0 <_ (H` k))) -> 0 <_ (B - A))
64	61, 63	syl 13	. . . . . . . 8 |- (((M e. ZZ /\ H ~~> (B - A)) /\ A.k e. (ZZ>=` M)ph) -> 0 <_ (B - A))
65	40, 64	sylbir 244	. . . . . . 7 |- ((H ~~> (B - A) /\ (M e. ZZ /\ A.k e. (ZZ>=` M)ph)) -> 0 <_ (B - A))
66	65	ex 398	. . . . . 6 |- (H ~~> (B - A) -> ((M e. ZZ /\ A.k e. (ZZ>=` M)ph) -> 0 <_ (B - A)))
67	28, 36, 66	3syl 41	. . . . 5 |- ((ch /\ (M e. ZZ /\ A.k e. (ZZ>=` M)ph)) -> ((M e. ZZ /\ A.k e. (ZZ>=` M)ph) -> 0 <_ (B - A)))
68	67	ex 398	. . . 4 |- (ch -> ((M e. ZZ /\ A.k e. (ZZ>=` M)ph) -> ((M e. ZZ /\ A.k e. (ZZ>=` M)ph) -> 0 <_ (B - A))))
69	68	pm2.43d 109	. . 3 |- (ch -> ((M e. ZZ /\ A.k e. (ZZ>=` M)ph) -> 0 <_ (B - A)))
70	69	imp 393	. 2 |- ((ch /\ (M e. ZZ /\ A.k e. (ZZ>=` M)ph)) -> 0 <_ (B - A))
71	14	ralimi 2418	. . . . 5 |- (A.k e. (ZZ>=` M)ph -> A.k e. (ZZ>=` M)(G` k) e. RR)
72	33	climrecl 8766	. . . . . . . 8 |- ((M e. ZZ /\ G ~~> B /\ A.k e. (ZZ>=` M)(G` k) e. RR) -> B e. RR)
73	72	3com12 1321	. . . . . . 7 |- ((G ~~> B /\ M e. ZZ /\ A.k e. (ZZ>=` M)(G` k) e. RR) -> B e. RR)
74	73	3adant1l 1339	. . . . . 6 |- (((F ~~> A /\ G ~~> B) /\ M e. ZZ /\ A.k e. (ZZ>=` M)(G` k) e. RR) -> B e. RR)
75	1, 74	syl3an1b 1385	. . . . 5 |- ((ch /\ M e. ZZ /\ A.k e. (ZZ>=` M)(G` k) e. RR) -> B e. RR)
76	71, 75	syl3an3 1384	. . . 4 |- ((ch /\ M e. ZZ /\ A.k e. (ZZ>=` M)ph) -> B e. RR)
77	15	ralimi 2418	. . . . 5 |- (A.k e. (ZZ>=` M)ph -> A.k e. (ZZ>=` M)(F` k) e. RR)
78	34	climrecl 8766	. . . . . . . 8 |- ((M e. ZZ /\ F ~~> A /\ A.k e. (ZZ>=` M)(F` k) e. RR) -> A e. RR)
79	78	3com12 1321	. . . . . . 7 |- ((F ~~> A /\ M e. ZZ /\ A.k e. (ZZ>=` M)(F` k) e. RR) -> A e. RR)
80	79	3adant1r 1340	. . . . . 6 |- (((F ~~> A /\ G ~~> B) /\ M e. ZZ /\ A.k e. (ZZ>=` M)(F` k) e. RR) -> A e. RR)
81	1, 80	syl3an1b 1385	. . . . 5 |- ((ch /\ M e. ZZ /\ A.k e. (ZZ>=` M)(F` k) e. RR) -> A e. RR)
82	77, 81	syl3an3 1384	. . . 4 |- ((ch /\ M e. ZZ /\ A.k e. (ZZ>=` M)ph) -> A e. RR)
83		subge0 7196	. . . 4 |- ((B e. RR /\ A e. RR) -> (0 <_ (B - A) <-> A <_ B))
84	76, 82, 83	syl11anc 659	. . 3 |- ((ch /\ M e. ZZ /\ A.k e. (ZZ>=` M)ph) -> (0 <_ (B - A) <-> A <_ B))
85	84	3expb 1318	. 2 |- ((ch /\ (M e. ZZ /\ A.k e. (ZZ>=` M)ph)) -> (0 <_ (B - A) <-> A <_ B))
86	70, 85	mpbid 317	1 |- ((ch /\ (M e. ZZ /\ A.k e. (ZZ>=` M)ph)) -> A <_ B)

Syntax hints:   -> wi 3   <-> wb 219   /\ wa 337   /\ w3a 1102   = wceq 1586   e. wcel 1588  A.wral 2355  _Vcvv 2538   class class class wbr 3507  {copab 3565  ` cfv 4131  (class class class)co 4981  CCcc 6750  RRcr 6751  0cc0 6752   <_ cle 6841   - cmin 6989  ZZcz 6994  ZZ>=cuz 7933   ~~> cli 8630

This theorem is referenced by:  climcmp 8794

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-nel 2269  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-mpt 5099  df-1st 5126  df-2nd 5127  df-iota 5219  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-en 5588  df-dom 5589  df-sdom 5590  df-undef 5725  df-riota 5729  df-sup 5888  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-mp 6607  df-ltp 6608  df-plpr 6682  df-mpr 6683  df-enr 6684  df-nr 6685  df-plr 6686  df-mr 6687  df-ltr 6688  df-0r 6689  df-1r 6690  df-m1r 6691  df-c 6758  df-0 6759  df-1 6760  df-i 6761  df-r 6762  df-plus 6763  df-mul 6764  df-lt 6765  df-pnf 6846  df-mnf 6847  df-xr 6848  df-ltxr 6849  df-le 6850  df-sub 7009  df-neg 7011  df-div 7223  df-n 7441  df-2 7487  df-n0 7649  df-z 7686  df-uz 7934  df-seq1 8094  df-exp 8196  df-sqr 8304  df-re 8385  df-im 8386  df-cj 8387  df-abs 8388  df-clim 8631

Copyright terms: Public domain