This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abstri

Description: Triangle inequality for absolute value. Proposition 10-3.7(h) of Gleason p. 133. (Contributed by NM, 7-Mar-2005) (Proof shortened by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion abstri 
|- ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A + B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) )

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 1 a1i 
 |-  ( ( A e. CC /\ B e. CC ) -> 2 e. RR )
3 simpl 
 |-  ( ( A e. CC /\ B e. CC ) -> A e. CC )
4 simpr 
 |-  ( ( A e. CC /\ B e. CC ) -> B e. CC )
5 4 cjcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` B ) e. CC )
6 3 5 mulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. ( * ` B ) ) e. CC )
7 6 recld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A x. ( * ` B ) ) ) e. RR )
8 2 7 remulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) e. RR )
9 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
10 3 9 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` A ) e. RR )
11 abscl 
 |-  ( B e. CC -> ( abs ` B ) e. RR )
12 4 11 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` B ) e. RR )
13 10 12 remulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` A ) x. ( abs ` B ) ) e. RR )
14 2 13 remulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. ( ( abs ` A ) x. ( abs ` B ) ) ) e. RR )
15 10 resqcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` A ) ^ 2 ) e. RR )
16 12 resqcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` B ) ^ 2 ) e. RR )
17 15 16 readdcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) e. RR )
18 releabs 
 |-  ( ( A x. ( * ` B ) ) e. CC -> ( Re ` ( A x. ( * ` B ) ) ) <_ ( abs ` ( A x. ( * ` B ) ) ) )
19 6 18 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A x. ( * ` B ) ) ) <_ ( abs ` ( A x. ( * ` B ) ) ) )
20 absmul 
 |-  ( ( A e. CC /\ ( * ` B ) e. CC ) -> ( abs ` ( A x. ( * ` B ) ) ) = ( ( abs ` A ) x. ( abs ` ( * ` B ) ) ) )
21 3 5 20 syl2anc 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A x. ( * ` B ) ) ) = ( ( abs ` A ) x. ( abs ` ( * ` B ) ) ) )
22 abscj 
 |-  ( B e. CC -> ( abs ` ( * ` B ) ) = ( abs ` B ) )
23 4 22 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` ( * ` B ) ) = ( abs ` B ) )
24 23 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` A ) x. ( abs ` ( * ` B ) ) ) = ( ( abs ` A ) x. ( abs ` B ) ) )
25 21 24 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A x. ( * ` B ) ) ) = ( ( abs ` A ) x. ( abs ` B ) ) )
26 19 25 breqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A x. ( * ` B ) ) ) <_ ( ( abs ` A ) x. ( abs ` B ) ) )
27 2rp 
 |-  2 e. RR+
28 27 a1i 
 |-  ( ( A e. CC /\ B e. CC ) -> 2 e. RR+ )
29 7 13 28 lemul2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` ( A x. ( * ` B ) ) ) <_ ( ( abs ` A ) x. ( abs ` B ) ) <-> ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) <_ ( 2 x. ( ( abs ` A ) x. ( abs ` B ) ) ) ) )
30 26 29 mpbid 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) <_ ( 2 x. ( ( abs ` A ) x. ( abs ` B ) ) ) )
31 8 14 17 30 leadd2dd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) + ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) ) <_ ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) + ( 2 x. ( ( abs ` A ) x. ( abs ` B ) ) ) ) )
32 sqabsadd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` ( A + B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) + ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) ) )
33 10 recnd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` A ) e. CC )
34 12 recnd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` B ) e. CC )
35 binom2 
 |-  ( ( ( abs ` A ) e. CC /\ ( abs ` B ) e. CC ) -> ( ( ( abs ` A ) + ( abs ` B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( 2 x. ( ( abs ` A ) x. ( abs ` B ) ) ) ) + ( ( abs ` B ) ^ 2 ) ) )
36 33 34 35 syl2anc 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( abs ` A ) + ( abs ` B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( 2 x. ( ( abs ` A ) x. ( abs ` B ) ) ) ) + ( ( abs ` B ) ^ 2 ) ) )
37 15 recnd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` A ) ^ 2 ) e. CC )
38 14 recnd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. ( ( abs ` A ) x. ( abs ` B ) ) ) e. CC )
39 16 recnd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` B ) ^ 2 ) e. CC )
40 37 38 39 add32d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( abs ` A ) ^ 2 ) + ( 2 x. ( ( abs ` A ) x. ( abs ` B ) ) ) ) + ( ( abs ` B ) ^ 2 ) ) = ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) + ( 2 x. ( ( abs ` A ) x. ( abs ` B ) ) ) ) )
41 36 40 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( abs ` A ) + ( abs ` B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) + ( 2 x. ( ( abs ` A ) x. ( abs ` B ) ) ) ) )
42 31 32 41 3brtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` ( A + B ) ) ^ 2 ) <_ ( ( ( abs ` A ) + ( abs ` B ) ) ^ 2 ) )
43 addcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
44 abscl 
 |-  ( ( A + B ) e. CC -> ( abs ` ( A + B ) ) e. RR )
45 43 44 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A + B ) ) e. RR )
46 10 12 readdcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` A ) + ( abs ` B ) ) e. RR )
47 absge0 
 |-  ( ( A + B ) e. CC -> 0 <_ ( abs ` ( A + B ) ) )
48 43 47 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> 0 <_ ( abs ` ( A + B ) ) )
49 absge0 
 |-  ( A e. CC -> 0 <_ ( abs ` A ) )
50 3 49 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> 0 <_ ( abs ` A ) )
51 absge0 
 |-  ( B e. CC -> 0 <_ ( abs ` B ) )
52 4 51 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> 0 <_ ( abs ` B ) )
53 10 12 50 52 addge0d 
 |-  ( ( A e. CC /\ B e. CC ) -> 0 <_ ( ( abs ` A ) + ( abs ` B ) ) )
54 45 46 48 53 le2sqd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` ( A + B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) <-> ( ( abs ` ( A + B ) ) ^ 2 ) <_ ( ( ( abs ` A ) + ( abs ` B ) ) ^ 2 ) ) )
55 42 54 mpbird 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A + B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) )