trirni - Mathbox for Jeff Madsen

Mathbox for Jeff Madsen

< Previous Next >
Related theorems
Unicode version

Theorem trirni 15833

Description: Triangle inequality in R^n.

**Hypotheses**
Ref	Expression
trirni.1
trirni.2
trirni.3

**Assertion**
Ref	Expression
trirni

Distinct variable groups:

**Proof of Theorem trirni**
Step	Hyp	Ref	Expression
1		trirni.1	. . . . . . . . . . 11
2		elnnuz 7609	. . . . . . . . . . 11
3	1, 2	mpbi 206	. . . . . . . . . 10
4		trirni.2	. . . . . . . . . . . . 13
5	4	ffvelrni 4788	. . . . . . . . . . . 12
6		trirni.3	. . . . . . . . . . . . 13
7	6	ffvelrni 4788	. . . . . . . . . . . 12
8		remulcl 6457	. . . . . . . . . . . 12 $/\$
9	5, 7, 8	syl11anc 524	. . . . . . . . . . 11
10	9	rgen 2159	. . . . . . . . . 10
11		fsumrecl 8277	. . . . . . . . . 10 $/\$
12	3, 10, 11	mp2an 761	. . . . . . . . 9
13	12	leabsi 8124	. . . . . . . 8
14	1, 4, 6	csbrni 15832	. . . . . . . . . 10
15		absresq 8118	. . . . . . . . . . 11
16	12, 15	ax-mp 7	. . . . . . . . . 10
17		reexpcl 7823	. . . . . . . . . . . . . . . 16 $/\$
18		2nn0 7324	. . . . . . . . . . . . . . . 16
19	17, 5, 18	sylancl 525	. . . . . . . . . . . . . . 15
20		sqge0 7878	. . . . . . . . . . . . . . . 16
21	5, 20	syl 12	. . . . . . . . . . . . . . 15
22	19, 21	jca 310	. . . . . . . . . . . . . 14 $/\$
23	22	rgen 2159	. . . . . . . . . . . . 13 $/\$
24		fsumcmp0 8301	. . . . . . . . . . . . 13 $/\$ $/\$
25	3, 23, 24	mp2an 761	. . . . . . . . . . . 12
26		reexpcl 7823	. . . . . . . . . . . . . . . 16 $/\$
27	26, 7, 18	sylancl 525	. . . . . . . . . . . . . . 15
28		sqge0 7878	. . . . . . . . . . . . . . . 16
29	7, 28	syl 12	. . . . . . . . . . . . . . 15
30	27, 29	jca 310	. . . . . . . . . . . . . 14 $/\$
31	30	rgen 2159	. . . . . . . . . . . . 13 $/\$
32		fsumcmp0 8301	. . . . . . . . . . . . 13 $/\$ $/\$
33	3, 31, 32	mp2an 761	. . . . . . . . . . . 12
34	19	rgen 2159	. . . . . . . . . . . . . 14
35		fsumrecl 8277	. . . . . . . . . . . . . 14 $/\$
36	3, 34, 35	mp2an 761	. . . . . . . . . . . . 13
37	27	rgen 2159	. . . . . . . . . . . . . 14
38		fsumrecl 8277	. . . . . . . . . . . . . 14 $/\$
39	3, 37, 38	mp2an 761	. . . . . . . . . . . . 13
40	36, 39	mulge0i 6787	. . . . . . . . . . . 12 $/\$
41	25, 33, 40	mp2an 761	. . . . . . . . . . 11
42	36, 39	remulcli 6488	. . . . . . . . . . . 12
43	42	sqsqri 7971	. . . . . . . . . . 11
44	41, 43	ax-mp 7	. . . . . . . . . 10
45	14, 16, 44	3brtr4i 3365	. . . . . . . . 9
46	12	recni 6467	. . . . . . . . . . 11
47	46	absge0i 8091	. . . . . . . . . 10
48	42	sqrge0i 7952	. . . . . . . . . . 11
49	41, 48	ax-mp 7	. . . . . . . . . 10
50	46	abscli 8090	. . . . . . . . . . 11
51	42	sqrcli 7950	. . . . . . . . . . . 12
52	41, 51	ax-mp 7	. . . . . . . . . . 11
53	50, 52	le2sqi 7870	. . . . . . . . . 10 $/\$
54	47, 49, 53	mp2an 761	. . . . . . . . 9
55	45, 54	mpbir 207	. . . . . . . 8
56	12, 50, 52	letri 6763	. . . . . . . 8 $/\$
57	13, 55, 56	mp2an 761	. . . . . . 7
58		2pos 7173	. . . . . . . 8
59		2re 7163	. . . . . . . . 9
60	12, 52, 59	lemul2i 7018	. . . . . . . 8
61	58, 60	ax-mp 7	. . . . . . 7
62	57, 61	mpbi 206	. . . . . 6
63		2cn 7164	. . . . . . 7
64	5	recnd 6468	. . . . . . . . 9
65	7	recnd 6468	. . . . . . . . 9
66		mulcl 6456	. . . . . . . . 9 $/\$
67	64, 65, 66	syl11anc 524	. . . . . . . 8
68	67	rgen 2159	. . . . . . 7
69		fsummulc1 8293	. . . . . . 7 $/\$ $/\$
70	3, 63, 68, 69	mp3an 1191	. . . . . 6
71	36, 39, 25, 33	sqrmulii 7954	. . . . . . 7
72	71	opreq2i 4893	. . . . . 6
73	62, 70, 72	3brtr3i 3364	. . . . 5
74		remulcl 6457	. . . . . . . . 9 $/\$
75	74, 59, 9	sylancr 526	. . . . . . . 8
76	75	rgen 2159	. . . . . . 7
77		fsumrecl 8277	. . . . . . 7 $/\$
78	3, 76, 77	mp2an 761	. . . . . 6
79	36	sqrcli 7950	. . . . . . . . 9
80	25, 79	ax-mp 7	. . . . . . . 8
81	39	sqrcli 7950	. . . . . . . . 9
82	33, 81	ax-mp 7	. . . . . . . 8
83	80, 82	remulcli 6488	. . . . . . 7
84	59, 83	remulcli 6488	. . . . . 6
85	78, 84, 36	leadd2i 6768	. . . . 5
86	73, 85	mpbi 206	. . . 4
87	36, 78	readdcli 6487	. . . . 5
88	36, 84	readdcli 6487	. . . . 5
89	87, 88, 39	leadd1i 6767	. . . 4
90	86, 89	mpbi 206	. . 3
91		reexpcl 7823	. . . . . . . . 9 $/\$
92		readdcl 6455	. . . . . . . . . 10 $/\$
93	5, 7, 92	syl11anc 524	. . . . . . . . 9
94	91, 93, 18	sylancl 525	. . . . . . . 8
95		sqge0 7878	. . . . . . . . 9
96	93, 95	syl 12	. . . . . . . 8
97	94, 96	jca 310	. . . . . . 7 $/\$
98	97	rgen 2159	. . . . . 6 $/\$
99		fsumcmp0 8301	. . . . . 6 $/\$ $/\$
100	3, 98, 99	mp2an 761	. . . . 5
101	94	rgen 2159	. . . . . . 7
102		fsumrecl 8277	. . . . . . 7 $/\$
103	3, 101, 102	mp2an 761	. . . . . 6
104	103	sqsqri 7971	. . . . 5
105	100, 104	ax-mp 7	. . . 4
106		binom2 7896	. . . . . 6 $/\$
107	64, 65, 106	syl11anc 524	. . . . 5
108	107	sumeq2i 8248	. . . 4
109	19	recnd 6468	. . . . . . . . 9
110		mulcl 6456	. . . . . . . . . 10 $/\$
111	110, 63, 67	sylancr 526	. . . . . . . . 9
112		addcl 6454	. . . . . . . . 9 $/\$
113	109, 111, 112	syl11anc 524	. . . . . . . 8
114	27	recnd 6468	. . . . . . . 8
115	113, 114	jca 310	. . . . . . 7 $/\$
116	115	rgen 2159	. . . . . 6 $/\$
117		fsumadd 8282	. . . . . 6 $/\$ $/\$
118	3, 116, 117	mp2an 761	. . . . 5
119	109, 111	jca 310	. . . . . . . 8 $/\$
120	119	rgen 2159	. . . . . . 7 $/\$
121		fsumadd 8282	. . . . . . 7 $/\$ $/\$
122	3, 120, 121	mp2an 761	. . . . . 6
123	122	opreq1i 4892	. . . . 5
124	118, 123	eqtri 1908	. . . 4
125	105, 108, 124	3eqtri 1912	. . 3
126	80	recni 6467	. . . . 5
127	82	recni 6467	. . . . 5
128	126, 127	binom2i 7890	. . . 4
129	36	sqsqri 7971	. . . . . . 7
130	25, 129	ax-mp 7	. . . . . 6
131	130	opreq1i 4892	. . . . 5
132	39	sqsqri 7971	. . . . . 6
133	33, 132	ax-mp 7	. . . . 5
134	131, 133	opreq12i 4894	. . . 4
135	128, 134	eqtri 1908	. . 3
136	90, 125, 135	3brtr4i 3365	. 2
137	103	sqrge0i 7952	. . . 4
138	100, 137	ax-mp 7	. . 3
139	36	sqrge0i 7952	. . . . 5
140	25, 139	ax-mp 7	. . . 4
141	39	sqrge0i 7952	. . . . 5
142	33, 141	ax-mp 7	. . . 4
143	80, 82	addge0i 6777	. . . 4 $/\$
144	140, 142, 143	mp2an 761	. . 3
145	103	sqrcli 7950	. . . . 5
146	100, 145	ax-mp 7	. . . 4
147	80, 82	readdcli 6487	. . . 4
148	146, 147	le2sqi 7870	. . 3 $/\$
149	138, 144, 148	mp2an 761	. 2
150	136, 149	mpbir 207	1

