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 ) ) )