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 BC\in ℝ$$
7		remulcl	$$⊢\left(2\in ℝ\wedge BC\in ℝ\right)\to 2BC\in ℝ$$
8	5 6 7	sylancr	$$⊢\left(\phi \wedge k\in A\right)\to 2BC\in ℝ$$
9	4 8	readdcld	$$⊢\left(\phi \wedge k\in A\right)\to B^2+2BC\in ℝ$$
10	1 9	fsumrecl	$$⊢\phi \to \sum _{k\in A}\left(B^2+2BC\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 2BC\in ℂ$$
26	1 24 25	fsumadd	$$⊢\phi \to \sum _{k\in A}\left(B^2+2BC\right)=\sum _{k\in A}{B}^2+\sum _{k\in A}2BC$$
27	1 8	fsumrecl	$$⊢\phi \to \sum _{k\in A}2BC\in ℝ$$
28		2cnd	$$⊢\phi \to 2\in ℂ$$
29	6	recnd	$$⊢\left(\phi \wedge k\in A\right)\to BC\in ℂ$$
30	1 28 29	fsummulc2	$$⊢\phi \to 2\sum _{k\in A}BC=\sum _{k\in A}2BC$$
31	1 6	fsumrecl	$$⊢\phi \to \sum _{k\in A}BC\in ℝ$$
32	31	recnd	$$⊢\phi \to \sum _{k\in A}BC\in ℂ$$
33	32	abscld	$$⊢\phi \to \left|\sum _{k\in A}BC\right|\in ℝ$$
34	31	leabsd	$$⊢\phi \to \sum _{k\in A}BC\le \left|\sum _{k\in A}BC\right|$$
35	1 2 3	csbren	$$⊢\phi \to {\sum _{k\in A}BC}^2\le \sum _{k\in A}{B}^2\sum _{k\in A}{C}^2$$
36		absresq	$$⊢\sum _{k\in A}BC\in ℝ\to {\left|\sum _{k\in A}BC\right|}^2={\sum _{k\in A}BC}^2$$
37	31 36	syl	$$⊢\phi \to {\left|\sum _{k\in A}BC\right|}^2={\sum _{k\in A}BC}^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}BC\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}BC\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}BC\right|\le \sqrt{\sum _{k\in A}{B}^2\sum _{k\in A}{C}^2}\leftrightarrow {\left|\sum _{k\in A}BC\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}BC\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}BC\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}BC\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}BC\le \sqrt{\sum _{k\in A}{B}^2\sum _{k\in A}{C}^2}\leftrightarrow 2\sum _{k\in A}BC\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}BC\le \sqrt{\sum _{k\in A}{B}^2\sum _{k\in A}{C}^2}\leftrightarrow 2\sum _{k\in A}BC\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}BC\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}2BC\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}2BC\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+2BC\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+2BC\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+2BC+C^2$$
66	63 64 65	syl2anc	$$⊢\left(\phi \wedge k\in A\right)\to {\left(B+C\right)}^2=B^2+2BC+C^2$$
67	66	sumeq2dv	$$⊢\phi \to \sum _{k\in A}{\left(B+C\right)}^2=\sum _{k\in A}\left(B^2+2BC+C^2\right)$$
68	9	recnd	$$⊢\left(\phi \wedge k\in A\right)\to B^2+2BC\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+2BC+C^2\right)=\sum _{k\in A}\left(B^2+2BC\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+2BC\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+2BC\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}\leftrightarrow {\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}$$