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 φ A Fin
csbrn.2 φ k A B
csbrn.3 φ k A C
Assertion csbren φ k A B C 2 k A B 2 k A C 2

Proof

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