Metamath Proof Explorer

Theorem trirn

Description: Triangle inequality in 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 trirn 
|- ( ph -> ( sqrt ` sum_ k e. A ( ( B + C ) ^ 2 ) ) <_ ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) + ( sqrt ` 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 2 resqcld 
 |-  ( ( ph /\ k e. A ) -> ( B ^ 2 ) e. RR )
5 2re 
 |-  2 e. RR
6 2 3 remulcld 
 |-  ( ( ph /\ k e. A ) -> ( B x. C ) e. RR )
7 remulcl 
 |-  ( ( 2 e. RR /\ ( B x. C ) e. RR ) -> ( 2 x. ( B x. C ) ) e. RR )
8 5 6 7 sylancr 
 |-  ( ( ph /\ k e. A ) -> ( 2 x. ( B x. C ) ) e. RR )
9 4 8 readdcld 
 |-  ( ( ph /\ k e. A ) -> ( ( B ^ 2 ) + ( 2 x. ( B x. C ) ) ) e. RR )
10 1 9 fsumrecl 
 |-  ( ph -> sum_ k e. A ( ( B ^ 2 ) + ( 2 x. ( B x. C ) ) ) e. RR )
11 1 4 fsumrecl 
 |-  ( ph -> sum_ k e. A ( B ^ 2 ) e. RR )
12 3 resqcld 
 |-  ( ( ph /\ k e. A ) -> ( C ^ 2 ) e. RR )
13 1 12 fsumrecl 
 |-  ( ph -> sum_ k e. A ( C ^ 2 ) e. RR )
14 11 13 remulcld 
 |-  ( ph -> ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) e. RR )
15 2 sqge0d 
 |-  ( ( ph /\ k e. A ) -> 0 <_ ( B ^ 2 ) )
16 1 4 15 fsumge0 
 |-  ( ph -> 0 <_ sum_ k e. A ( B ^ 2 ) )
17 3 sqge0d 
 |-  ( ( ph /\ k e. A ) -> 0 <_ ( C ^ 2 ) )
18 1 12 17 fsumge0 
 |-  ( ph -> 0 <_ sum_ k e. A ( C ^ 2 ) )
19 11 13 16 18 mulge0d 
 |-  ( ph -> 0 <_ ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) )
20 14 19 resqrtcld 
 |-  ( ph -> ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) e. RR )
21 remulcl 
 |-  ( ( 2 e. RR /\ ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) e. RR ) -> ( 2 x. ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ) e. RR )
22 5 20 21 sylancr 
 |-  ( ph -> ( 2 x. ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ) e. RR )
23 11 22 readdcld 
 |-  ( ph -> ( sum_ k e. A ( B ^ 2 ) + ( 2 x. ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ) ) e. RR )
24 4 recnd 
 |-  ( ( ph /\ k e. A ) -> ( B ^ 2 ) e. CC )
25 8 recnd 
 |-  ( ( ph /\ k e. A ) -> ( 2 x. ( B x. C ) ) e. CC )
26 1 24 25 fsumadd 
 |-  ( ph -> sum_ k e. A ( ( B ^ 2 ) + ( 2 x. ( B x. C ) ) ) = ( sum_ k e. A ( B ^ 2 ) + sum_ k e. A ( 2 x. ( B x. C ) ) ) )
27 1 8 fsumrecl 
 |-  ( ph -> sum_ k e. A ( 2 x. ( B x. C ) ) e. RR )
28 2cnd 
 |-  ( ph -> 2 e. CC )
29 6 recnd 
 |-  ( ( ph /\ k e. A ) -> ( B x. C ) e. CC )
30 1 28 29 fsummulc2 
 |-  ( ph -> ( 2 x. sum_ k e. A ( B x. C ) ) = sum_ k e. A ( 2 x. ( B x. C ) ) )
31 1 6 fsumrecl 
 |-  ( ph -> sum_ k e. A ( B x. C ) e. RR )
32 31 recnd 
 |-  ( ph -> sum_ k e. A ( B x. C ) e. CC )
