Theorem resubcld 11613

Description: Closure law for subtraction of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
renegcld.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
resubcld.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
resubcld	⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ)

Proof of Theorem resubcld

Step	Hyp	Ref	Expression
1		renegcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		resubcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		resubcl 11493	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7390  ℝcr 11074   − cmin 11412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220  df-sub 11414  df-neg 11415

This theorem is referenced by:  ltsubadd  11655  lesubadd  11657  lesub1  11679  lesub2  11680  ltsub1  11681  ltsub2  11682  lt2sub  11683  le2sub  11684  ltmul1a  12038  supaddc  12157  cru  12185  ge2halflem1  13075  qbtwnre  13166  lincmb01cmp  13463  iccf1o  13464  xov1plusxeqvd  13466  intfracq  13828  fldiv  13829  modlt  13849  modsubdir  13912  modsumfzodifsn  13916  serle  14029  expmulnbnd  14207  discr  14212  fzsdom2  14400  cshwidxmod  14775  crre  15087  remullem  15101  01sqrexlem7  15221  absrdbnd  15315  fzomaxdiflem  15316  caubnd2  15331  amgm2  15343  icodiamlt  15411  bhmafibid1  15441  mulcn2  15569  reccn2  15570  rlimo1  15590  climle  15613  climsqz  15614  climsqz2  15615  rlimle  15621  isercolllem1  15638  climsup  15643  caucvgrlem  15646  caucvgrlem2  15648  iseraltlem2  15656  iseraltlem3  15657  iseralt  15658  fsumle  15772  cvgcmp  15789  cvgcmpce  15791  bpoly4  16032  eflt  16092  resinhcl  16131  tanhlt1  16135  sin01bnd  16160  sin01gt0  16165  moddvds  16240  bitscmp  16415  bitsinv1lem  16418  smueqlem  16467  modprm0  16783  pcbc  16878  4sqlem15  16937  blss2ps  24298  blss2  24299  blssps  24319  blss  24320  nm2dif  24520  nlmvscnlem2  24580  nrginvrcnlem  24586  iccntr  24717  icccmplem2  24719  metdstri  24747  cnllycmp  24862  evth  24865  lebnumii  24872  ipcnlem2  25151  cncmet  25229  rrxds  25300  rrxmval  25312  rrxmet  25315  rrxdstprj1  25316  rrxdsfi  25318  ehl1eudis  25327  ehl2eudis  25329  minveclem3b  25335  minveclem4  25339  ivthlem2  25360  ivthlem3  25361  ovollb2lem  25396  ovoliunlem1  25410  ovolscalem1  25421  ovolicc1  25424  ovolicc2lem4  25428  ovolicc2  25430  ovolicc  25431  voliunlem2  25459  ovolioo  25476  ioorcl2  25480  uniioovol  25487  uniioombllem2  25491  uniioombllem3a  25492  uniioombllem3  25493  uniioombllem4  25494  uniioombllem6  25496  opnmbllem  25509  volcn  25514  vitalilem2  25517  ismbf3d  25562  mbfaddlem  25568  i1fadd  25603  itg1addlem4  25607  mbfi1fseqlem6  25628  itg2seq  25650  itg2split  25657  itg2cnlem2  25670  itg2cn  25671  itgrevallem1  25703  dvcjbr  25860  dvferm1lem  25895  dvferm2lem  25897  cmvth  25902  cmvthOLD  25903  mvth  25904  dvlip  25905  dvlip2  25907  c1liplem1  25908  dvgt0  25916  dvlt0  25917  dvge0  25918  dvle  25919  dvivthlem1  25920  lhop1lem  25925  lhop  25928  dvcnvrelem1  25929  dvcnvrelem2  25930  dvcnvre  25931  dvcvx  25932  dvfsumle  25933  dvfsumleOLD  25934  dvfsumge  25935  dvfsumrlimf  25938  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem3  25942  dvfsumlem4  25943  dvfsum2  25948  ftc1a  25951  ftc1lem4  25953  coe1mul3  26011  ply1divex  26049  plydivex  26212  aalioulem2  26248  aalioulem3  26249  aalioulem4  26250  aalioulem5  26251  aalioulem6  26252  aaliou3lem7  26264  taylthlem2  26289  taylthlem2OLD  26290  mtest  26320  pilem2  26369  tangtx  26421  cosordlem  26446  efif1olem2  26459  logcnlem3  26560  logcnlem4  26561  isosctrlem2  26736  chordthmlem2  26750  chordthmlem4  26752  heron  26755  atanlogsublem  26832  atantan  26840  birthdaylem3  26870  logdifbnd  26911  emcllem1  26913  emcllem2  26914  emcllem5  26917  emcllem6  26918  harmonicbnd4  26928  fsumharmonic  26929  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamucov  26955  relgamcl  26979  ftalem2  26991  ftalem5  26994  chpub  27138  logfaclbnd  27140  logfacbnd3  27141  logexprlim  27143  bposlem1  27202  bposlem9  27210  gausslemma2dlem1a  27283  lgseisenlem1  27293  lgsquadlem1  27298  2sqmod  27354  chtppilimlem1  27391  vmadivsum  27400  vmadivsumb  27401  rplogsumlem1  27402  rplogsumlem2  27403  rpvmasumlem  27405  dchrisumlem2  27408  dchrisum0re  27431  rplogsum  27445  mulogsumlem  27449  mulog2sumlem1  27452  vmalogdivsum2  27456  vmalogdivsum  27457  2vmadivsumlem  27458  log2sumbnd  27462  selbergb  27467  selberg2lem  27468  selberg2b  27470  chpdifbndlem1  27471  selberg3lem1  27475  selberg3lem2  27476  selberg3  27477  selberg4lem1  27478  selberg4  27479  pntrf  27481  pntrmax  27482  pntrsumo1  27483  selberg3r  27487  selberg4r  27488  selberg34r  27489  pntrlog2bndlem1  27495  pntrlog2bndlem2  27496  pntrlog2bndlem3  27497  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntrlog2bndlem6  27501  pntrlog2bnd  27502  pntpbnd1a  27503  pntpbnd2  27505  pntibndlem2  27509  pntlemg  27516  pntlemn  27518  pntlemj  27521  pntlemf  27523  pntlemo  27525  pntlem3  27527  pntleml  27529  ttgcontlem1  28819  eqeelen  28838  brbtwn2  28839  colinearalg  28844  axcgrid  28850  axsegconlem1  28851  axsegconlem3  28853  axsegconlem8  28858  axsegconlem9  28859  axsegconlem10  28860  ax5seglem3a  28864  ax5seg  28872  axpaschlem  28874  axcontlem8  28905  nbusgrvtxm1  29313  crctcshwlkn0lem3  29749  crctcshwlkn0lem5  29751  crctcsh  29761  clwlkclwwlklem2fv2  29932  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  nvabs  30608  dipcj  30650  minvecolem4  30816  lt2addrd  32681  xlt2addrd  32689  fzsplit3  32723  bcm1n  32725  sgnsub  32769  ply1degltel  33567  ply1degltlss  33569  iconstr  33763  constrresqrtcl  33774  cos9thpiminplylem1  33779  submateqlem1  33804  cnre2csqlem  33907  tpr2rico  33909  dya2ub  34268  dya2icoseg  34275  ballotlemfcc  34492  ballotlemfrcn0  34528  signslema  34560  ftc2re  34596  subfacval3  35183  dnibndlem8  36480  dnibndlem10  36482  dnibndlem11  36483  dnibndlem12  36484  dnicn  36487  knoppcnlem4  36491  unblimceq0  36502  unbdqndv2lem2  36505  knoppndvlem11  36517  knoppndvlem14  36520  knoppndvlem15  36521  knoppndvlem17  36523  knoppndvlem20  36526  irrdifflemf  37320  poimirlem29  37650  broucube  37655  opnmbllem0  37657  mblfinlem3  37660  mblfinlem4  37661  itg2addnclem  37672  itg2addnclem3  37674  itg2gt0cn  37676  ftc1cnnclem  37692  areacirclem1  37709  areacirclem2  37710  areacirclem4  37712  areacirclem5  37713  areacirc  37714  cntotbnd  37797  rrnmet  37830  rrndstprj1  37831  rrndstprj2  37832  lcmineqlem23  42046  intlewftc  42056  aks4d1p1p2  42065  aks4d1p1p4  42066  dvle2  42067  aks4d1p1  42071  primrootlekpowne0  42100  hashscontpow1  42116  aks6d1c2  42125  aks6d1c5lem2  42133  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  aks6d1c6lem3  42167  bcled  42173  bcle2d  42174  unitscyglem2  42191  unitscyglem4  42193  readdrcl2d  42268  frlmvscadiccat  42501  fltnlta  42658  3cubeslem2  42680  3cubeslem4  42684  irrapxlem2  42818  irrapxlem3  42819  irrapxlem4  42820  irrapxlem5  42821  pellexlem2  42825  pellexlem6  42829  pell1qrgaplem  42868  rmspecsqrtnq  42901  rmspecfund  42904  rmspecpos  42912  jm2.24nn  42955  jm2.17c  42958  fzmaxdif  42977  acongeq  42979  modabsdifz  42982  jm3.1lem2  43014  areaquad  43212  sqrtcvallem2  43633  sqrtcvallem3  43634  sqrtcval  43637  imo72b2lem0  44161  cvgdvgrat  44309  hashnzfzclim  44318  binomcxplemdvbinom  44349  oddfl  45283  lefldiveq  45297  fperiodmul  45309  fzdifsuc2  45315  suprltrp  45331  supxrgere  45336  supxrgelem  45340  suplesup  45342  infleinflem2  45374  infleinf  45375  xrralrecnnge  45393  iccshift  45523  iooshift  45527  iooiinicc  45547  fmul01lt1lem2  45590  climinf  45611  sumnnodd  45635  ltmod  45643  lptre2pt  45645  climleltrp  45681  limsupgtlem  45782  liminflimsupclim  45812  fperdvper  45924  dvbdfbdioolem1  45933  dvbdfbdioolem2  45934  dvbdfbdioo  45935  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnmul  45948  iblspltprt  45978  itgspltprt  45984  itgiccshift  45985  itgperiod  45986  itgsbtaddcnst  45987  sublevolico  45989  stoweidlem1  46006  stoweidlem11  46016  stoweidlem12  46017  stoweidlem13  46018  stoweidlem14  46019  stoweidlem23  46028  stoweidlem24  46029  stoweidlem25  46030  stoweidlem26  46031  stoweidlem34  46039  stoweidlem40  46045  stoweidlem41  46046  stoweidlem42  46047  stoweidlem45  46050  stoweidlem60  46065  stoweidlem62  46067  wallispilem3  46072  wallispilem4  46073  wallispi  46075  wallispi2lem1  46076  stirlinglem5  46083  stirlinglem11  46089  stirlinglem12  46090  dirkercncflem1  46108  fourierdlem4  46116  fourierdlem6  46118  fourierdlem7  46119  fourierdlem9  46121  fourierdlem13  46125  fourierdlem14  46126  fourierdlem15  46127  fourierdlem19  46131  fourierdlem26  46138  fourierdlem35  46147  fourierdlem39  46151  fourierdlem40  46152  fourierdlem41  46153  fourierdlem42  46154  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem51  46162  fourierdlem56  46167  fourierdlem57  46168  fourierdlem59  46170  fourierdlem60  46171  fourierdlem61  46172  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem66  46177  fourierdlem68  46179  fourierdlem71  46182  fourierdlem72  46183  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem78  46189  fourierdlem79  46190  fourierdlem81  46192  fourierdlem82  46193  fourierdlem83  46194  fourierdlem84  46195  fourierdlem88  46199  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem92  46203  fourierdlem93  46204  fourierdlem95  46206  fourierdlem97  46208  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  fourierdlem107  46218  fourierdlem109  46220  fourierdlem111  46222  fouriersw  46236  elaa2lem  46238  etransclem23  46262  rrxtopnfi  46292  rrndistlt  46295  ioorrnopnlem  46309  ioorrnopnxrlem  46311  sge0gtfsumgt  46448  iundjiun  46465  volicorecl  46551  hoiprodcl  46552  hoiprodcl3  46585  volicore  46586  hoidmvcl  46587  hoidmv1lelem2  46597  hoidmv1lelem3  46598  hoidmv1le  46599  hoidmvlelem1  46600  hoidmvlelem2  46601  hoiqssbllem1  46627  hoiqssbllem2  46628  hoiqssbllem3  46629  hspmbllem1  46631  ovolval5lem1  46657  ovolval5lem2  46658  iunhoiioolem  46680  iccvonmbllem  46683  vonicclem1  46688  preimageiingt  46725  salpreimagtge  46730  smfaddlem1  46768  smflimlem4  46779  smfmullem1  46796  smfmullem2  46797  smfmullem3  46798  ltsubsubaddltsub  47306  2elfz2melfz  47323  2tceilhalfelfzo1  47337  requad01  47626  requad1  47627  requad2  47628  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  bgoldbtbndlem4  47813  bgoldbtbnd  47814  gpgedgvtx0  48056  gpgedgvtx1  48057  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx13starlem2  48067  ply1mulgsumlem2  48380  nnpw2pmod  48576  dignn0flhalflem1  48608  affinecomb1  48695  rrxlinesc  48728  rrxlinec  48729  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731  rrx2vlinest  48734  rrx2linest2  48737  2sphere  48742  line2  48745  itsclc0lem2  48750  itsclc0lem3  48751  itscnhlc0yqe  48752  itsclc0yqsollem2  48756  itsclc0yqsol  48757  itscnhlc0xyqsol  48758  itsclinecirc0  48766  itsclinecirc0b  48767  itsclinecirc0in  48768  itsclquadb  48769  2itscp  48774  itscnhlinecirc02plem1  48775  itscnhlinecirc02p  48778  inlinecirc02plem  48779  amgmwlem  49795