Theorem abstri

Description: Triangle inequality for absolute value. Proposition 10-3.7(h) of Gleason p. 133. (Contributed by NM, 7-Mar-2005) (Proof shortened by Mario Carneiro, 29-May-2016)

	Ref	Expression
Assertion	abstri	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|A+B\right|\le \left|A\right|+\left|B\right|$$

Proof

Step	Hyp	Ref	Expression
1		2re	$$⊢2\in ℝ$$
2	1	a1i	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 2\in ℝ$$
3		simpl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A\in ℂ$$
4		simpr	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to B\in ℂ$$
5	4	cjcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \bar{B}\in ℂ$$
6	3 5	mulcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A\bar{B}\in ℂ$$
7	6	recld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \Re \left(A\bar{B}\right)\in ℝ$$
8	2 7	remulcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 2\Re \left(A\bar{B}\right)\in ℝ$$
9		abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$
10	3 9	syl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|A\right|\in ℝ$$
11		abscl	$$⊢B\in ℂ\to \left|B\right|\in ℝ$$
12	4 11	syl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|B\right|\in ℝ$$
13	10 12	remulcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|A\right|\left|B\right|\in ℝ$$
14	2 13	remulcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 2\left|A\right|\left|B\right|\in ℝ$$
15	10	resqcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left|A\right|}^2\in ℝ$$
16	12	resqcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left|B\right|}^2\in ℝ$$
17	15 16	readdcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left|A\right|}^2+{\left|B\right|}^2\in ℝ$$
18		releabs	$$⊢A\bar{B}\in ℂ\to \Re \left(A\bar{B}\right)\le \left|A\bar{B}\right|$$
19	6 18	syl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \Re \left(A\bar{B}\right)\le \left|A\bar{B}\right|$$
20		absmul	$$⊢\left(A\in ℂ\wedge \bar{B}\in ℂ\right)\to \left|A\bar{B}\right|=\left|A\right|\left|\bar{B}\right|$$
21	3 5 20	syl2anc	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|A\bar{B}\right|=\left|A\right|\left|\bar{B}\right|$$
22		abscj	$$⊢B\in ℂ\to \left|\bar{B}\right|=\left|B\right|$$
23	4 22	syl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|\bar{B}\right|=\left|B\right|$$
24	23	oveq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|A\right|\left|\bar{B}\right|=\left|A\right|\left|B\right|$$
25	21 24	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|A\bar{B}\right|=\left|A\right|\left|B\right|$$
26	19 25	breqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \Re \left(A\bar{B}\right)\le \left|A\right|\left|B\right|$$
27		2rp	$$⊢2\in {ℝ}^{+}$$
28	27	a1i	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 2\in {ℝ}^{+}$$
29	7 13 28	lemul2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(\Re \left(A\bar{B}\right)\le \left|A\right|\left|B\right|\leftrightarrow 2\Re \left(A\bar{B}\right)\le 2\left|A\right|\left|B\right|\right)$$
30	26 29	mpbid	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 2\Re \left(A\bar{B}\right)\le 2\left|A\right|\left|B\right|$$
31	8 14 17 30	leadd2dd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left|A\right|}^2+{\left|B\right|}^2+2\Re \left(A\bar{B}\right)\le {\left|A\right|}^2+{\left|B\right|}^2+2\left|A\right|\left|B\right|$$
32		sqabsadd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left|A+B\right|}^2={\left|A\right|}^2+{\left|B\right|}^2+2\Re \left(A\bar{B}\right)$$
33	10	recnd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|A\right|\in ℂ$$
34	12	recnd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|B\right|\in ℂ$$
35		binom2	$$⊢\left(\left|A\right|\in ℂ\wedge \left|B\right|\in ℂ\right)\to {\left(\left|A\right|+\left|B\right|\right)}^2={\left|A\right|}^2+2\left|A\right|\left|B\right|+{\left|B\right|}^2$$
36	33 34 35	syl2anc	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left(\left|A\right|+\left|B\right|\right)}^2={\left|A\right|}^2+2\left|A\right|\left|B\right|+{\left|B\right|}^2$$
37	15	recnd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left|A\right|}^2\in ℂ$$
38	14	recnd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 2\left|A\right|\left|B\right|\in ℂ$$
39	16	recnd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left|B\right|}^2\in ℂ$$
40	37 38 39	add32d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left|A\right|}^2+2\left|A\right|\left|B\right|+{\left|B\right|}^2={\left|A\right|}^2+{\left|B\right|}^2+2\left|A\right|\left|B\right|$$
41	36 40	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left(\left|A\right|+\left|B\right|\right)}^2={\left|A\right|}^2+{\left|B\right|}^2+2\left|A\right|\left|B\right|$$
42	31 32 41	3brtr4d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left|A+B\right|}^2\le {\left(\left|A\right|+\left|B\right|\right)}^2$$
43		addcl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B\in ℂ$$
44		abscl	$$⊢A+B\in ℂ\to \left|A+B\right|\in ℝ$$
45	43 44	syl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|A+B\right|\in ℝ$$
46	10 12	readdcld	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|A\right|+\left|B\right|\in ℝ$$
47		absge0	$$⊢A+B\in ℂ\to 0\le \left|A+B\right|$$
48	43 47	syl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 0\le \left|A+B\right|$$
49		absge0	$$⊢A\in ℂ\to 0\le \left|A\right|$$
50	3 49	syl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 0\le \left|A\right|$$
51		absge0	$$⊢B\in ℂ\to 0\le \left|B\right|$$
52	4 51	syl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 0\le \left|B\right|$$
53	10 12 50 52	addge0d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 0\le \left|A\right|+\left|B\right|$$
54	45 46 48 53	le2sqd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(\left|A+B\right|\le \left|A\right|+\left|B\right|\leftrightarrow {\left|A+B\right|}^2\le {\left(\left|A\right|+\left|B\right|\right)}^2\right)$$
55	42 54	mpbird	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left|A+B\right|\le \left|A\right|+\left|B\right|$$