33 32 abscld 
 |-  ( ph -> ( abs ` sum_ k e. A ( B x. C ) ) e. RR )
34 31 leabsd 
 |-  ( ph -> sum_ k e. A ( B x. C ) <_ ( abs ` sum_ k e. A ( B x. C ) ) )
35 1 2 3 csbren 
 |-  ( ph -> ( sum_ k e. A ( B x. C ) ^ 2 ) <_ ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) )
36 absresq 
 |-  ( sum_ k e. A ( B x. C ) e. RR -> ( ( abs ` sum_ k e. A ( B x. C ) ) ^ 2 ) = ( sum_ k e. A ( B x. C ) ^ 2 ) )
37 31 36 syl 
 |-  ( ph -> ( ( abs ` sum_ k e. A ( B x. C ) ) ^ 2 ) = ( sum_ k e. A ( B x. C ) ^ 2 ) )
38 resqrtth 
 |-  ( ( ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) e. RR /\ 0 <_ ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) -> ( ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ^ 2 ) = ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) )
39 14 19 38 syl2anc 
 |-  ( ph -> ( ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ^ 2 ) = ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) )
40 35 37 39 3brtr4d 
 |-  ( ph -> ( ( abs ` sum_ k e. A ( B x. C ) ) ^ 2 ) <_ ( ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ^ 2 ) )
41 32 absge0d 
 |-  ( ph -> 0 <_ ( abs ` sum_ k e. A ( B x. C ) ) )
42 14 19 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) )
43 33 20 41 42 le2sqd 
 |-  ( ph -> ( ( abs ` sum_ k e. A ( B x. C ) ) <_ ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) <-> ( ( abs ` sum_ k e. A ( B x. C ) ) ^ 2 ) <_ ( ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ^ 2 ) ) )
44 40 43 mpbird 
 |-  ( ph -> ( abs ` sum_ k e. A ( B x. C ) ) <_ ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) )
45 31 33 20 34 44 letrd 
 |-  ( ph -> sum_ k e. A ( B x. C ) <_ ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) )
46 5 a1i 
 |-  ( ph -> 2 e. RR )
47 2pos 
 |-  0 < 2
48 47 a1i 
 |-  ( ph -> 0 < 2 )
49 lemul2 
 |-  ( ( sum_ k e. A ( B x. C ) e. RR /\ ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( sum_ k e. A ( B x. C ) <_ ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) <-> ( 2 x. sum_ k e. A ( B x. C ) ) <_ ( 2 x. ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ) ) )
50 31 20 46 48 49 syl112anc 
 |-  ( ph -> ( sum_ k e. A ( B x. C ) <_ ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) <-> ( 2 x. sum_ k e. A ( B x. C ) ) <_ ( 2 x. ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ) ) )
51 45 50 mpbid 
 |-  ( ph -> ( 2 x. sum_ k e. A ( B x. C ) ) <_ ( 2 x. ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ) )
52 30 51 eqbrtrrd 
 |-  ( ph -> sum_ k e. A ( 2 x. ( B x. C ) ) <_ ( 2 x. ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ) )
53 27 22 11 52 leadd2dd 
 |-  ( ph -> ( sum_ k e. A ( B ^ 2 ) + sum_ k e. A ( 2 x. ( B x. C ) ) ) <_ ( sum_ k e. A ( B ^ 2 ) + ( 2 x. ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ) ) )
54 26 53 eqbrtrd 
 |-  ( ph -> sum_ k e. A ( ( B ^ 2 ) + ( 2 x. ( B x. C ) ) ) <_ ( sum_ k e. A ( B ^ 2 ) + ( 2 x. ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ) ) )
55 10 23 13 54 leadd1dd 
 |-  ( ph -> ( sum_ k e. A ( ( B ^ 2 ) + ( 2 x. ( B x. C ) ) ) + sum_ k e. A ( C ^ 2 ) ) <_ ( ( sum_ k e. A ( B ^ 2 ) + ( 2 x. ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ) ) + sum_ k e. A ( C ^ 2 ) ) )
56 2 3 readdcld 
 |-  ( ( ph /\ k e. A ) -> ( B + C ) e. RR )
57 56 resqcld 
 |-  ( ( ph /\ k e. A ) -> ( ( B + C ) ^ 2 ) e. RR )
58 1 57 fsumrecl 
 |-  ( ph -> sum_ k e. A ( ( B + C ) ^ 2 ) e. RR )
59 56 sqge0d 
 |-  ( ( ph /\ k e. A ) -> 0 <_ ( ( B + C ) ^ 2 ) )
60 1 57 59 fsumge0 
 |-  ( ph -> 0 <_ sum_ k e. A ( ( B + C ) ^ 2 ) )
61 resqrtth 
 |-  ( ( sum_ k e. A ( ( B + C ) ^ 2 ) e. RR /\ 0 <_ sum_ k e. A ( ( B + C ) ^ 2 ) ) -> ( ( sqrt ` sum_ k e. A ( ( B + C ) ^ 2 ) ) ^ 2 ) = sum_ k e. A ( ( B + C ) ^ 2 ) )
