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

Metamath Proof Explorer

Theorem trirn

Description: Triangle inequality in R^n. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 4-Jun-2014)

Ref Expression
Hypotheses csbrn.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
csbrn.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
csbrn.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
Assertion trirn ( 𝜑 → ( √ ‘ Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) ) ≤ ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 csbrn.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 csbrn.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3 csbrn.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
4 2 resqcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 ↑ 2 ) ∈ ℝ )
5 2re ⊢ 2 ∈ ℝ
6 2 3 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 · 𝐶 ) ∈ ℝ )
7 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( 𝐵 · 𝐶 ) ∈ ℝ ) → ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℝ )
8 5 6 7 sylancr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℝ )
9 4 8 readdcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · 𝐶 ) ) ) ∈ ℝ )
10 1 9 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · 𝐶 ) ) ) ∈ ℝ )
11 1 4 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ∈ ℝ )
12 3 resqcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 ↑ 2 ) ∈ ℝ )
13 1 12 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ∈ ℝ )
14 11 13 remulcld ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ∈ ℝ )
15 2 sqge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ ( 𝐵 ↑ 2 ) )
16 1 4 15 fsumge0 ⊢ ( 𝜑 → 0 ≤ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) )
17 3 sqge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ ( 𝐶 ↑ 2 ) )
18 1 12 17 fsumge0 ⊢ ( 𝜑 → 0 ≤ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) )
19 11 13 16 18 mulge0d ⊢ ( 𝜑 → 0 ≤ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) )
20 14 19 resqrtcld ⊢ ( 𝜑 → ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ∈ ℝ )
21 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ∈ ℝ ) → ( 2 · ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) ∈ ℝ )
22 5 20 21 sylancr ⊢ ( 𝜑 → ( 2 · ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) ∈ ℝ )
23 11 22 readdcld ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) + ( 2 · ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) ) ∈ ℝ )
24 4 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
25 8 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℂ )
26 1 24 25 fsumadd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · 𝐶 ) ) ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) + Σ 𝑘 ∈ 𝐴 ( 2 · ( 𝐵 · 𝐶 ) ) ) )
27 1 8 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℝ )
28 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
29 6 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
30 1 28 29 fsummulc2 ⊢ ( 𝜑 → ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) = Σ 𝑘 ∈ 𝐴 ( 2 · ( 𝐵 · 𝐶 ) ) )
31 1 6 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ∈ ℝ )
32 31 recnd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ∈ ℂ )
33 32 abscld ⊢ ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ∈ ℝ )
34 31 leabsd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ≤ ( abs ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) )
35 1 2 3 csbren ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ↑ 2 ) ≤ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) )
36 absresq ⊢ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ∈ ℝ → ( ( abs ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ↑ 2 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ↑ 2 ) )
37 31 36 syl ⊢ ( 𝜑 → ( ( abs ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ↑ 2 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ↑ 2 ) )
38 resqrtth ⊢ ( ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) → ( ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ↑ 2 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) )
39 14 19 38 syl2anc ⊢ ( 𝜑 → ( ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ↑ 2 ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) )
40 35 37 39 3brtr4d ⊢ ( 𝜑 → ( ( abs ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ↑ 2 ) ≤ ( ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ↑ 2 ) )
41 32 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) )
42 14 19 sqrtge0d ⊢ ( 𝜑 → 0 ≤ ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) )
43 33 20 41 42 le2sqd ⊢ ( 𝜑 → ( ( abs ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ≤ ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ↔ ( ( abs ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ↑ 2 ) ≤ ( ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ↑ 2 ) ) )
44 40 43 mpbird ⊢ ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ≤ ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) )
45 31 33 20 34 44 letrd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ≤ ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) )
46 5 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
47 2pos ⊢ 0 < 2
48 47 a1i ⊢ ( 𝜑 → 0 < 2 )
49 lemul2 ⊢ ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ∈ ℝ ∧ ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ≤ ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ↔ ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ≤ ( 2 · ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) ) )
50 31 20 46 48 49 syl112anc ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ≤ ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ↔ ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ≤ ( 2 · ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) ) )
51 45 50 mpbid ⊢ ( 𝜑 → ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ≤ ( 2 · ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) )
52 30 51 eqbrtrrd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 2 · ( 𝐵 · 𝐶 ) ) ≤ ( 2 · ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) )
53 27 22 11 52 leadd2dd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) + Σ 𝑘 ∈ 𝐴 ( 2 · ( 𝐵 · 𝐶 ) ) ) ≤ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) + ( 2 · ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) ) )
54 26 53 eqbrtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · 𝐶 ) ) ) ≤ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) + ( 2 · ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) ) )
55 10 23 13 54 leadd1dd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · 𝐶 ) ) ) + Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ≤ ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) + ( 2 · ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) ) + Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) )
56 2 3 readdcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
57 56 resqcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐵 + 𝐶 ) ↑ 2 ) ∈ ℝ )
58 1 57 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) ∈ ℝ )
59 56 sqge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ ( ( 𝐵 + 𝐶 ) ↑ 2 ) )
60 1 57 59 fsumge0 ⊢ ( 𝜑 → 0 ≤ Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) )
61 resqrtth ⊢ ( ( Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) ∈ ℝ ∧ 0 ≤ Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) ) → ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) )
62 58 60 61 syl2anc ⊢ ( 𝜑 → ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) )
63 2 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
64 3 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
65 binom2 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 + 𝐶 ) ↑ 2 ) = ( ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · 𝐶 ) ) ) + ( 𝐶 ↑ 2 ) ) )
66 63 64 65 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐵 + 𝐶 ) ↑ 2 ) = ( ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · 𝐶 ) ) ) + ( 𝐶 ↑ 2 ) ) )
67 66 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) = Σ 𝑘 ∈ 𝐴 ( ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · 𝐶 ) ) ) + ( 𝐶 ↑ 2 ) ) )
68 9 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · 𝐶 ) ) ) ∈ ℂ )
69 12 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 ↑ 2 ) ∈ ℂ )
70 1 68 69 fsumadd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · 𝐶 ) ) ) + ( 𝐶 ↑ 2 ) ) = ( Σ 𝑘 ∈ 𝐴 ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · 𝐶 ) ) ) + Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) )
71 67 70 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) = ( Σ 𝑘 ∈ 𝐴 ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · 𝐶 ) ) ) + Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) )
72 62 71 eqtrd ⊢ ( 𝜑 → ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) ) ↑ 2 ) = ( Σ 𝑘 ∈ 𝐴 ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · 𝐶 ) ) ) + Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) )
73 11 16 resqrtcld ⊢ ( 𝜑 → ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) ∈ ℝ )
74 73 recnd ⊢ ( 𝜑 → ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) ∈ ℂ )
75 13 18 resqrtcld ⊢ ( 𝜑 → ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ∈ ℝ )
76 75 recnd ⊢ ( 𝜑 → ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ∈ ℂ )
77 binom2 ⊢ ( ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) ∈ ℂ ∧ ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ∈ ℂ ) → ( ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ↑ 2 ) = ( ( ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) ↑ 2 ) + ( 2 · ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) · ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) ) + ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ↑ 2 ) ) )
78 74 76 77 syl2anc ⊢ ( 𝜑 → ( ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ↑ 2 ) = ( ( ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) ↑ 2 ) + ( 2 · ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) · ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) ) + ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ↑ 2 ) ) )
79 resqrtth ⊢ ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ∈ ℝ ∧ 0 ≤ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) → ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) )
80 11 16 79 syl2anc ⊢ ( 𝜑 → ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) )
81 11 16 13 18 sqrtmuld ⊢ ( 𝜑 → ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) = ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) · ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) )
82 81 eqcomd ⊢ ( 𝜑 → ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) · ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) = ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) )
83 82 oveq2d ⊢ ( 𝜑 → ( 2 · ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) · ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) = ( 2 · ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) )
84 80 83 oveq12d ⊢ ( 𝜑 → ( ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) ↑ 2 ) + ( 2 · ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) · ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) ) = ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) + ( 2 · ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) ) )
85 resqrtth ⊢ ( ( Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ∈ ℝ ∧ 0 ≤ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) → ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) )
86 13 18 85 syl2anc ⊢ ( 𝜑 → ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) )
87 84 86 oveq12d ⊢ ( 𝜑 → ( ( ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) ↑ 2 ) + ( 2 · ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) · ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) ) + ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ↑ 2 ) ) = ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) + ( 2 · ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) ) + Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) )
88 78 87 eqtrd ⊢ ( 𝜑 → ( ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ↑ 2 ) = ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) + ( 2 · ( √ ‘ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) ) + Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) )
89 55 72 88 3brtr4d ⊢ ( 𝜑 → ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) ) ↑ 2 ) ≤ ( ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ↑ 2 ) )
90 58 60 resqrtcld ⊢ ( 𝜑 → ( √ ‘ Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) ) ∈ ℝ )
91 73 75 readdcld ⊢ ( 𝜑 → ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ∈ ℝ )
92 58 60 sqrtge0d ⊢ ( 𝜑 → 0 ≤ ( √ ‘ Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) ) )
93 11 16 sqrtge0d ⊢ ( 𝜑 → 0 ≤ ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) )
94 13 18 sqrtge0d ⊢ ( 𝜑 → 0 ≤ ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) )
95 73 75 93 94 addge0d ⊢ ( 𝜑 → 0 ≤ ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) )
96 90 91 92 95 le2sqd ⊢ ( 𝜑 → ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) ) ≤ ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ↔ ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) ) ↑ 2 ) ≤ ( ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ↑ 2 ) ) )
97 89 96 mpbird ⊢ ( 𝜑 → ( √ ‘ Σ 𝑘 ∈ 𝐴 ( ( 𝐵 + 𝐶 ) ↑ 2 ) ) ≤ ( ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ) + ( √ ‘ Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) )