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}BC}^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 BC\in ℝ$$
6	1 5	fsumrecl	$$⊢\phi \to \sum _{k\in A}BC\in ℝ$$
7	6	recnd	$$⊢\phi \to \sum _{k\in A}BC\in ℂ$$
8		sqmul	$$⊢\left(2\in ℂ\wedge \sum _{k\in A}BC\in ℂ\right)\to {2\sum _{k\in A}BC}^2=2^2{\sum _{k\in A}BC}^2$$
9	4 7 8	sylancr	$$⊢\phi \to {2\sum _{k\in A}BC}^2=2^2{\sum _{k\in A}BC}^2$$
10		sq2	$$⊢2^2=4$$
11	10	oveq1i	$$⊢2^2{\sum _{k\in A}BC}^2=4{\sum _{k\in A}BC}^2$$
12	9 11	eqtrdi	$$⊢\phi \to {2\sum _{k\in A}BC}^2=4{\sum _{k\in A}BC}^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}BC\in ℝ\right)\to 2\sum _{k\in A}BC\in ℝ$$
17	15 6 16	sylancr	$$⊢\phi \to 2\sum _{k\in A}BC\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 BC\in ℝ\right)\to 2BC\in ℝ$$
26	15 5 25	sylancr	$$⊢\left(\phi \wedge k\in A\right)\to 2BC\in ℝ$$
27	26	adantlr	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge k\in A\right)\to 2BC\in ℝ$$
28	27 22	remulcld	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge k\in A\right)\to 2BCx\in ℝ$$
29	24 28	readdcld	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge k\in A\right)\to B^2{x}^2+2BCx\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+2BCx+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 Bx\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 Bx+C\in ℝ$$
36	35	sqge0d	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge k\in A\right)\to 0\le {\left(Bx+C\right)}^2$$
37	33	recnd	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge k\in A\right)\to Bx\in ℂ$$
38	34	recnd	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge k\in A\right)\to C\in ℂ$$
39		binom2	$$⊢\left(Bx\in ℂ\wedge C\in ℂ\right)\to {\left(Bx+C\right)}^2={Bx}^2+2BxC+C^2$$
40	37 38 39	syl2anc	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge k\in A\right)\to {\left(Bx+C\right)}^2={Bx}^2+2BxC+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 {Bx}^2=B^2{x}^2$$
44	41 42 38	mul32d	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge k\in A\right)\to BxC=BCx$$
45	44	oveq2d	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge k\in A\right)\to 2BxC=2BCx$$
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 BC\in ℝ$$
48	47	recnd	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge k\in A\right)\to BC\in ℂ$$
49	46 48 42	mulassd	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge k\in A\right)\to 2BCx=2BCx$$
50	45 49	eqtr4d	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge k\in A\right)\to 2BxC=2BCx$$
51	43 50	oveq12d	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge k\in A\right)\to {Bx}^2+2BxC=B^2{x}^2+2BCx$$
52	51	oveq1d	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge k\in A\right)\to {Bx}^2+2BxC+C^2=B^2{x}^2+2BCx+C^2$$
53	40 52	eqtrd	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge k\in A\right)\to {\left(Bx+C\right)}^2=B^2{x}^2+2BCx+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+2BCx+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+2BCx+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 2BCx\in ℂ$$
58	56 57	addcld	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge k\in A\right)\to B^2{x}^2+2BCx\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+2BCx+C^2\right)=\sum _{k\in A}\left(B^2{x}^2+2BCx\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+2BCx\right)=\sum _{k\in A}{B}^2{x}^2+\sum _{k\in A}2BCx$$
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}BC=\sum _{k\in A}2BC$$
69	68	oveq1d	$$⊢\left(\phi \wedge x\in ℝ\right)\to 2\sum _{k\in A}BCx=\sum _{k\in A}2BCx$$
70	26	recnd	$$⊢\left(\phi \wedge k\in A\right)\to 2BC\in ℂ$$
71	70	adantlr	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge k\in A\right)\to 2BC\in ℂ$$
72	20 63 71	fsummulc1	$$⊢\left(\phi \wedge x\in ℝ\right)\to \sum _{k\in A}2BCx=\sum _{k\in A}2BCx$$
73	69 72	eqtrd	$$⊢\left(\phi \wedge x\in ℝ\right)\to 2\sum _{k\in A}BCx=\sum _{k\in A}2BCx$$
74	66 73	oveq12d	$$⊢\left(\phi \wedge x\in ℝ\right)\to \sum _{k\in A}{B}^2{x}^2+2\sum _{k\in A}BCx=\sum _{k\in A}{B}^2{x}^2+\sum _{k\in A}2BCx$$
75	61 74	eqtr4d	$$⊢\left(\phi \wedge x\in ℝ\right)\to \sum _{k\in A}\left(B^2{x}^2+2BCx\right)=\sum _{k\in A}{B}^2{x}^2+2\sum _{k\in A}BCx$$
76	75	oveq1d	$$⊢\left(\phi \wedge x\in ℝ\right)\to \sum _{k\in A}\left(B^2{x}^2+2BCx\right)+\sum _{k\in A}{C}^2=\sum _{k\in A}{B}^2{x}^2+2\sum _{k\in A}BCx+\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+2BCx+C^2\right)=\sum _{k\in A}{B}^2{x}^2+2\sum _{k\in A}BCx+\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}BCx+\sum _{k\in A}{C}^2$$
79	14 17 19 78	discr	$$⊢\phi \to {2\sum _{k\in A}BC}^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}BC}^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}BC}^2-4\sum _{k\in A}{B}^2\sum _{k\in A}{C}^2\le 0\leftrightarrow {2\sum _{k\in A}BC}^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}BC}^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}BC}^2\le 4\sum _{k\in A}{B}^2\sum _{k\in A}{C}^2$$
88	6	resqcld	$$⊢\phi \to {\sum _{k\in A}BC}^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}BC}^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}BC}^2\le \sum _{k\in A}{B}^2\sum _{k\in A}{C}^2\leftrightarrow 4{\sum _{k\in A}BC}^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}BC}^2\le \sum _{k\in A}{B}^2\sum _{k\in A}{C}^2\leftrightarrow 4{\sum _{k\in A}BC}^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}BC}^2\le \sum _{k\in A}{B}^2\sum _{k\in A}{C}^2$$