Theorem resubcl 9940

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 9631	. . 3 |- ( A e. RR -> A e. CC )
2		recn 9631	. . 3 |- ( B e. RR -> B e. CC )
3		negsub 9924	. . 3 |- ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
4	1, 2, 3	syl2an 480	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A + -u B ) = ( A - B ) )
5		renegcl 9939	. . 3 |- ( B e. RR -> -u B e. RR )
6		readdcl 9624	. . 3 |- ( ( A e. RR /\ -u B e. RR ) -> ( A + -u B ) e. RR )
7	5, 6	sylan2 477	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A + -u B ) e. RR )
8	4, 7	eqeltrrd 2512	1 |- ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1438   e. wcel 1869  (class class class)co 6303   CCcc 9539   RRcr 9540   + caddc 9544   - cmin 9862   -ucneg 9863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-resscn 9598  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-mulcom 9605  ax-addass 9606  ax-mulass 9607  ax-distr 9608  ax-i2m1 9609  ax-1ne0 9610  ax-1rid 9611  ax-rnegex 9612  ax-rrecex 9613  ax-cnre 9614  ax-pre-lttri 9615  ax-pre-lttrn 9616  ax-pre-ltadd 9617

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  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-reu 2783  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-opab 4481  df-mpt 4482  df-id 4766  df-po 4772  df-so 4773  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-riota 6265  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-er 7369  df-en 7576  df-dom 7577  df-sdom 7578  df-pnf 9679  df-mnf 9680  df-ltxr 9682  df-sub 9864  df-neg 9865

This theorem is referenced by:  peano2rem  9943  resubcld  10049  ltaddsub  10090  leaddsub  10092  posdif  10109  lt2sub  10114  le2sub  10115  mulsuble0b  10479  cju  10607  elz2  10956  rpnnen1lem5  11296  difrp  11339  qbtwnre  11494  iooshf  11715  iccshftl  11770  lincmb01cmp  11777  uzsubsubfz  11823  difelfzle  11906  fzonmapblen  11963  eluzgtdifelfzo  11977  fracle1  12040  fldiv  12088  modcl  12101  2submod  12152  modsubdir  12159  expubnd  12334  absdiflt  13374  absdifle  13375  elicc4abs  13376  abssubge0  13384  abs2difabs  13391  rddif  13397  absrdbnd  13398  climsup  13726  flo1  13905  supcvg  13907  refallfaccl  14064  resin4p  14185  recos4p  14186  cos01bnd  14233  cos01gt0  14238  pythagtriplem12  14769  pythagtriplem14  14771  pythagtriplem16  14773  fldivp1  14835  prmreclem6  14858  cshwshashlem2  15060  bl2ioo  21802  ioo2bl  21803  ioo2blex  21804  blssioo  21805  blcvx  21808  reconnlem2  21837  opnreen  21841  iirev  21949  iihalf2  21953  iccpnfhmeo  21965  iccvolcl  22512  ioovolcl  22514  ismbf3d  22602  itgrecl  22747  cmvth  22935  dvle  22951  dvcvx  22964  dvfsumge  22966  aalioulem3  23282  aaliou  23286  aaliou3lem9  23298  abelthlem2  23379  abelthlem7  23385  abelth2  23389  sincosq1sgn  23445  sincosq2sgn  23446  sincosq3sgn  23447  sincosq4sgn  23448  tangtx  23452  sinq12gt0  23454  cosq14gt0  23457  cosq14ge0  23458  cosne0  23471  sinord  23475  resinf1o  23477  tanregt0  23480  efif1olem2  23484  relogdiv  23534  logneg2  23556  logdivlti  23561  logcnlem4  23582  logccv  23600  cxpaddlelem  23683  loglesqrt  23690  ang180lem2  23731  acoscos  23811  acosbnd  23818  acosrecl  23821  atanlogaddlem  23831  atans2  23849  leibpi  23860  divsqrtsumo1  23901  cvxcl  23902  scvxcvx  23903  jensenlem2  23905  amgmlem  23907  harmonicbnd4  23928  zetacvg  23932  ftalem5  23993  ftalem5OLD  23995  basellem9  24007  mumullem2  24099  ppiub  24124  chtub  24132  bposlem1  24204  bposlem6  24209  bposlem9  24212  chtppilim  24305  chto1ub  24306  rplogsumlem2  24315  rpvmasumlem  24317  dchrisum0flblem1  24338  dchrisum0re  24343  log2sumbnd  24374  selberglem2  24376  pntrmax  24394  pntpbnd2  24417  pntlem3  24439  brbtwn2  24927  colinearalglem4  24931  eleesub  24933  eleesubd  24934  axsegconlem2  24940  ax5seglem2  24951  ax5seglem3  24953  axpaschlem  24962  axpasch  24963  axcontlem2  24987  xlt2addrd  28338  signshf  29479  rescon  29971  sinccvglem  30318  fz0n  30365  sin2h  31893  tan2h  31895  poimir  31931  mblfinlem3  31937  mblfinlem4  31938  dvtanlemOLD  31949  itg2addnclem  31951  itg2addnclem3  31953  ftc1anclem5  31979  ftc1anclem6  31980  ftc1anclem7  31981  dvasin  31986  geomcau  32046  bfp  32114  ismrer1  32128  iccbnd  32130  rmspecsqrtnq  35718  jm2.17a  35774  acongeq  35797  jm3.1lem2  35837  areaquad  36065  lptre2pt  37584  dvnmul  37682  stoweidlem59  37784  fourierdlem42  37876  fourierdlem42OLD  37877  bgoldbtbndlem2  38657  ltsubsubaddltsub  38781  zm1nn  38782  nn0resubcl  38785  subsubelfzo0  38795  ply1mulgsumlem2  39523  ltsubaddb  39655  ltsubsubb  39656  ltsubadd2b  39657