Theorem resubcl 9879

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

Step	Hyp	Ref	Expression
1		recn 9578	. . 3 |- ( A e. RR -> A e. CC )
2		recn 9578	. . 3 |- ( B e. RR -> B e. CC )
3		negsub 9863	. . 3 |- ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
4	1, 2, 3	syl2an 477	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A + -u B ) = ( A - B ) )
5		renegcl 9878	. . 3 |- ( B e. RR -> -u B e. RR )
6		readdcl 9571	. . 3 |- ( ( A e. RR /\ -u B e. RR ) -> ( A + -u B ) e. RR )
7	5, 6	sylan2 474	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A + -u B ) e. RR )
8	4, 7	eqeltrrd 2556	1 |- ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1379   e. wcel 1767  (class class class)co 6282   CCcc 9486   RRcr 9487   + caddc 9491   - cmin 9801   -ucneg 9802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-po 4800  df-so 4801  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-er 7308  df-en 7514  df-dom 7515  df-sdom 7516  df-pnf 9626  df-mnf 9627  df-ltxr 9629  df-sub 9803  df-neg 9804

This theorem is referenced by:  peano2rem  9882  resubcld  9983  ltaddsub  10022  leaddsub  10024  posdif  10041  lt2sub  10046  le2sub  10047  mulsuble0b  10410  cju  10528  elz2  10877  uzindOLD  10951  rpnnen1lem5  11208  difrp  11249  qbtwnre  11394  iooshf  11599  iccshftl  11652  lincmb01cmp  11659  uzsubsubfz  11703  difelfzle  11781  fzonmapblen  11832  eluzgtdifelfzo  11842  fracle1  11904  fldiv  11951  modcl  11964  2submod  12012  modsubdir  12019  expubnd  12190  absdiflt  13109  absdifle  13110  elicc4abs  13111  abssubge0  13119  abs2difabs  13126  rddif  13132  absrdbnd  13133  climsup  13451  flo1  13625  supcvg  13626  resin4p  13730  recos4p  13731  cos01bnd  13778  cos01gt0  13783  pythagtriplem12  14205  pythagtriplem14  14207  pythagtriplem16  14209  fldivp1  14271  prmreclem6  14294  cshwshashlem2  14435  bl2ioo  21032  ioo2bl  21033  ioo2blex  21034  blssioo  21035  blcvx  21038  reconnlem2  21067  opnreen  21071  iirev  21164  iihalf2  21168  iccpnfhmeo  21180  iccvolcl  21712  ioovolcl  21714  ismbf3d  21796  itgrecl  21939  cmvth  22127  dvle  22143  dvcvx  22156  dvfsumge  22158  aalioulem3  22464  aaliou  22468  aaliou3lem9  22480  abelthlem2  22561  abelthlem7  22567  abelth2  22571  sincosq1sgn  22624  sincosq2sgn  22625  sincosq3sgn  22626  sincosq4sgn  22627  tangtx  22631  sinq12gt0  22633  cosq14gt0  22636  cosq14ge0  22637  cosne0  22650  sinord  22654  resinf1o  22656  tanregt0  22659  efif1olem2  22663  relogdiv  22705  logneg2  22728  logdivlti  22733  logcnlem4  22754  logccv  22772  cxpaddlelem  22853  loglesqrt  22860  ang180lem2  22870  acoscos  22952  acosbnd  22959  acosrecl  22962  atanlogaddlem  22972  atans2  22990  leibpi  23001  divsqrtsumo1  23041  cvxcl  23042  scvxcvx  23043  jensenlem2  23045  amgmlem  23047  harmonicbnd4  23068  ftalem5  23078  basellem9  23090  mumullem2  23182  ppiub  23207  chtub  23215  bposlem1  23287  bposlem6  23292  bposlem9  23295  chtppilim  23388  chto1ub  23389  rplogsumlem2  23398  rpvmasumlem  23400  dchrisum0flblem1  23421  dchrisum0re  23426  log2sumbnd  23457  selberglem2  23459  pntrmax  23477  pntpbnd2  23500  pntlem3  23522  brbtwn2  23884  colinearalglem4  23888  eleesub  23890  eleesubd  23891  axsegconlem2  23897  ax5seglem2  23908  ax5seglem3  23910  axpaschlem  23919  axpasch  23920  axcontlem2  23944  xlt2addrd  27246  signshf  28185  zetacvg  28197  rescon  28331  sinccvglem  28513  fz0n  28585  refallfaccl  28717  sin2h  29622  tan2h  29624  mblfinlem3  29630  mblfinlem4  29631  dvtanlem  29641  itg2addnclem  29643  itg2addnclem3  29645  ftc1anclem5  29671  ftc1anclem6  29672  ftc1anclem7  29673  dvasin  29680  geomcau  29855  bfp  29923  ismrer1  29937  iccbnd  29939  rmspecsqrtnq  30446  jm2.17a  30502  acongeq  30525  jm3.1lem2  30564  areaquad  30789  zltlesub  31045  lptre2pt  31182  ioodvbdlimc2lem  31264  stoweidlem59  31359  fourierdlem26  31433  fourierdlem42  31449  fourierdlem57  31464  fourierdlem79  31486  fourierdlem111  31518  fouriersw  31532  ltsubsubaddltsub  31793  zm1nn  31794  nn0resubcl  31797  subsubelfzo0  31807  ply1mulgsumlem2  32060