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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( 𝐴 + 𝐵 ) ) ≤ ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 1 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 2 ∈ ℝ )
3 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
4 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
5 4 cjcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ 𝐵 ) ∈ ℂ )
6 3 5 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ∈ ℂ )
7 6 recld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ∈ ℝ )
8 2 7 remulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) ∈ ℝ )
9 abscl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
10 3 9 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ 𝐴 ) ∈ ℝ )
11 abscl ⊢ ( 𝐵 ∈ ℂ → ( abs ‘ 𝐵 ) ∈ ℝ )
12 4 11 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ 𝐵 ) ∈ ℝ )
13 10 12 remulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) ∈ ℝ )
14 2 13 remulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) ) ∈ ℝ )
15 10 resqcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) ∈ ℝ )
16 12 resqcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ 𝐵 ) ↑ 2 ) ∈ ℝ )
17 15 16 readdcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) ∈ ℝ )
18 releabs ⊢ ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ∈ ℂ → ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ≤ ( abs ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) )
19 6 18 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ≤ ( abs ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) )
20 absmul ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ∗ ‘ 𝐵 ) ∈ ℂ ) → ( abs ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ ( ∗ ‘ 𝐵 ) ) ) )
21 3 5 20 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ ( ∗ ‘ 𝐵 ) ) ) )
22 abscj ⊢ ( 𝐵 ∈ ℂ → ( abs ‘ ( ∗ ‘ 𝐵 ) ) = ( abs ‘ 𝐵 ) )
23 4 22 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( ∗ ‘ 𝐵 ) ) = ( abs ‘ 𝐵 ) )
24 23 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ 𝐴 ) · ( abs ‘ ( ∗ ‘ 𝐵 ) ) ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) )
25 21 24 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) )
26 19 25 breqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ≤ ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) )
27 2rp ⊢ 2 ∈ ℝ+
28 27 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 2 ∈ ℝ+ )
29 7 13 28 lemul2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ≤ ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) ↔ ( 2 · ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) ≤ ( 2 · ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) ) ) )
30 26 29 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) ≤ ( 2 · ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) ) )
31 8 14 17 30 leadd2dd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) + ( 2 · ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) ) ≤ ( ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) + ( 2 · ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) ) ) )
32 sqabsadd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) + ( 2 · ( ℜ ‘ ( 𝐴 · ( ∗ ‘ 𝐵 ) ) ) ) ) )
33 10 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ 𝐴 ) ∈ ℂ )
34 12 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ 𝐵 ) ∈ ℂ )
35 binom2 ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℂ ∧ ( abs ‘ 𝐵 ) ∈ ℂ ) → ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐵 ) ) ↑ 2 ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( 2 · ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) ) ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) )
36 33 34 35 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐵 ) ) ↑ 2 ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( 2 · ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) ) ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) )
37 15 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
38 14 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) ) ∈ ℂ )
39 16 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ 𝐵 ) ↑ 2 ) ∈ ℂ )
40 37 38 39 add32d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( 2 · ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) ) ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) + ( 2 · ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) ) ) )
41 36 40 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐵 ) ) ↑ 2 ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) + ( 2 · ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐵 ) ) ) ) )
42 31 32 41 3brtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) ≤ ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐵 ) ) ↑ 2 ) )
43 addcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
44 abscl ⊢ ( ( 𝐴 + 𝐵 ) ∈ ℂ → ( abs ‘ ( 𝐴 + 𝐵 ) ) ∈ ℝ )
45 43 44 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( 𝐴 + 𝐵 ) ) ∈ ℝ )
46 10 12 readdcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐵 ) ) ∈ ℝ )
47 absge0 ⊢ ( ( 𝐴 + 𝐵 ) ∈ ℂ → 0 ≤ ( abs ‘ ( 𝐴 + 𝐵 ) ) )
48 43 47 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 0 ≤ ( abs ‘ ( 𝐴 + 𝐵 ) ) )
49 absge0 ⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( abs ‘ 𝐴 ) )
50 3 49 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 0 ≤ ( abs ‘ 𝐴 ) )
51 absge0 ⊢ ( 𝐵 ∈ ℂ → 0 ≤ ( abs ‘ 𝐵 ) )
52 4 51 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 0 ≤ ( abs ‘ 𝐵 ) )
53 10 12 50 52 addge0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 0 ≤ ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐵 ) ) )
54 45 46 48 53 le2sqd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ ( 𝐴 + 𝐵 ) ) ≤ ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐵 ) ) ↔ ( ( abs ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) ≤ ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐵 ) ) ↑ 2 ) ) )
55 42 54 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( 𝐴 + 𝐵 ) ) ≤ ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐵 ) ) )