# 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 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
csbrn.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℝ$
csbrn.3 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\in ℝ$
Assertion csbren ${⊢}{\phi }\to {\sum _{{k}\in {A}}{B}{C}}^{2}\le \sum _{{k}\in {A}}{{B}}^{2}\sum _{{k}\in {A}}{{C}}^{2}$

### Proof

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