Theorem resubcl 9963

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 9654	. . 3 |- ( A e. RR -> A e. CC )
2		recn 9654	. . 3 |- ( B e. RR -> B e. CC )
3		negsub 9947	. . 3 |- ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
4	1, 2, 3	syl2an 484	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A + -u B ) = ( A - B ) )
5		renegcl 9962	. . 3 |- ( B e. RR -> -u B e. RR )
6		readdcl 9647	. . 3 |- ( ( A e. RR /\ -u B e. RR ) -> ( A + -u B ) e. RR )
7	5, 6	sylan2 481	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A + -u B ) e. RR )
8	4, 7	eqeltrrd 2540	1 |- ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )

Syntax hints:   -> wi 4   /\ wa 375   = wceq 1454   e. wcel 1897  (class class class)co 6314   CCcc 9562   RRcr 9563   + caddc 9567   - cmin 9885   -ucneg 9886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-opab 4475  df-mpt 4476  df-id 4767  df-po 4773  df-so 4774  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-er 7388  df-en 7595  df-dom 7596  df-sdom 7597  df-pnf 9702  df-mnf 9703  df-ltxr 9705  df-sub 9887  df-neg 9888

This theorem is referenced by:  peano2rem  9966  resubcld  10074  ltaddsub  10115  leaddsub  10117  posdif  10134  lt2sub  10139  le2sub  10140  mulsuble0b  10504  cju  10632  elz2  10982  rpnnen1lem5  11322  difrp  11365  qbtwnre  11520  iooshf  11741  iccshftl  11796  lincmb01cmp  11803  uzsubsubfz  11849  difelfzle  11933  fzonmapblen  11991  eluzgtdifelfzo  12006  fracle1  12070  fldiv  12118  modcl  12131  2submod  12182  modsubdir  12189  expubnd  12364  absdiflt  13428  absdifle  13429  elicc4abs  13430  abssubge0  13438  abs2difabs  13445  rddif  13451  absrdbnd  13452  climsup  13781  flo1  13960  supcvg  13962  refallfaccl  14119  resin4p  14240  recos4p  14241  cos01bnd  14288  cos01gt0  14293  pythagtriplem12  14824  pythagtriplem14  14826  pythagtriplem16  14828  fldivp1  14890  prmreclem6  14913  cshwshashlem2  15115  bl2ioo  21858  ioo2bl  21859  ioo2blex  21860  blssioo  21861  blcvx  21864  reconnlem2  21893  opnreen  21897  iirev  22005  iihalf2  22009  iccpnfhmeo  22021  iccvolcl  22568  ioovolcl  22570  ismbf3d  22658  itgrecl  22803  cmvth  22991  dvle  23007  dvcvx  23020  dvfsumge  23022  aalioulem3  23338  aaliou  23342  aaliou3lem9  23354  abelthlem2  23435  abelthlem7  23441  abelth2  23445  sincosq1sgn  23501  sincosq2sgn  23502  sincosq3sgn  23503  sincosq4sgn  23504  tangtx  23508  sinq12gt0  23510  cosq14gt0  23513  cosq14ge0  23514  cosne0  23527  sinord  23531  resinf1o  23533  tanregt0  23536  efif1olem2  23540  relogdiv  23590  logneg2  23612  logdivlti  23617  logcnlem4  23638  logccv  23656  cxpaddlelem  23739  loglesqrt  23746  ang180lem2  23787  acoscos  23867  acosbnd  23874  acosrecl  23877  atanlogaddlem  23887  atans2  23905  leibpi  23916  divsqrtsumo1  23957  cvxcl  23958  scvxcvx  23959  jensenlem2  23961  amgmlem  23963  harmonicbnd4  23984  zetacvg  23988  ftalem5  24049  ftalem5OLD  24051  basellem9  24063  mumullem2  24155  ppiub  24180  chtub  24188  bposlem1  24260  bposlem6  24265  bposlem9  24268  chtppilim  24361  chto1ub  24362  rplogsumlem2  24371  rpvmasumlem  24373  dchrisum0flblem1  24394  dchrisum0re  24399  log2sumbnd  24430  selberglem2  24432  pntrmax  24450  pntpbnd2  24473  pntlem3  24495  brbtwn2  24983  colinearalglem4  24987  eleesub  24989  eleesubd  24990  axsegconlem2  24996  ax5seglem2  25007  ax5seglem3  25009  axpaschlem  25018  axpasch  25019  axcontlem2  25043  xlt2addrd  28386  signshf  29525  rescon  30017  sinccvglem  30364  fz0n  30412  sin2h  31979  tan2h  31981  poimir  32017  mblfinlem3  32023  mblfinlem4  32024  dvtanlemOLD  32035  itg2addnclem  32037  itg2addnclem3  32039  ftc1anclem5  32065  ftc1anclem6  32066  ftc1anclem7  32067  dvasin  32072  geomcau  32132  bfp  32200  ismrer1  32214  iccbnd  32216  rmspecsqrtnq  35798  jm2.17a  35854  acongeq  35877  jm3.1lem2  35917  areaquad  36145  lptre2pt  37757  dvnmul  37855  stoweidlem59  37957  fourierdlem42  38049  fourierdlem42OLD  38050  hoidmvlelem2  38455  bgoldbtbndlem2  38938  ltsubsubaddltsub  39089  zm1nn  39090  nn0resubcl  39093  subsubelfzo0  39103  ply1mulgsumlem2  40451  ltsubaddb  40583  ltsubsubb  40584  ltsubadd2b  40585