Theorem climaddlem3 7069

Description: Lemma for climadd 7070. Warning: The HTML proof page is 3/4 megabyte in size.

Hypotheses

Ref	Expression
climadd.1	|- F e. V
climadd.2	|- G e. V
climadd.3	|- H e. V
climadd.4	|- A e. V
climadd.5	|- B e. V
climaddlem.6	|- (ph <-> ((F ~~> A /\ G ~~> B) /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) + (G` k)))))

Assertion

Ref	Expression
climaddlem3	|- ((M e. ZZ /\ ph) -> H ~~> (A + B))

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

Proof of Theorem climaddlem3

Step	Hyp	Ref	Expression
1		climadd.4	. . . . . . . . . . . 12 |- A e. V
2		0z 6103	. . . . . . . . . . . . 13 |- 0 e. ZZ
3		nn0uz 6383	. . . . . . . . . . . . . 14 |- NN0 = (ZZ>` 0)
4	3	eqimss2i 2109	. . . . . . . . . . . . 13 |- (ZZ>` 0) (_ NN0
5		uzssz 6375	. . . . . . . . . . . . 13 |- (ZZ>` M) (_ ZZ
6	2, 4, 5	clmi2 7040	. . . . . . . . . . . 12 |- (((A e. V /\ F ~~> A) /\ ((v / 2) e. RR /\ 0 < (v / 2))) -> E.u e. NN0 A.t e. (ZZ>` M)(u <_ t -> (abs` ((F` t) - A)) < (v / 2)))
7	1, 6	mpanl1 705	. . . . . . . . . . 11 |- ((F ~~> A /\ ((v / 2) e. RR /\ 0 < (v / 2))) -> E.u e. NN0 A.t e. (ZZ>` M)(u <_ t -> (abs` ((F` t) - A)) < (v / 2)))
8		climadd.5	. . . . . . . . . . . 12 |- B e. V
9	2, 4, 5	clmi2 7040	. . . . . . . . . . . 12 |- (((B e. V /\ G ~~> B) /\ ((v / 2) e. RR /\ 0 < (v / 2))) -> E.f e. NN0 A.g e. (ZZ>` M)(f <_ g -> (abs` ((G` g) - B)) < (v / 2)))
10	8, 9	mpanl1 705	. . . . . . . . . . 11 |- ((G ~~> B /\ ((v / 2) e. RR /\ 0 < (v / 2))) -> E.f e. NN0 A.g e. (ZZ>` M)(f <_ g -> (abs` ((G` g) - B)) < (v / 2)))
11	7, 10	anim12i 333	. . . . . . . . . 10 |- (((F ~~> A /\ ((v / 2) e. RR /\ 0 < (v / 2))) /\ (G ~~> B /\ ((v / 2) e. RR /\ 0 < (v / 2)))) -> (E.u e. NN0 A.t e. (ZZ>` M)(u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ E.f e. NN0 A.g e. (ZZ>` M)(f <_ g -> (abs` ((G` g) - B)) < (v / 2))))
12	11	anandirs 513	. . . . . . . . 9 |- (((F ~~> A /\ G ~~> B) /\ ((v / 2) e. RR /\ 0 < (v / 2))) -> (E.u e. NN0 A.t e. (ZZ>` M)(u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ E.f e. NN0 A.g e. (ZZ>` M)(f <_ g -> (abs` ((G` g) - B)) < (v / 2))))
13	12	adantlr 393	. . . . . . . 8 |- ((((F ~~> A /\ G ~~> B) /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) + (G` k)))) /\ ((v / 2) e. RR /\ 0 < (v / 2))) -> (E.u e. NN0 A.t e. (ZZ>` M)(u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ E.f e. NN0 A.g e. (ZZ>` M)(f <_ g -> (abs` ((G` g) - B)) < (v / 2))))
14		climaddlem.6	. . . . . . . 8 |- (ph <-> ((F ~~> A /\ G ~~> B) /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) + (G` k)))))
15	13, 14	sylanb 449	. . . . . . 7 |- ((ph /\ ((v / 2) e. RR /\ 0 < (v / 2))) -> (E.u e. NN0 A.t e. (ZZ>` M)(u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ E.f e. NN0 A.g e. (ZZ>` M)(f <_ g -> (abs` ((G` g) - B)) < (v / 2))))
16		rehalfclt 5991	. . . . . . . . 9 |- (v e. RR -> (v / 2) e. RR)
17	16	adantr 389	. . . . . . . 8 |- ((v e. RR /\ 0 < v) -> (v / 2) e. RR)
18		2re 5936	. . . . . . . . . 10 |- 2 e. RR
19		2pos 5946	. . . . . . . . . 10 |- 0 < 2
20	18, 19	pm3.2i 285	. . . . . . . . 9 |- (2 e. RR /\ 0 < 2)
21		divgt0t 5819	. . . . . . . . 9 |- (((v e. RR /\ 0 < v) /\ (2 e. RR /\ 0 < 2)) -> 0 < (v / 2))
22	20, 21	mpan2 695	. . . . . . . 8 |- ((v e. RR /\ 0 < v) -> 0 < (v / 2))
23	17, 22	jca 288	. . . . . . 7 |- ((v e. RR /\ 0 < v) -> ((v / 2) e. RR /\ 0 < (v / 2)))
24	15, 23	sylan2 451	. . . . . 6 |- ((ph /\ (v e. RR /\ 0 < v)) -> (E.u e. NN0 A.t e. (ZZ>` M)(u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ E.f e. NN0 A.g e. (ZZ>` M)(f <_ g -> (abs` ((G` g) - B)) < (v / 2))))
25		pm3.27 323	. . . . . . . . . . . . . . . . . 18 |- (((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>` M)) -> t e. (ZZ>` M))
26		nn0addge1t 6087	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. RR /\ f e. NN0) -> u <_ (u + f))
27		nn0ret 6065	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (u e. NN0 -> u e. RR)
28	26, 27	sylan 448	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. NN0 /\ f e. NN0) -> u <_ (u + f))
29	28	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((u e. NN0 /\ f e. NN0) /\ t e. RR) -> u <_ (u + f))
30		letrt 5508	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. RR /\ (u + f) e. RR /\ t e. RR) -> ((u <_ (u + f) /\ (u + f) <_ t) -> u <_ t))
31	30	3expa 832	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((u e. RR /\ (u + f) e. RR) /\ t e. RR) -> ((u <_ (u + f) /\ (u + f) <_ t) -> u <_ t))
32		pm3.26 319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((u e. RR /\ f e. RR) -> u e. RR)
33		axaddrcl 5255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((u e. RR /\ f e. RR) -> (u + f) e. RR)
34	32, 33	jca 288	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. RR /\ f e. RR) -> (u e. RR /\ (u + f) e. RR))
35		nn0ret 6065	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f e. NN0 -> f e. RR)
36	34, 27, 35	syl2an 454	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. NN0 /\ f e. NN0) -> (u e. RR /\ (u + f) e. RR))
37	31, 36	sylan 448	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((u e. NN0 /\ f e. NN0) /\ t e. RR) -> ((u <_ (u + f) /\ (u + f) <_ t) -> u <_ t))
38	29, 37	mpand 700	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((u e. NN0 /\ f e. NN0) /\ t e. RR) -> ((u + f) <_ t -> u <_ t))
39		eluzelz 6368	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (t e. (ZZ>` M) -> t e. ZZ)
40		zret 6096	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (t e. ZZ -> t e. RR)
41	39, 40	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (t e. (ZZ>` M) -> t e. RR)
42	38, 41	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>` M)) -> ((u + f) <_ t -> u <_ t))
43	42	adantr 389	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>` M)) /\ g e. (ZZ>` M)) -> ((u + f) <_ t -> u <_ t))
44		nn0addge2t 6088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f e. RR /\ u e. NN0) -> f <_ (u + f))
45	44	ancoms 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. NN0 /\ f e. RR) -> f <_ (u + f))
46	45, 35	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. NN0 /\ f e. NN0) -> f <_ (u + f))
47	46	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((u e. NN0 /\ f e. NN0) /\ g e. RR) -> f <_ (u + f))
48		letrt 5508	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f e. RR /\ (u + f) e. RR /\ g e. RR) -> ((f <_ (u + f) /\ (u + f) <_ g) -> f <_ g))
49	48	3expa 832	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((f e. RR /\ (u + f) e. RR) /\ g e. RR) -> ((f <_ (u + f) /\ (u + f) <_ g) -> f <_ g))
50		pm3.27 323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((u e. RR /\ f e. RR) -> f e. RR)
51	50, 33	jca 288	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. RR /\ f e. RR) -> (f e. RR /\ (u + f) e. RR))
52	51, 27, 35	syl2an 454	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. NN0 /\ f e. NN0) -> (f e. RR /\ (u + f) e. RR))
53	49, 52	sylan 448	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((u e. NN0 /\ f e. NN0) /\ g e. RR) -> ((f <_ (u + f) /\ (u + f) <_ g) -> f <_ g))
54	47, 53	mpand 700	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((u e. NN0 /\ f e. NN0) /\ g e. RR) -> ((u + f) <_ g -> f <_ g))
55		eluzelz 6368	. . . . . . . . . . . . . . . . . . . . . . . . . 26