MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexadd Structured version   Visualization version   Unicode version

Theorem rexadd 11554
Description: The extended real addition operation when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
rexadd  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A +e
B )  =  ( A  +  B ) )

Proof of Theorem rexadd
StepHypRef Expression
1 rexr 9712 . . 3  |-  ( A  e.  RR  ->  A  e.  RR* )
2 rexr 9712 . . 3  |-  ( B  e.  RR  ->  B  e.  RR* )
3 xaddval 11545 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A +e B )  =  if ( A  = +oo ,  if ( B  = -oo ,  0 , +oo ) ,  if ( A  = -oo ,  if ( B  = +oo ,  0 , -oo ) ,  if ( B  = +oo , +oo ,  if ( B  = -oo , -oo , 
( A  +  B
) ) ) ) ) )
41, 2, 3syl2an 484 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A +e
B )  =  if ( A  = +oo ,  if ( B  = -oo ,  0 , +oo ) ,  if ( A  = -oo ,  if ( B  = +oo ,  0 , -oo ) ,  if ( B  = +oo , +oo ,  if ( B  = -oo , -oo ,  ( A  +  B ) ) ) ) ) )
5 renepnf 9714 . . . . 5  |-  ( A  e.  RR  ->  A  =/= +oo )
6 ifnefalse 3905 . . . . 5  |-  ( A  =/= +oo  ->  if ( A  = +oo ,  if ( B  = -oo ,  0 , +oo ) ,  if ( A  = -oo ,  if ( B  = +oo ,  0 , -oo ) ,  if ( B  = +oo , +oo ,  if ( B  = -oo , -oo , 
( A  +  B
) ) ) ) )  =  if ( A  = -oo ,  if ( B  = +oo ,  0 , -oo ) ,  if ( B  = +oo , +oo ,  if ( B  = -oo , -oo , 
( A  +  B
) ) ) ) )
75, 6syl 17 . . . 4  |-  ( A  e.  RR  ->  if ( A  = +oo ,  if ( B  = -oo ,  0 , +oo ) ,  if ( A  = -oo ,  if ( B  = +oo ,  0 , -oo ) ,  if ( B  = +oo , +oo ,  if ( B  = -oo , -oo ,  ( A  +  B ) ) ) ) )  =  if ( A  = -oo ,  if ( B  = +oo ,  0 , -oo ) ,  if ( B  = +oo , +oo ,  if ( B  = -oo , -oo ,  ( A  +  B ) ) ) ) )
8 renemnf 9715 . . . . 5  |-  ( A  e.  RR  ->  A  =/= -oo )
9 ifnefalse 3905 . . . . 5  |-  ( A  =/= -oo  ->  if ( A  = -oo ,  if ( B  = +oo ,  0 , -oo ) ,  if ( B  = +oo , +oo ,  if ( B  = -oo , -oo , 
( A  +  B
) ) ) )  =  if ( B  = +oo , +oo ,  if ( B  = -oo , -oo , 
( A  +  B
) ) ) )
108, 9syl 17 . . . 4  |-  ( A  e.  RR  ->  if ( A  = -oo ,  if ( B  = +oo ,  0 , -oo ) ,  if ( B  = +oo , +oo ,  if ( B  = -oo , -oo ,  ( A  +  B ) ) ) )  =  if ( B  = +oo , +oo ,  if ( B  = -oo , -oo ,  ( A  +  B ) ) ) )
117, 10eqtrd 2496 . . 3  |-  ( A  e.  RR  ->  if ( A  = +oo ,  if ( B  = -oo ,  0 , +oo ) ,  if ( A  = -oo ,  if ( B  = +oo ,  0 , -oo ) ,  if ( B  = +oo , +oo ,  if ( B  = -oo , -oo ,  ( A  +  B ) ) ) ) )  =  if ( B  = +oo , +oo ,  if ( B  = -oo , -oo ,  ( A  +  B ) ) ) )
12 renepnf 9714 . . . . 5  |-  ( B  e.  RR  ->  B  =/= +oo )
13 ifnefalse 3905 . . . . 5  |-  ( B  =/= +oo  ->  if ( B  = +oo , +oo ,  if ( B  = -oo , -oo ,  ( A  +  B ) ) )  =  if ( B  = -oo , -oo ,  ( A  +  B ) ) )
1412, 13syl 17 . . . 4  |-  ( B  e.  RR  ->  if ( B  = +oo , +oo ,  if ( B  = -oo , -oo ,  ( A  +  B ) ) )  =  if ( B  = -oo , -oo ,  ( A  +  B ) ) )
15 renemnf 9715 . . . . 5  |-  ( B  e.  RR  ->  B  =/= -oo )
16 ifnefalse 3905 . . . . 5  |-  ( B  =/= -oo  ->  if ( B  = -oo , -oo ,  ( A  +  B ) )  =  ( A  +  B
) )
1715, 16syl 17 . . . 4  |-  ( B  e.  RR  ->  if ( B  = -oo , -oo ,  ( A  +  B ) )  =  ( A  +  B ) )
1814, 17eqtrd 2496 . . 3  |-  ( B  e.  RR  ->  if ( B  = +oo , +oo ,  if ( B  = -oo , -oo ,  ( A  +  B ) ) )  =  ( A  +  B ) )
1911, 18sylan9eq 2516 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  if ( A  = +oo ,  if ( B  = -oo , 
0 , +oo ) ,  if ( A  = -oo ,  if ( B  = +oo , 
0 , -oo ) ,  if ( B  = +oo , +oo ,  if ( B  = -oo , -oo ,  ( A  +  B ) ) ) ) )  =  ( A  +  B
) )
204, 19eqtrd 2496 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A +e
B )  =  ( A  +  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1455    e. wcel 1898    =/= wne 2633   ifcif 3893  (class class class)co 6315   RRcr 9564   0cc0 9565    + caddc 9568   +oocpnf 9698   -oocmnf 9699   RR*cxr 9700   +ecxad 11436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-mulcl 9627  ax-i2m1 9633
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-xr 9705  df-xadd 11439
This theorem is referenced by:  rexsub  11555  xaddnemnf  11556  xaddnepnf  11557  xnegid  11558  xaddcom  11560  xaddid1  11561  xnegdi  11563  xaddass  11564  xpncan  11566  xleadd1a  11568  xadddilem  11609  x2times  11614  hashunx  12597  isxmet2d  21391  ismet2  21397  mettri2  21405  prdsxmetlem  21432  bl2in  21464  xblss2ps  21465  xmeter  21497  methaus  21584  metustexhalf  21620  metdcnlem  21903  metnrmlem3  21927  metnrmlem3OLD  21942  iscau3  22297  vdgrfival  25674  vdgrf  25675  vdgrfif  25676  vdgr0  25677  vdgr1d  25680  vdgr1b  25681  vdgr1a  25683  xlt2addrd  28387  xrsmulgzz  28489  xrge0slmod  28656  xrge0iifhom  28792  esumfsupre  28941  esumpfinvallem  28944  omssubadd  29177  omssubaddOLD  29181  probun  29301  heicant  32020  cntotbnd  32173  heiborlem6  32193  supxrgelem  37598  supxrge  37599  infrpge  37612  xrlexaddrp  37613  rexaddd  37622  sge0tsms  38260  sge0pr  38274  sge0resplit  38286  sge0split  38289  sge0iunmptlemfi  38293  sge0iunmptlemre  38295  sge0xaddlem1  38313  sge0xaddlem2  38314  carageniuncllem1  38380  carageniuncllem2  38381  hoidmv1lelem2  38452  hoidmvlelem2  38456  hspmbllem3  38488  xnn0xaddcl  39132  xnn0xadd0  39134  vtxdgfival  39580  vtxduhgrfiun  39589  uspgrloopvd2  39607
  Copyright terms: Public domain W3C validator