HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem climmullem3 7066
Description: Lemma for climmul 7072.
Assertion
Ref Expression
climmullem3 |- ((((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) /\ ((abs` (F - A)) < 1 /\ (abs` (G - B)) < ((v / 2) / (1 + (abs` A))))) -> (abs` (F x. (G - B))) < (v / 2))
Proof of Theorem climmullem3
StepHypRef Expression
1 ltmul12it 5805 . . 3 |- (((((abs` F) e. RR /\ (1 + (abs` A)) e. RR) /\ (0 <_ (abs` F) /\ (abs` F) < (1 + (abs` A)))) /\ (((abs` (G - B)) e. RR /\ ((v / 2) / (1 + (abs` A))) e. RR) /\ (0 <_ (abs` (G - B)) /\ (abs` (G - B)) < ((v / 2) / (1 + (abs` A)))))) -> ((abs` F) x. (abs` (G - B))) < ((1 + (abs` A)) x. ((v / 2) / (1 + (abs` A)))))
2 absclt 6776 . . . . . . 7 |- (F e. CC -> (abs` F) e. RR)
32ad2antrr 404 . . . . . 6 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> (abs` F) e. RR)
433adant3 798 . . . . 5 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) -> (abs` F) e. RR)
54adantr 389 . . . 4 |- ((((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) /\ ((abs` (F - A)) < 1 /\ (abs` (G - B)) < ((v / 2) / (1 + (abs` A))))) -> (abs` F) e. RR)
6 absclt 6776 . . . . . . . 8 |- (A e. CC -> (abs` A) e. RR)
7 1re 5415 . . . . . . . . 9 |- 1 e. RR
8 axaddrcl 5252 . . . . . . . . 9 |- ((1 e. RR /\ (abs` A) e. RR) -> (1 + (abs` A)) e. RR)
97, 8mpan 694 . . . . . . . 8 |- ((abs` A) e. RR -> (1 + (abs` A)) e. RR)
106, 9syl 10 . . . . . . 7 |- (A e. CC -> (1 + (abs` A)) e. RR)
1110ad2antrl 406 . . . . . 6 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> (1 + (abs` A)) e. RR)
12113adant3 798 . . . . 5 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) -> (1 + (abs` A)) e. RR)
1312adantr 389 . . . 4 |- ((((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) /\ ((abs` (F - A)) < 1 /\ (abs` (G - B)) < ((v / 2) / (1 + (abs` A))))) -> (1 + (abs` A)) e. RR)
145, 13jca 288 . . 3 |- ((((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) /\ ((abs` (F - A)) < 1 /\ (abs` (G - B)) < ((v / 2) / (1 + (abs` A))))) -> ((abs` F) e. RR /\ (1 + (abs` A)) e. RR))
15 absge0t 6797 . . . . . . 7 |- (F e. CC -> 0 <_ (abs` F))
1615ad2antrr 404 . . . . . 6 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> 0 <_ (abs` F))
17163adant3 798 . . . . 5 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) -> 0 <_ (abs` F))
1817adantr 389 . . . 4 |- ((((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) /\ ((abs` (F - A)) < 1 /\ (abs` (G - B)) < ((v / 2) / (1 + (abs` A))))) -> 0 <_ (abs` F))
19 npcant 5379 . . . . . . . . . . . 12 |- ((F e. CC /\ A e. CC) -> ((F - A) + A) = F)
2019fveq2d 3719 . . . . . . . . . . 11 |- ((F e. CC /\ A e. CC) -> (abs` ((F - A) + A)) = (abs` F))
21 subclt 5347 . . . . . . . . . . . 12 |- ((F e. CC /\ A e. CC) -> (F - A) e. CC)
22 abstrit 6843 . . . . . . . . . . . 12 |- (((F - A) e. CC /\ A e. CC) -> (abs` ((F - A) + A)) <_ ((abs` (F - A)) + (abs` A)))
2321, 22sylancom 475 . . . . . . . . . . 11 |- ((F e. CC /\ A e. CC) -> (abs` ((F - A) + A)) <_ ((abs` (F - A)) + (abs` A)))
2420, 23eqbrtrrd 2632 . . . . . . . . . 10 |- ((F e. CC /\ A e. CC) -> (abs` F) <_ ((abs` (F - A)) + (abs` A)))
2524adantr 389 . . . . . . . . 9 |- (((F e. CC /\ A e. CC) /\ (abs` (F - A)) < 1) -> (abs` F) <_ ((abs` (F - A)) + (abs` A)))
26 ltadd1t 5605 . . . . . . . . . . 11 |- (((abs` (F - A)) e. RR /\ 1 e. RR /\ (abs` A) e. RR) -> ((abs` (F - A)) < 1 <-> ((abs` (F - A)) + (abs` A)) < (1 + (abs` A))))
27 absclt 6776 . . . . . . . . . . . 12 |- ((F - A) e. CC -> (abs` (F - A)) e. RR)
2821, 27syl 10 . . . . . . . . . . 11 |- ((F e. CC /\ A e. CC) -> (abs` (F - A)) e. RR)
297a1i 8 . . . . . . . . . . 11 |- ((F e. CC /\ A e. CC) -> 1 e. RR)
306adantl 388 . . . . . . . . . . 11 |- ((F e. CC /\ A e. CC) -> (abs` A) e. RR)
3126, 28, 29, 30syl3anc 857 . . . . . . . . . 10 |- ((F e. CC /\ A e. CC) -> ((abs` (F - A)) < 1 <-> ((abs` (F - A)) + (abs` A)) < (1 + (abs` A))))
3231biimpa 416 . . . . . . . . 9 |- (((F e. CC /\ A e. CC) /\ (abs` (F - A)) < 1) -> ((abs` (F - A)) + (abs` A)) < (1 + (abs` A)))
33 lelttrt 5504 . . . . . . . . . . 11 |- (((abs` F) e. RR /\ ((abs` (F - A)) + (abs` A)) e. RR /\ (1 + (abs` A)) e. RR) -> (((abs` F) <_ ((abs` (F - A)) + (abs` A)) /\ ((abs` (F - A)) + (abs` A)) < (1 + (abs` A))) -> (abs` F) < (1 + (abs` A))))
342adantr 389 . . . . . . . . . . 11 |- ((F e. CC /\ A e. CC) -> (abs` F) e. RR)
35 axaddrcl 5252 . . . . . . . . . . . 12 |- (((abs` (F - A)) e. RR /\ (abs` A) e. RR) -> ((abs` (F - A)) + (abs` A)) e. RR)
3635, 28, 30sylanc 471 . . . . . . . . . . 11 |- ((F e. CC /\ A e. CC) -> ((abs` (F - A)) + (abs` A)) e. RR)
3710adantl 388 . . . . . . . . . . 11 |- ((F e. CC /\ A e. CC) -> (1 + (abs` A)) e. RR)
3833, 34, 36, 37syl3anc 857 . . . . . . . . . 10 |- ((F e. CC /\ A e. CC) -> (((abs` F) <_ ((abs` (F - A)) + (abs` A)) /\ ((abs` (F - A)) + (abs` A)) < (1 + (abs` A))) -> (abs` F) < (1 + (abs` A))))
3938adantr 389 . . . . . . . . 9 |- (((F e. CC /\ A e. CC) /\ (abs` (F - A)) < 1) -> (((abs` F) <_ ((abs` (F - A)) + (abs` A)) /\ ((abs` (F - A)) + (abs` A)) < (1 + (abs` A))) -> (abs` F) < (1 + (abs` A))))
4025, 32, 39mp2and 702 . . . . . . . 8 |- (((F e. CC /\ A e. CC) /\ (abs` (F - A)) < 1) -> (abs` F) < (1 + (abs` A)))
4140adantlrr 399 . . . . . . 7 |- (((F e. CC /\ (A e. CC /\ B e. CC)) /\ (abs` (F - A)) < 1) -> (abs` F) < (1 + (abs` A)))
4241adantllr 397 . . . . . 6 |- ((((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) /\ (abs` (F - A)) < 1) -> (abs` F) < (1 + (abs` A)))
43423adantl3 804 . . . . 5 |- ((((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\