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