62 58 60 61 syl2anc 
 |-  ( ph -> ( ( sqrt ` sum_ k e. A ( ( B + C ) ^ 2 ) ) ^ 2 ) = sum_ k e. A ( ( B + C ) ^ 2 ) )
63 2 recnd 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
64 3 recnd 
 |-  ( ( ph /\ k e. A ) -> C e. CC )
65 binom2 
 |-  ( ( B e. CC /\ C e. CC ) -> ( ( B + C ) ^ 2 ) = ( ( ( B ^ 2 ) + ( 2 x. ( B x. C ) ) ) + ( C ^ 2 ) ) )
66 63 64 65 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( ( B + C ) ^ 2 ) = ( ( ( B ^ 2 ) + ( 2 x. ( B x. C ) ) ) + ( C ^ 2 ) ) )
67 66 sumeq2dv 
 |-  ( ph -> sum_ k e. A ( ( B + C ) ^ 2 ) = sum_ k e. A ( ( ( B ^ 2 ) + ( 2 x. ( B x. C ) ) ) + ( C ^ 2 ) ) )
68 9 recnd 
 |-  ( ( ph /\ k e. A ) -> ( ( B ^ 2 ) + ( 2 x. ( B x. C ) ) ) e. CC )
69 12 recnd 
 |-  ( ( ph /\ k e. A ) -> ( C ^ 2 ) e. CC )
70 1 68 69 fsumadd 
 |-  ( ph -> sum_ k e. A ( ( ( B ^ 2 ) + ( 2 x. ( B x. C ) ) ) + ( C ^ 2 ) ) = ( sum_ k e. A ( ( B ^ 2 ) + ( 2 x. ( B x. C ) ) ) + sum_ k e. A ( C ^ 2 ) ) )
71 67 70 eqtrd 
 |-  ( ph -> sum_ k e. A ( ( B + C ) ^ 2 ) = ( sum_ k e. A ( ( B ^ 2 ) + ( 2 x. ( B x. C ) ) ) + sum_ k e. A ( C ^ 2 ) ) )
72 62 71 eqtrd 
 |-  ( ph -> ( ( sqrt ` sum_ k e. A ( ( B + C ) ^ 2 ) ) ^ 2 ) = ( sum_ k e. A ( ( B ^ 2 ) + ( 2 x. ( B x. C ) ) ) + sum_ k e. A ( C ^ 2 ) ) )
73 11 16 resqrtcld 
 |-  ( ph -> ( sqrt ` sum_ k e. A ( B ^ 2 ) ) e. RR )
74 73 recnd 
 |-  ( ph -> ( sqrt ` sum_ k e. A ( B ^ 2 ) ) e. CC )
75 13 18 resqrtcld 
 |-  ( ph -> ( sqrt ` sum_ k e. A ( C ^ 2 ) ) e. RR )
76 75 recnd 
 |-  ( ph -> ( sqrt ` sum_ k e. A ( C ^ 2 ) ) e. CC )