Colors of variables: wff set class

Syntax hints:

wb 163 $/\$ wa 240

wceq 1298

wcel 1300

wral 2105 class class class wbr 3338

wf 3994

cfv 3998 (class class class)co 4884

cc 6384

cr 6385

cc0 6386

c1 6387

caddc 6389

cmul 6391

cle 6448

cn 6449

cn0 6450

clt 6653

c2 7145

cuz 7586

cfz 7637

cexp 7811

csqr 7919

cabs 8000

csu 8239

This theorem is referenced by: trirn 15834

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-5 1302 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-rep 3428 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790 ax-inf2 5731

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-nel 2020 df-ral 2109 df-rex 2110 df-reu 2111 df-rab 2112 df-v 2294 df-sbc 2454 df-csb 2541 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-pss 2607 df-nul 2876 df-if 2983 df-pw 3035 df-sn 3049 df-pr 3050 df-tp 3052 df-op 3053 df-uni 3178 df-int 3215 df-iun 3257 df-br 3339 df-opab 3396 df-tr 3412 df-eprel 3583 df-id 3586 df-po 3591 df-so 3604 df-fr 3625 df-we 3644 df-ord 3660 df-on 3661 df-lim 3662 df-suc 3663 df-om 3950 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-f 4010 df-f1 4011 df-fo 4012 df-f1o 4013 df-fv 4014 df-opr 4886 df-oprab 4887 df-mpt 5006 df-1st 5020 df-2nd 5021 df-iota 5089 df-rdg 5140 df-1o 5177 df-oadd 5179 df-omul 5180 df-er 5318 df-ec 5320 df-qs 5323 df-en 5427 df-dom 5428 df-sdom 5429 df-undef 5556 df-riota 5560 df-sup 5664 df-ni 6152 df-pli 6153 df-mi 6154 df-lti 6155 df-plpq 6187 df-mpq 6188 df-enq 6189 df-nq 6190 df-plq 6191 df-mq 6192 df-rq 6193 df-ltq 6194 df-1q 6195 df-np 6238 df-1p 6239 df-plp 6240 df-mp 6241 df-ltp 6242 df-plpr 6316 df-mpr 6317 df-enr 6318 df-nr 6319 df-plr 6320 df-mr 6321 df-ltr 6322 df-0r 6323 df-1r 6324 df-m1r 6325 df-c 6392 df-0 6393 df-1 6394 df-i 6395 df-r 6396 df-plus 6397 df-mul 6398 df-lt 6399 df-sub 6511 df-neg 6513 df-pnf 6654 df-mnf 6655 df-xr 6656 df-ltxr 6657 df-le 6658 df-div 6892 df-n 7108 df-2 7154 df-3 7155 df-4 7156 df-n0 7309 df-z 7345 df-uz 7587 df-fz 7638 df-seq1 7721 df-shft 7754 df-seqz 7776 df-exp 7812 df-sqr 7920 df-re 8001 df-im 8002 df-cj 8003 df-abs 8004 df-sum 8240