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

Theorem rexadd 11538
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 9699 . . 3  |-  ( A  e.  RR  ->  A  e.  RR* )
2 rexr 9699 . . 3  |-  ( B  e.  RR  ->  B  e.  RR* )
3 xaddval 11529 . . 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 480 . 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 9701 . . . . 5  |-  ( A  e.  RR  ->  A  =/= +oo )
6 ifnefalse 3929 . . . . 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 9702 . . . . 5  |-  ( A  e.  RR  ->  A  =/= -oo )
9 ifnefalse 3929 . . . . 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 2464 . . 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 9701 . . . . 5  |-  ( B  e.  RR  ->  B  =/= +oo )
13 ifnefalse 3929 . . . . 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 9702 . . . . 5  |-  ( B  e.  RR  ->  B  =/= -oo )
16 ifnefalse 3929 . . . . 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 2464 . . 3  |-  ( B  e.  RR  ->  if ( B  = +oo , +oo ,  if ( B  = -oo , -oo ,  ( A  +  B ) ) )  =  ( A  +  B ) )
1911, 18sylan9eq 2484 . 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 2464 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A +e
B )  =  ( A  +  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1438    e. wcel 1873    =/= wne 2619   ifcif 3917  (class class class)co 6311   RRcr 9551   0cc0 9552    + caddc 9555   +oocpnf 9685   -oocmnf 9686   RR*cxr 9687   +ecxad 11420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-8 1875  ax-9 1877  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402  ax-sep 4552  ax-nul 4561  ax-pow 4608  ax-pr 4666  ax-un 6603  ax-cnex 9608  ax-resscn 9609  ax-1cn 9610  ax-icn 9611  ax-addcl 9612  ax-mulcl 9614  ax-i2m1 9620
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3087  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3918  df-pw 3989  df-sn 4005  df-pr 4007  df-op 4011  df-uni 4226  df-br 4430  df-opab 4489  df-mpt 4490  df-id 4774  df-xp 4865  df-rel 4866  df-cnv 4867  df-co 4868  df-dm 4869  df-rn 4870  df-res 4871  df-ima 4872  df-iota 5571  df-fun 5609  df-fn 5610  df-f 5611  df-f1 5612  df-fo 5613  df-f1o 5614  df-fv 5615  df-ov 6314  df-oprab 6315  df-mpt2 6316  df-er 7380  df-en 7587  df-dom 7588  df-sdom 7589  df-pnf 9690  df-mnf 9691  df-xr 9692  df-xadd 11423
This theorem is referenced by:  rexsub  11539  xaddnemnf  11540  xaddnepnf  11541  xnegid  11542  xaddcom  11544  xaddid1  11545  xnegdi  11547  xaddass  11548  xpncan  11550  xleadd1a  11552  xadddilem  11593  x2times  11598  hashunx  12577  isxmet2d  21346  ismet2  21352  mettri2  21360  prdsxmetlem  21387  bl2in  21419  xblss2ps  21420  xmeter  21452  methaus  21539  metustexhalf  21575  metdcnlem  21858  metnrmlem3  21882  metnrmlem3OLD  21897  iscau3  22252  vdgrfival  25629  vdgrf  25630  vdgrfif  25631  vdgr0  25632  vdgr1d  25635  vdgr1b  25636  vdgr1a  25638  xlt2addrd  28350  xrsmulgzz  28453  xrge0slmod  28621  xrge0iifhom  28757  esumfsupre  28906  esumpfinvallem  28909  omssubadd  29142  omssubaddOLD  29146  probun  29266  heicant  31945  cntotbnd  32098  heiborlem6  32118  supxrgelem  37520  supxrge  37521  infrpge  37534  xrlexaddrp  37535  sge0tsms  38136  sge0pr  38150  sge0resplit  38162  sge0split  38165  sge0iunmptlemfi  38169  sge0iunmptlemre  38171  sge0xaddlem1  38189  sge0xaddlem2  38190  carageniuncllem1  38256  carageniuncllem2  38257  hoidmv1lelem2  38324  hoidmvlelem2  38328
  Copyright terms: Public domain W3C validator