77 binom2 
 |-  ( ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) e. CC /\ ( sqrt ` sum_ k e. A ( C ^ 2 ) ) e. CC ) -> ( ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) + ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ) ^ 2 ) = ( ( ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) ^ 2 ) + ( 2 x. ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) x. ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ) ) ) + ( ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ^ 2 ) ) )
78 74 76 77 syl2anc 
 |-  ( ph -> ( ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) + ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ) ^ 2 ) = ( ( ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) ^ 2 ) + ( 2 x. ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) x. ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ) ) ) + ( ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ^ 2 ) ) )
79 resqrtth 
 |-  ( ( sum_ k e. A ( B ^ 2 ) e. RR /\ 0 <_ sum_ k e. A ( B ^ 2 ) ) -> ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) ^ 2 ) = sum_ k e. A ( B ^ 2 ) )
80 11 16 79 syl2anc 
 |-  ( ph -> ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) ^ 2 ) = sum_ k e. A ( B ^ 2 ) )
81 11 16 13 18 sqrtmuld 
 |-  ( ph -> ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) = ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) x. ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ) )
82 81 eqcomd 
 |-  ( ph -> ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) x. ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ) = ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) )
83 82 oveq2d 
 |-  ( ph -> ( 2 x. ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) x. ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ) ) = ( 2 x. ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ) )
84 80 83 oveq12d 
 |-  ( ph -> ( ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) ^ 2 ) + ( 2 x. ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) x. ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ) ) ) = ( sum_ k e. A ( B ^ 2 ) + ( 2 x. ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ) ) )
85 resqrtth 
 |-  ( ( sum_ k e. A ( C ^ 2 ) e. RR /\ 0 <_ sum_ k e. A ( C ^ 2 ) ) -> ( ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ^ 2 ) = sum_ k e. A ( C ^ 2 ) )
86 13 18 85 syl2anc 
 |-  ( ph -> ( ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ^ 2 ) = sum_ k e. A ( C ^ 2 ) )
87 84 86 oveq12d 
 |-  ( ph -> ( ( ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) ^ 2 ) + ( 2 x. ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) x. ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ) ) ) + ( ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ^ 2 ) ) = ( ( sum_ k e. A ( B ^ 2 ) + ( 2 x. ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ) ) + sum_ k e. A ( C ^ 2 ) ) )
88 78 87 eqtrd 
 |-  ( ph -> ( ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) + ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ) ^ 2 ) = ( ( sum_ k e. A ( B ^ 2 ) + ( 2 x. ( sqrt ` ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) ) ) ) + sum_ k e. A ( C ^ 2 ) ) )
89 55 72 88 3brtr4d 
 |-  ( ph -> ( ( sqrt ` sum_ k e. A ( ( B + C ) ^ 2 ) ) ^ 2 ) <_ ( ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) + ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ) ^ 2 ) )
90 58 60 resqrtcld 
 |-  ( ph -> ( sqrt ` sum_ k e. A ( ( B + C ) ^ 2 ) ) e. RR )
91 73 75 readdcld 
 |-  ( ph -> ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) + ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ) e. RR )
92 58 60 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` sum_ k e. A ( ( B + C ) ^ 2 ) ) )
93 11 16 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` sum_ k e. A ( B ^ 2 ) ) )
94 13 18 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` sum_ k e. A ( C ^ 2 ) ) )
95 73 75 93 94 addge0d 
 |-  ( ph -> 0 <_ ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) + ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ) )
96 90 91 92 95 le2sqd 
 |-  ( ph -> ( ( sqrt ` sum_ k e. A ( ( B + C ) ^ 2 ) ) <_ ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) + ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ) <-> ( ( sqrt ` sum_ k e. A ( ( B + C ) ^ 2 ) ) ^ 2 ) <_ ( ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) + ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ) ^ 2 ) ) )
97 89 96 mpbird 
 |-  ( ph -> ( sqrt ` sum_ k e. A ( ( B + C ) ^ 2 ) ) <_ ( ( sqrt ` sum_ k e. A ( B ^ 2 ) ) + ( sqrt ` sum_ k e. A ( C ^ 2 ) ) ) )