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 
|- ( ph -> A e. Fin )
csbrn.2 
|- ( ( ph /\ k e. A ) -> B e. RR )
csbrn.3 
|- ( ( ph /\ k e. A ) -> C e. RR )
Assertion csbren 
|- ( ph -> ( sum_ k e. A ( B x. C ) ^ 2 ) <_ ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) )

Proof

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