Metamath Proof Explorer

Theorem csbren

Description: Cauchy-Schwarz-Bunjakovsky inequality for 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 csbren ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ↑ 2 ) ≤ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 csbrn.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 csbrn.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3 csbrn.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
4 2cn ⊢ 2 ∈ ℂ
5 2 3 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 · 𝐶 ) ∈ ℝ )
6 1 5 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ∈ ℝ )
7 6 recnd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ∈ ℂ )
8 sqmul ⊢ ( ( 2 ∈ ℂ ∧ Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ∈ ℂ ) → ( ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ↑ 2 ) ) )
9 4 7 8 sylancr ⊢ ( 𝜑 → ( ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ↑ 2 ) ) )
10 sq2 ⊢ ( 2 ↑ 2 ) = 4
11 10 oveq1i ⊢ ( ( 2 ↑ 2 ) · ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ↑ 2 ) ) = ( 4 · ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ↑ 2 ) )
12 9 11 eqtrdi ⊢ ( 𝜑 → ( ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ↑ 2 ) = ( 4 · ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ↑ 2 ) ) )
13 2 resqcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 ↑ 2 ) ∈ ℝ )
14 1 13 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) ∈ ℝ )
15 2re ⊢ 2 ∈ ℝ
16 remulcl ⊢ ( ( 2 ∈ ℝ ∧ Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ∈ ℝ ) → ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ∈ ℝ )
17 15 6 16 sylancr ⊢ ( 𝜑 → ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ∈ ℝ )
18 3 resqcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 ↑ 2 ) ∈ ℝ )
19 1 18 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ∈ ℝ )
20 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ Fin )
21 13 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 ↑ 2 ) ∈ ℝ )
22 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
23 22 resqcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ↑ 2 ) ∈ ℝ )
24 21 23 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) ∈ ℝ )
25 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( 𝐵 · 𝐶 ) ∈ ℝ ) → ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℝ )
26 15 5 25 sylancr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℝ )
27 26 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℝ )
28 27 22 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ∈ ℝ )
29 24 28 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) ∈ ℝ )
30 18 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 ↑ 2 ) ∈ ℝ )
31 29 30 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( ( ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) + ( 𝐶 ↑ 2 ) ) ∈ ℝ )
32 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
33 32 22 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 · 𝑥 ) ∈ ℝ )
34 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
35 33 34 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐵 · 𝑥 ) + 𝐶 ) ∈ ℝ )
36 35 sqge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ ( ( ( 𝐵 · 𝑥 ) + 𝐶 ) ↑ 2 ) )
37 33 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 · 𝑥 ) ∈ ℂ )
38 34 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
39 binom2 ⊢ ( ( ( 𝐵 · 𝑥 ) ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐵 · 𝑥 ) + 𝐶 ) ↑ 2 ) = ( ( ( ( 𝐵 · 𝑥 ) ↑ 2 ) + ( 2 · ( ( 𝐵 · 𝑥 ) · 𝐶 ) ) ) + ( 𝐶 ↑ 2 ) ) )
40 37 38 39 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( ( ( 𝐵 · 𝑥 ) + 𝐶 ) ↑ 2 ) = ( ( ( ( 𝐵 · 𝑥 ) ↑ 2 ) + ( 2 · ( ( 𝐵 · 𝑥 ) · 𝐶 ) ) ) + ( 𝐶 ↑ 2 ) ) )
41 32 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
42 22 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → 𝑥 ∈ ℂ )
43 41 42 sqmuld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐵 · 𝑥 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) )
44 41 42 38 mul32d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐵 · 𝑥 ) · 𝐶 ) = ( ( 𝐵 · 𝐶 ) · 𝑥 ) )
45 44 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( 2 · ( ( 𝐵 · 𝑥 ) · 𝐶 ) ) = ( 2 · ( ( 𝐵 · 𝐶 ) · 𝑥 ) ) )
46 2cnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → 2 ∈ ℂ )
47 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 · 𝐶 ) ∈ ℝ )
48 47 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
49 46 48 42 mulassd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) = ( 2 · ( ( 𝐵 · 𝐶 ) · 𝑥 ) ) )
50 45 49 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( 2 · ( ( 𝐵 · 𝑥 ) · 𝐶 ) ) = ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) )
51 43 50 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( ( ( 𝐵 · 𝑥 ) ↑ 2 ) + ( 2 · ( ( 𝐵 · 𝑥 ) · 𝐶 ) ) ) = ( ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) )
52 51 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( ( ( ( 𝐵 · 𝑥 ) ↑ 2 ) + ( 2 · ( ( 𝐵 · 𝑥 ) · 𝐶 ) ) ) + ( 𝐶 ↑ 2 ) ) = ( ( ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) + ( 𝐶 ↑ 2 ) ) )
53 40 52 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( ( ( 𝐵 · 𝑥 ) + 𝐶 ) ↑ 2 ) = ( ( ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) + ( 𝐶 ↑ 2 ) ) )
54 36 53 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ ( ( ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) + ( 𝐶 ↑ 2 ) ) )
55 20 31 54 fsumge0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ≤ Σ 𝑘 ∈ 𝐴 ( ( ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) + ( 𝐶 ↑ 2 ) ) )
56 24 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) ∈ ℂ )
57 28 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ∈ ℂ )
58 56 57 addcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) ∈ ℂ )
59 30 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 ↑ 2 ) ∈ ℂ )
60 20 58 59 fsumadd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → Σ 𝑘 ∈ 𝐴 ( ( ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) + ( 𝐶 ↑ 2 ) ) = ( Σ 𝑘 ∈ 𝐴 ( ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) + Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) )
61 20 56 57 fsumadd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → Σ 𝑘 ∈ 𝐴 ( ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) = ( Σ 𝑘 ∈ 𝐴 ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + Σ 𝑘 ∈ 𝐴 ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) )
62 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
63 62 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
64 63 sqcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ↑ 2 ) ∈ ℂ )
65 21 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
66 20 64 65 fsummulc1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) = Σ 𝑘 ∈ 𝐴 ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) )
67 2cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 2 ∈ ℂ )
68 20 67 48 fsummulc2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) = Σ 𝑘 ∈ 𝐴 ( 2 · ( 𝐵 · 𝐶 ) ) )
69 68 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) · 𝑥 ) = ( Σ 𝑘 ∈ 𝐴 ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) )
70 26 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℂ )
71 70 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝐴 ) → ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℂ )
72 20 63 71 fsummulc1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( Σ 𝑘 ∈ 𝐴 ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) = Σ 𝑘 ∈ 𝐴 ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) )
73 69 72 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) · 𝑥 ) = Σ 𝑘 ∈ 𝐴 ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) )
74 66 73 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) = ( Σ 𝑘 ∈ 𝐴 ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + Σ 𝑘 ∈ 𝐴 ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) )
75 61 74 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → Σ 𝑘 ∈ 𝐴 ( ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) = ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) )
76 75 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( Σ 𝑘 ∈ 𝐴 ( ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) + Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) = ( ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) + Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) )
77 60 76 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → Σ 𝑘 ∈ 𝐴 ( ( ( ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) + ( 𝐶 ↑ 2 ) ) = ( ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) + Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) )
78 55 77 breqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · ( 𝑥 ↑ 2 ) ) + ( ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) · 𝑥 ) ) + Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) )
79 14 17 19 78 discr ⊢ ( 𝜑 → ( ( ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) ≤ 0 )
80 17 resqcld ⊢ ( 𝜑 → ( ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ↑ 2 ) ∈ ℝ )
81 4re ⊢ 4 ∈ ℝ
82 14 19 remulcld ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ∈ ℝ )
83 remulcl ⊢ ( ( 4 ∈ ℝ ∧ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ∈ ℝ ) → ( 4 · ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ∈ ℝ )
84 81 82 83 sylancr ⊢ ( 𝜑 → ( 4 · ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ∈ ℝ )
85 80 84 suble0d ⊢ ( 𝜑 → ( ( ( ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) ≤ 0 ↔ ( ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ↑ 2 ) ≤ ( 4 · ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) )
86 79 85 mpbid ⊢ ( 𝜑 → ( ( 2 · Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ) ↑ 2 ) ≤ ( 4 · ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) )
87 12 86 eqbrtrrd ⊢ ( 𝜑 → ( 4 · ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ↑ 2 ) ) ≤ ( 4 · ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) )
88 6 resqcld ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ↑ 2 ) ∈ ℝ )
89 81 a1i ⊢ ( 𝜑 → 4 ∈ ℝ )
90 4pos ⊢ 0 < 4
91 90 a1i ⊢ ( 𝜑 → 0 < 4 )
92 lemul2 ⊢ ( ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ↑ 2 ) ∈ ℝ ∧ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ∈ ℝ ∧ ( 4 ∈ ℝ ∧ 0 < 4 ) ) → ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ↑ 2 ) ≤ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ↔ ( 4 · ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ↑ 2 ) ) ≤ ( 4 · ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) )
93 88 82 89 91 92 syl112anc ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ↑ 2 ) ≤ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ↔ ( 4 · ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ↑ 2 ) ) ≤ ( 4 · ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) ) ) )
94 87 93 mpbird ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) ↑ 2 ) ≤ ( Σ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 2 ) · Σ 𝑘 ∈ 𝐴 ( 𝐶 ↑ 2 ) ) )