Theorem abstri 8535

Description: Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133.

Assertion

Ref	Expression
abstri	|- ((A e. CC /\ B e. CC) -> (abs` (A + B)) <_ ((abs` A) + (abs` B)))

Proof of Theorem abstri

Step	Hyp	Ref	Expression
1		opreq1 4986	. . . 4 |- (A = if(A e. CC, A, 0) -> (A + B) = (if(A e. CC, A, 0) + B))
2	1	fveq2d 4769	. . 3 |- (A = if(A e. CC, A, 0) -> (abs` (A + B)) = (abs` (if(A e. CC, A, 0) + B)))
3		fveq2 4765	. . . 4 |- (A = if(A e. CC, A, 0) -> (abs` A) = (abs` if(A e. CC, A, 0)))
4	3	opreq1d 4993	. . 3 |- (A = if(A e. CC, A, 0) -> ((abs` A) + (abs` B)) = ((abs` if(A e. CC, A, 0)) + (abs` B)))
5	2, 4	breq12d 3520	. 2 |- (A = if(A e. CC, A, 0) -> ((abs` (A + B)) <_ ((abs` A) + (abs` B)) <-> (abs` (if(A e. CC, A, 0) + B)) <_ ((abs` if(A e. CC, A, 0)) + (abs` B))))
6		opreq2 4987	. . . 4 |- (B = if(B e. CC, B, 0) -> (if(A e. CC, A, 0) + B) = (if(A e. CC, A, 0) + if(B e. CC, B, 0)))
7	6	fveq2d 4769	. . 3 |- (B = if(B e. CC, B, 0) -> (abs` (if(A e. CC, A, 0) + B)) = (abs` (if(A e. CC, A, 0) + if(B e. CC, B, 0))))
8		fveq2 4765	. . . 4 |- (B = if(B e. CC, B, 0) -> (abs` B) = (abs` if(B e. CC, B, 0)))
9	8	opreq2d 4994	. . 3 |- (B = if(B e. CC, B, 0) -> ((abs` if(A e. CC, A, 0)) + (abs` B)) = ((abs` if(A e. CC, A, 0)) + (abs` if(B e. CC, B, 0))))
10	7, 9	breq12d 3520	. 2 |- (B = if(B e. CC, B, 0) -> ((abs` (if(A e. CC, A, 0) + B)) <_ ((abs` if(A e. CC, A, 0)) + (abs` B)) <-> (abs` (if(A e. CC, A, 0) + if(B e. CC, B, 0))) <_ ((abs` if(A e. CC, A, 0)) + (abs` if(B e. CC, B, 0)))))
11		0cn 6831	. . . 4 |- 0 e. CC
12	11	elimel 3219	. . 3 |- if(A e. CC, A, 0) e. CC
13	11	elimel 3219	. . 3 |- if(B e. CC, B, 0) e. CC
14	12, 13	abstrii 8527	. 2 |- (abs` (if(A e. CC, A, 0) + if(B e. CC, B, 0))) <_ ((abs` if(A e. CC, A, 0)) + (abs` if(B e. CC, B, 0)))
15	5, 10, 14	dedth2h 3209	1 |- ((A e. CC /\ B e. CC) -> (abs` (A + B)) <_ ((abs` A) + (abs` B)))

Syntax hints:   -> wi 3   /\ wa 337   = wceq 1586   e. wcel 1588  ifcif 3180   class class class wbr 3507  ` cfv 4131  (class class class)co 4981  CCcc 6750  0cc0 6752   + caddc 6755   <_ cle 6841  abscabs 8384

This theorem is referenced by:  abs3dif 8536  caubndi 8563  ser1absdiflem 8566  fsumabs 8699  2climnn 8758  2climnn0 8759  climaddlem3 8772  climmullem3 8778  climmullem5 8780  climcaui 8812  caucvgi 8819  serzf0i 8825  cnnv 10508

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-nel 2269  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-mpt 5099  df-1st 5126  df-2nd 5127  df-iota 5219  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-en 5588  df-dom 5589  df-sdom 5590  df-undef 5725  df-riota 5729  df-sup 5888  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-mp 6607  df-ltp 6608  df-plpr 6682  df-mpr 6683  df-enr 6684  df-nr 6685  df-plr 6686  df-mr 6687  df-ltr 6688  df-0r 6689  df-1r 6690  df-m1r 6691  df-c 6758  df-0 6759  df-1 6760  df-i 6761  df-r 6762  df-plus 6763  df-mul 6764  df-lt 6765  df-pnf 6846  df-mnf 6847  df-xr 6848  df-ltxr 6849  df-le 6850  df-sub 7009  df-neg 7011  df-div 7223  df-n 7441  df-2 7487  df-n0 7649  df-z 7686  df-seq1 8094  df-exp 8196  df-sqr 8304  df-re 8385  df-im 8386  df-cj 8387  df-abs 8388

Copyright terms: Public domain