HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem climmullem4 7076
Description: Lemma for climmul 7081.
Assertion
Ref Expression
climmullem4 |- ((((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) /\ (abs` (F - A)) < ((v / 2) / (1 + (abs` B)))) -> (abs` ((F - A) x. B)) < (v / 2))
Proof of Theorem climmullem4
StepHypRef Expression
1 absmult 6808 . . . . . . . 8 |- (((F - A) e. CC /\ B e. CC) -> (abs` ((F - A) x. B)) = ((abs` (F - A)) x. (abs` B)))
2 subclt 5350 . . . . . . . 8 |- ((F e. CC /\ A e. CC) -> (F - A) e. CC)
31, 2sylan 448 . . . . . . 7 |- (((F e. CC /\ A e. CC) /\ B e. CC) -> (abs` ((F - A) x. B)) = ((abs` (F - A)) x. (abs` B)))
43anasss 440 . . . . . 6 |- ((F e. CC /\ (A e. CC /\ B e. CC)) -> (abs` ((F - A) x. B)) = ((abs` (F - A)) x. (abs` B)))
54adantlr 393 . . . . 5 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> (abs` ((F - A) x. B)) = ((abs` (F - A)) x. (abs` B)))
653adant3 798 . . . 4 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) -> (abs` ((F - A) x. B)) = ((abs` (F - A)) x. (abs` B)))
76adantr 389 . . 3 |- ((((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) /\ (abs` (F - A)) < ((v / 2) / (1 + (abs` B)))) -> (abs` ((F - A) x. B)) = ((abs` (F - A)) x. (abs` B)))
8 lemul1itOLD 5804 . . . 4 |- ((((abs` (F - A)) e. RR /\ ((v / 2) / (1 + (abs` B))) e. RR /\ (abs` B) e. RR) /\ (0 <_ (abs` B) /\ (abs` (F - A)) <_ ((v / 2) / (1 + (abs` B))))) -> ((abs` (F - A)) x. (abs` B)) <_ (((v / 2) / (1 + (abs` B))) x. (abs` B)))
9 absclt 6783 . . . . . . . . 9 |- ((F - A) e. CC -> (abs` (F - A)) e. RR)
102, 9syl 10 . . . . . . . 8 |- ((F e. CC /\ A e. CC) -> (abs` (F - A)) e. RR)
1110ad2ant2r 409 . . . . . . 7 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> (abs` (F - A)) e. RR)
12113adant3 798 . . . . . 6 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) -> (abs` (F - A)) e. RR)
13 climmullem1 7073 . . . . . . . . 9 |- ((B e. CC /\ (v e. RR /\ 0 < v)) -> (((v / 2) / (1 + (abs` B))) e. RR /\ 0 < ((v / 2) / (1 + (abs` B)))))
1413pm3.26d 321 . . . . . . . 8 |- ((B e. CC /\ (v e. RR /\ 0 < v)) -> ((v / 2) / (1 + (abs` B))) e. RR)
1514adantll 392 . . . . . . 7 |- (((A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) -> ((v / 2) / (1 + (abs` B))) e. RR)
16153adant1 796 . . . . . 6 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) -> ((v / 2) / (1 + (abs` B))) e. RR)
17 absclt 6783 . . . . . . . 8 |- (B e. CC -> (abs` B) e. RR)
1817ad2antll 407 . . . . . . 7 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> (abs` B) e. RR)
19183adant3 798 . . . . . 6 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) -> (abs` B) e. RR)
2012, 16, 193jca 818 . . . . 5 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) -> ((abs` (F - A)) e. RR /\ ((v / 2) / (1 + (abs` B))) e. RR /\ (abs` B) e. RR))
2120adantr 389 . . . 4 |- ((((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) /\ (abs` (F - A)) < ((v / 2) / (1 + (abs` B)))) -> ((abs` (F - A)) e. RR /\ ((v / 2) / (1 + (abs` B))) e. RR /\ (abs` B) e. RR))
22 absge0t 6804 . . . . . . . 8 |- (B e. CC -> 0 <_ (abs` B))
2322ad2antll 407 . . . . . . 7 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC)) -> 0 <_ (abs` B))
24233adant3 798 . . . . . 6 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) -> 0 <_ (abs` B))
2524adantr 389 . . . . 5 |- ((((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) /\ (abs` (F - A)) < ((v / 2) / (1 + (abs` B)))) -> 0 <_ (abs` B))
26 ltlet 5503 . . . . . . 7 |- (((abs` (F - A)) e. RR /\ ((v / 2) / (1 + (abs` B))) e. RR) -> ((abs` (F - A)) < ((v / 2) / (1 + (abs` B))) -> (abs` (F - A)) <_ ((v / 2) / (1 + (abs` B)))))
2726, 12, 16sylanc 471 . . . . . 6 |- (((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) -> ((abs` (F - A)) < ((v / 2) / (1 + (abs` B))) -> (abs` (F - A)) <_ ((v / 2) / (1 + (abs` B)))))
2827imp 350 . . . . 5 |- ((((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) /\ (abs` (F - A)) < ((v / 2) / (1 + (abs` B)))) -> (abs` (F - A)) <_ ((v / 2) / (1 + (abs` B))))
2925, 28jca 288 . . . 4 |- ((((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) /\ (abs` (F - A)) < ((v / 2) / (1 + (abs` B)))) -> (0 <_ (abs` B) /\ (abs` (F - A)) <_ ((v / 2) / (1 + (abs` B)))))
308, 21, 29sylanc 471 . . 3 |- ((((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) /\ (abs` (F - A)) < ((v / 2) / (1 + (abs` B)))) -> ((abs` (F - A)) x. (abs` B)) <_ (((v / 2) / (1 + (abs` B))) x. (abs` B)))
317, 30eqbrtrd 2631 . 2 |- ((((F e. CC /\ G e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) /\ (abs` (F - A)) < ((v / 2) / (1 + (abs` B)))) -> (abs` ((F - A) x. B)) <_ (((v / 2) / (1 + (abs` B))) x. (abs` B)))
32 recp1lt1 5859 . . . . . . . . 9 |- (((abs` B) e. RR /\ 0 <_ (abs` B)) -> ((abs` B) / (1 + (abs` B))) < 1)
3332, 17, 22sylanc 471 . . . . . . . 8 |- (B e. CC -> ((abs` B) / (1 + (abs` B))) < 1)
3433adantr 389 . . . . . . 7 |- ((B e. CC /\ (v e. RR /\ 0 < v)) -> ((abs` B) / (1 + (abs` B))) < 1)
35 1re 5418 . . . . . . . . 9 |- 1 e. RR
36 ltmul1t 5796 . . . . . . . . 9 |- (((((abs` B) / (1 + (abs` B))) e. RR /\ 1 e. RR /\ (v / 2) e. RR) /\ 0 < (v / 2)) -> (((abs` B) / (1 + (abs` B))) < 1 <-> (((