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

Theorem resubcl 9325
Description: Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997.)
Assertion
Ref Expression
resubcl  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  -  B
)  e.  RR )

Proof of Theorem resubcl
StepHypRef Expression
1 recn 9040 . . 3  |-  ( A  e.  RR  ->  A  e.  CC )
2 recn 9040 . . 3  |-  ( B  e.  RR  ->  B  e.  CC )
3 negsub 9309 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  -u B )  =  ( A  -  B ) )
41, 2, 3syl2an 464 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  -u B )  =  ( A  -  B ) )
5 renegcl 9324 . . 3  |-  ( B  e.  RR  ->  -u B  e.  RR )
6 readdcl 9033 . . 3  |-  ( ( A  e.  RR  /\  -u B  e.  RR )  ->  ( A  +  -u B )  e.  RR )
75, 6sylan2 461 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  -u B )  e.  RR )
84, 7eqeltrrd 2483 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  -  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721  (class class class)co 6044   CCcc 8948   RRcr 8949    + caddc 8953    - cmin 9251   -ucneg 9252
This theorem is referenced by:  peano2rem  9327  resubcld  9425  ltaddsub  9462  leaddsub  9464  posdif  9481  lt2sub  9486  le2sub  9487  cju  9956  elz2  10258  uzindOLD  10324  rpnnen1lem5  10564  difrp  10605  qbtwnre  10745  iooshf  10949  iccshftl  10992  lincmb01cmp  10998  fracle1  11171  fldiv  11200  modcl  11212  modsubdir  11244  expubnd  11399  absdiflt  12080  absdifle  12081  elicc4abs  12082  abssubge0  12090  abs2difabs  12097  rddif  12103  absrdbnd  12104  climsup  12422  flo1  12593  supcvg  12594  resin4p  12698  recos4p  12699  cos01bnd  12746  cos01gt0  12751  pythagtriplem12  13159  pythagtriplem14  13161  pythagtriplem16  13163  fldivp1  13225  prmreclem6  13248  bl2ioo  18780  ioo2bl  18781  ioo2blex  18782  blssioo  18783  blcvx  18786  reconnlem2  18815  opnreen  18819  iirev  18911  iihalf2  18915  iccpnfhmeo  18927  iccvolcl  19418  ismbf3d  19503  itgrecl  19646  cmvth  19832  dvle  19848  dvcvx  19861  dvfsumge  19863  aalioulem3  20208  aaliou  20212  aaliou3lem9  20224  abelthlem2  20305  abelthlem7  20311  abelth2  20315  sincosq1sgn  20363  sincosq2sgn  20364  sincosq3sgn  20365  sincosq4sgn  20366  tangtx  20370  sinq12gt0  20372  cosq14gt0  20375  cosq14ge0  20376  cosne0  20389  sinord  20393  resinf1o  20395  tanregt0  20398  efif1olem2  20402  relogdiv  20444  logneg2  20467  logdivlti  20472  logcnlem4  20493  logccv  20511  cxpaddlelem  20592  loglesqr  20599  ang180lem2  20609  acoscos  20690  acosbnd  20697  acosrecl  20700  atanlogaddlem  20710  atans2  20728  leibpi  20739  divsqrsumo1  20779  cvxcl  20780  scvxcvx  20781  jensenlem2  20783  amgmlem  20785  harmonicbnd4  20806  ftalem5  20816  basellem9  20828  mumullem2  20920  ppiub  20945  chtub  20953  bposlem1  21025  bposlem6  21030  bposlem9  21033  chtppilim  21126  chto1ub  21127  rplogsumlem2  21136  rpvmasumlem  21138  dchrisum0flblem1  21159  dchrisum0re  21164  log2sumbnd  21195  selberglem2  21197  pntrmax  21215  pntpbnd2  21238  pntlem3  21260  xlt2addrd  24081  zetacvg  24756  rescon  24890  sinccvglem  25066  mulsuble0b  25150  fz0n  25159  refallfaccl  25290  brbtwn2  25752  colinearalglem4  25756  eleesub  25758  eleesubd  25759  axsegconlem2  25765  ax5seglem2  25776  ax5seglem3  25778  axpaschlem  25787  axpasch  25788  axcontlem2  25812  mblfinlem2  26148  mblfinlem3  26149  itg2addnclem  26159  itg2addnclem3  26161  geomcau  26359  bfp  26427  ismrer1  26441  iccbnd  26443  rmspecsqrnq  26863  jm2.17a  26919  acongeq  26942  jm3.1lem2  26983  ioovolcl  27613  stoweidlem59  27679  nn0resubcl  27979  ubmelm1fzo  27991
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664  ax-resscn 9007  ax-1cn 9008  ax-icn 9009  ax-addcl 9010  ax-addrcl 9011  ax-mulcl 9012  ax-mulrcl 9013  ax-mulcom 9014  ax-addass 9015  ax-mulass 9016  ax-distr 9017  ax-i2m1 9018  ax-1ne0 9019  ax-1rid 9020  ax-rnegex 9021  ax-rrecex 9022  ax-cnre 9023  ax-pre-lttri 9024  ax-pre-lttrn 9025  ax-pre-ltadd 9026
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-nel 2574  df-ral 2675  df-rex 2676  df-reu 2677  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-opab 4231  df-mpt 4232  df-id 4462  df-po 4467  df-so 4468  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-ov 6047  df-oprab 6048  df-mpt2 6049  df-riota 6512  df-er 6868  df-en 7073  df-dom 7074  df-sdom 7075  df-pnf 9082  df-mnf 9083  df-ltxr 9085  df-sub 9253  df-neg 9254
  Copyright terms: Public domain W3C validator