HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem climaddlem3 7052
Description: Lemma for climadd 7053. 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
StepHypRef Expression
1 climadd.4 . . . . . . . . . . . 12 |- A e. V
2 0z 6093 . . . . . . . . . . . . 13 |- 0 e. ZZ
3 nn0uz 6370 . . . . . . . . . . . . . 14 |- NN0 = (ZZ>` 0)
43eqimss2i 2102 . . . . . . . . . . . . 13 |- (ZZ>` 0) (_ NN0
5 uzssz 6362 . . . . . . . . . . . . 13 |- (ZZ>` M) (_ ZZ
62, 4, 5clmi2 7025 . . . . . . . . . . . 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)))
71, 6mpanl1 704 . . . . . . . . . . 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
92, 4, 5clmi2 7025 . . . . . . . . . . . 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)))
108, 9mpanl1 704 . . . . . . . . . . 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)))
117, 10anim12i 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))))
1211anandirs 512 . . . . . . . . 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))))
1312adantlr 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)))))
1513, 14sylanb 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 5981 . . . . . . . . 9 |- (v e. RR -> (v / 2) e. RR)
1716adantr 389 . . . . . . . 8 |- ((v e. RR /\ 0 < v) -> (v / 2) e. RR)
18 2re 5926 . . . . . . . . . 10 |- 2 e. RR
19 2pos 5936 . . . . . . . . . 10 |- 0 < 2
2018, 19pm3.2i 285 . . . . . . . . 9 |- (2 e. RR /\ 0 < 2)
21 divgt0t 5809 . . . . . . . . 9 |- (((v e. RR /\ 0 < v) /\ (2 e. RR /\ 0 < 2)) -> 0 < (v / 2))
2220, 21mpan2 694 . . . . . . . 8 |- ((v e. RR /\ 0 < v) -> 0 < (v / 2))
2317, 22jca 288 . . . . . . 7 |- ((v e. RR /\ 0 < v) -> ((v / 2) e. RR /\ 0 < (v / 2)))
2415, 23sylan2 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 6077 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. RR /\ f e. NN0) -> u <_ (u + f))
27 nn0ret 6055 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (u e. NN0 -> u e. RR)
2826, 27sylan 448 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. NN0 /\ f e. NN0) -> u <_ (u + f))
2928adantr 389 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((u e. NN0 /\ f e. NN0) /\ t e. RR) -> u <_ (u + f))
30 letrt 5498 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. RR /\ (u + f) e. RR /\ t e. RR) -> ((u <_ (u + f) /\ (u + f) <_ t) -> u <_ t))
31303expa 831 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((u e. RR /\ f e. RR) -> (u + f) e. RR)
3432, 33jca 288 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. RR /\ f e. RR) -> (u e. RR /\ (u + f) e. RR))
35 nn0ret 6055 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f e. NN0 -> f e. RR)
3634, 27, 35syl2an 454 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. NN0 /\ f e. NN0) -> (u e. RR /\ (u + f) e. RR))
3731, 36sylan 448 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((u e. NN0 /\ f e. NN0) /\ t e. RR) -> ((u <_ (u + f) /\ (u + f) <_ t) -> u <_ t))
3829, 37mpand 699 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((u e. NN0 /\ f e. NN0) /\ t e. RR) -> ((u + f) <_ t -> u <_ t))
39 eluzelz 6355 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (t e. (ZZ>` M) -> t e. ZZ)
40 zret 6086 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (t e. ZZ -> t e. RR)
4139, 40syl 10 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (t e. (ZZ>` M) -> t e. RR)
4238, 41sylan2 451 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>` M)) -> ((u + f) <_ t -> u <_ t))
4342adantr 389 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>` M)) /\ g e. (ZZ>` M)) -> ((u + f) <_ t -> u <_ t))
44 nn0addge2t 6078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f e. RR /\ u e. NN0) -> f <_ (u + f))
4544ancoms 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. NN0 /\ f e. RR) -> f <_ (u + f))
4645, 35sylan2 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. NN0 /\ f e. NN0) -> f <_ (u + f))
4746adantr 389 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((u e. NN0 /\ f e. NN0) /\ g e. RR) -> f <_ (u + f))
48 letrt 5498 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f e. RR /\ (u + f) e. RR /\ g e. RR) -> ((f <_ (u + f) /\ (u + f) <_ g) -> f <_ g))
49483expa 831 . . . . . . . . . . . . . . . . . . . . . . . . . . 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)
5150, 33jca 288 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. RR /\ f e. RR) -> (f e. RR /\ (u + f) e. RR))
5251, 27, 35syl2an 454 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. NN0 /\ f e. NN0) -> (f e. RR /\ (u + f) e. RR))
5349, 52sylan 448 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((u e. NN0 /\ f e. NN0) /\ g e. RR) -> ((f <_ (u + f) /\ (u + f) <_ g) -> f <_ g))
5447, 53mpand 699 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((u e. NN0 /\ f e. NN0) /\ g e. RR) -> ((u + f) <_ g -> f <_ g))
55 eluzelz 6355 . . . . . . . . . . . . . . . . . . . . . . . . . 26