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	$⊢ φ \to A \in Fin$
	csbrn.2	$⊢ (φ \land k \in A) \to B \in ℝ$
	csbrn.3	$⊢ (φ \land k \in A) \to C \in ℝ$
Assertion	csbren	$⊢ φ \to {\sum_{k \in A} B C}^{2} \leq \sum_{k \in A} B^{2} \sum_{k \in A} C^{2}$

Proof

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

Metamath Proof Explorer

Theorem csbren

Proof