Theorem resubcld 11615

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 11495	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 593	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2142  (class class class)co 7396  ℝcr 11072   − cmin 11414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-ltxr 11221  df-sub 11416  df-neg 11417

This theorem is referenced by:  ltsubadd  11657  lesubadd  11659  lesub1  11681  lesub2  11682  ltsub1  11683  ltsub2  11684  lt2sub  11685  le2sub  11686  ltmul1a  12040  supaddc  12159  cru  12187  ge2halflem1  13110  qbtwnre  13202  lincmb01cmp  13499  iccf1o  13500  xov1plusxeqvd  13502  intfracq  13869  fldiv  13870  modlt  13890  modsubdir  13953  modsumfzodifsn  13957  serle  14070  expmulnbnd  14248  discr  14253  fzsdom2  14441  cshwidxmod  14816  sgnsub  15119  crre  15141  remullem  15155  01sqrexlem7  15275  absrdbnd  15369  fzomaxdiflem  15370  caubnd2  15385  amgm2  15397  icodiamlt  15465  bhmafibid1  15495  mulcn2  15623  reccn2  15624  rlimo1  15644  climle  15667  climsqz  15668  climsqz2  15669  rlimle  15675  isercolllem1  15692  climsup  15697  caucvgrlem  15700  caucvgrlem2  15702  iseraltlem2  15710  iseraltlem3  15711  iseralt  15712  fsumle  15827  cvgcmp  15844  cvgcmpce  15846  bpoly4  16089  eflt  16149  resinhcl  16188  tanhlt1  16192  sin01bnd  16217  sin01gt0  16222  moddvds  16297  bitscmp  16472  bitsinv1lem  16475  smueqlem  16524  modprm0  16841  pcbc  16936  4sqlem15  16995  blss2ps  24463  blss2  24464  blssps  24484  blss  24485  nm2dif  24685  nlmvscnlem2  24745  nrginvrcnlem  24751  iccntr  24882  icccmplem2  24884  metdstri  24912  cnllycmp  25018  evth  25021  lebnumii  25028  ipcnlem2  25306  cncmet  25384  rrxds  25455  rrxmval  25467  rrxmet  25470  rrxdstprj1  25471  rrxdsfi  25473  ehl1eudis  25482  ehl2eudis  25484  minveclem3b  25490  minveclem4  25494  ivthlem2  25514  ivthlem3  25515  ovollb2lem  25550  ovoliunlem1  25564  ovolscalem1  25575  ovolicc1  25578  ovolicc2lem4  25582  ovolicc2  25584  ovolicc  25585  voliunlem2  25613  ovolioo  25630  ioorcl2  25634  uniioovol  25641  uniioombllem2  25645  uniioombllem3a  25646  uniioombllem3  25647  uniioombllem4  25648  uniioombllem6  25650  opnmbllem  25663  volcn  25668  vitalilem2  25671  ismbf3d  25716  mbfaddlem  25722  i1fadd  25757  itg1addlem4  25761  mbfi1fseqlem6  25782  itg2seq  25804  itg2split  25811  itg2cnlem2  25824  itg2cn  25825  itgrevallem1  25857  dvcjbr  26011  dvferm1lem  26046  dvferm2lem  26048  cmvth  26053  mvth  26054  dvlip  26055  dvlip2  26057  c1liplem1  26058  dvgt0  26066  dvlt0  26067  dvge0  26068  dvle  26069  dvivthlem1  26070  lhop1lem  26075  lhop  26078  dvcnvrelem1  26079  dvcnvrelem2  26080  dvcnvre  26081  dvcvx  26082  dvfsumle  26083  dvfsumge  26084  dvfsumrlimf  26087  dvfsumlem2  26089  dvfsumlem3  26090  dvfsumlem4  26091  dvfsum2  26096  ftc1a  26099  ftc1lem4  26101  coe1mul3  26159  ply1divex  26197  plydivex  26361  aalioulem2  26397  aalioulem3  26398  aalioulem4  26399  aalioulem5  26400  aalioulem6  26401  aaliou3lem7  26413  taylthlem2  26437  mtest  26467  pilem2  26515  tangtx  26570  cosordlem  26595  efif1olem2  26608  logcnlem3  26709  logcnlem4  26710  isosctrlem2  26884  chordthmlem2  26898  chordthmlem4  26900  heron  26903  atanlogsublem  26980  atantan  26988  birthdaylem3  27018  logdifbnd  27058  emcllem1  27060  emcllem2  27061  emcllem5  27064  emcllem6  27065  harmonicbnd4  27075  fsumharmonic  27076  lgamgulmlem2  27094  lgamgulmlem3  27095  lgamucov  27102  relgamcl  27126  ftalem2  27138  ftalem5  27141  chpub  27284  logfaclbnd  27286  logfacbnd3  27287  logexprlim  27289  bposlem1  27348  bposlem9  27356  gausslemma2dlem1a  27429  lgseisenlem1  27439  lgsquadlem1  27444  2sqmod  27500  chtppilimlem1  27537  vmadivsum  27546  vmadivsumb  27547  rplogsumlem1  27548  rplogsumlem2  27549  rpvmasumlem  27551  dchrisumlem2  27554  dchrisum0re  27577  rplogsum  27591  mulogsumlem  27595  mulog2sumlem1  27598  vmalogdivsum2  27602  vmalogdivsum  27603  2vmadivsumlem  27604  log2sumbnd  27608  selbergb  27613  selberg2lem  27614  selberg2b  27616  chpdifbndlem1  27617  selberg3lem1  27621  selberg3lem2  27622  selberg3  27623  selberg4lem1  27624  selberg4  27625  pntrf  27627  pntrmax  27628  pntrsumo1  27629  selberg3r  27633  selberg4r  27634  selberg34r  27635  pntrlog2bndlem1  27641  pntrlog2bndlem2  27642  pntrlog2bndlem3  27643  pntrlog2bndlem4  27644  pntrlog2bndlem5  27645  pntrlog2bndlem6  27647  pntrlog2bnd  27648  pntpbnd1a  27649  pntpbnd2  27651  pntibndlem2  27655  pntlemg  27662  pntlemn  27664  pntlemj  27667  pntlemf  27669  pntlemo  27671  pntlem3  27673  pntleml  27675  ttgcontlem1  29085  eqeelen  29105  brbtwn2  29106  colinearalg  29111  axcgrid  29117  axsegconlem1  29118  axsegconlem3  29120  axsegconlem8  29125  axsegconlem9  29126  axsegconlem10  29127  ax5seglem3a  29131  ax5seg  29139  axpaschlem  29141  axcontlem8  29172  nbusgrvtxm1  29580  crctcshwlkn0lem3  30012  crctcshwlkn0lem5  30014  crctcsh  30024  clwlkclwwlklem2fv2  30198  clwlkclwwlklem2a4  30199  clwlkclwwlklem2a  30200  nvabs  30875  dipcj  30917  minvecolem4  31083  lt2addrd  32952  xlt2addrd  32961  fzsplit3  32995  bcm1n  32997  ply1degltel  33790  ply1degltlss  33792  iconstr  34063  constrresqrtcl  34074  cos9thpiminplylem1  34079  submateqlem1  34104  cnre2csqlem  34207  tpr2rico  34209  dya2ub  34567  dya2icoseg  34574  ballotlemfcc  34791  ballotlemfrcn0  34827  signslema  34856  ftc2re  34892  subfacval3  35539  dnibndlem8  36923  dnibndlem10  36925  dnibndlem11  36926  dnibndlem12  36927  dnicn  36930  knoppcnlem4  36934  unblimceq0  36945  unbdqndv2lem2  36948  knoppndvlem11  36960  knoppndvlem14  36963  knoppndvlem15  36964  knoppndvlem17  36966  knoppndvlem20  36969  irrdifflemf  37817  qdiff  37819  poimirlem29  38148  broucube  38153  opnmbllem0  38155  mblfinlem3  38158  mblfinlem4  38159  itg2addnclem  38170  itg2addnclem3  38172  itg2gt0cn  38174  ftc1cnnclem  38190  areacirclem1  38207  areacirclem2  38208  areacirclem4  38210  areacirclem5  38211  areacirc  38212  cntotbnd  38295  rrnmet  38328  rrndstprj1  38329  rrndstprj2  38330  lcmineqlem23  42668  intlewftc  42678  aks4d1p1p2  42687  aks4d1p1p4  42688  dvle2  42689  aks4d1p1  42693  primrootlekpowne0  42722  hashscontpow1  42738  aks6d1c2  42747  aks6d1c5lem2  42755  sticksstones10  42772  sticksstones12a  42774  sticksstones12  42775  aks6d1c6lem3  42789  bcled  42795  bcle2d  42796  unitscyglem2  42813  unitscyglem4  42815  readdrcl2d  42882  frlmvscadiccat  43128  fltnlta  43245  3cubeslem2  43266  3cubeslem4  43270  irrapxlem2  43400  irrapxlem3  43401  irrapxlem4  43402  irrapxlem5  43403  pellexlem2  43407  pellexlem6  43411  pell1qrgaplem  43450  rmspecsqrtnq  43483  rmspecfund  43486  rmspecpos  43493  jm2.24nn  43536  jm2.17c  43539  fzmaxdif  43558  acongeq  43560  modabsdifz  43563  jm3.1lem2  43595  areaquad  43793  sqrtcvallem2  44213  sqrtcvallem3  44214  sqrtcval  44217  imo72b2lem0  44741  cvgdvgrat  44889  hashnzfzclim  44898  binomcxplemdvbinom  44929  oddfl  45857  lefldiveq  45871  fperiodmul  45883  fzdifsuc2  45889  suprltrp  45904  supxrgere  45909  supxrgelem  45913  suplesup  45915  infleinflem2  45946  infleinf  45947  xrralrecnnge  45965  iccshift  46094  iooshift  46098  iooiinicc  46118  fmul01lt1lem2  46161  climinf  46182  sumnnodd  46206  ltmod  46212  lptre2pt  46214  climleltrp  46250  limsupgtlem  46351  liminflimsupclim  46381  fperdvper  46493  dvbdfbdioolem1  46502  dvbdfbdioolem2  46503  dvbdfbdioo  46504  ioodvbdlimc1lem1  46505  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  dvnmul  46517  iblspltprt  46547  itgspltprt  46553  itgiccshift  46554  itgperiod  46555  itgsbtaddcnst  46556  sublevolico  46558  stoweidlem1  46575  stoweidlem11  46585  stoweidlem12  46586  stoweidlem13  46587  stoweidlem14  46588  stoweidlem23  46597  stoweidlem24  46598  stoweidlem25  46599  stoweidlem26  46600  stoweidlem34  46608  stoweidlem40  46614  stoweidlem41  46615  stoweidlem42  46616  stoweidlem45  46619  stoweidlem60  46634  stoweidlem62  46636  wallispilem3  46641  wallispilem4  46642  wallispi  46644  wallispi2lem1  46645  stirlinglem5  46652  stirlinglem11  46658  stirlinglem12  46659  dirkercncflem1  46677  fourierdlem4  46685  fourierdlem6  46687  fourierdlem7  46688  fourierdlem9  46690  fourierdlem13  46694  fourierdlem14  46695  fourierdlem15  46696  fourierdlem19  46700  fourierdlem26  46707  fourierdlem35  46716  fourierdlem39  46720  fourierdlem40  46721  fourierdlem41  46722  fourierdlem42  46723  fourierdlem48  46728  fourierdlem49  46729  fourierdlem50  46730  fourierdlem51  46731  fourierdlem56  46736  fourierdlem57  46737  fourierdlem59  46739  fourierdlem60  46740  fourierdlem61  46741  fourierdlem63  46743  fourierdlem64  46744  fourierdlem65  46745  fourierdlem66  46746  fourierdlem68  46748  fourierdlem71  46751  fourierdlem72  46752  fourierdlem73  46753  fourierdlem74  46754  fourierdlem75  46755  fourierdlem76  46756  fourierdlem78  46758  fourierdlem79  46759  fourierdlem81  46761  fourierdlem82  46762  fourierdlem83  46763  fourierdlem84  46764  fourierdlem88  46768  fourierdlem89  46769  fourierdlem90  46770  fourierdlem91  46771  fourierdlem92  46772  fourierdlem93  46773  fourierdlem95  46775  fourierdlem97  46777  fourierdlem101  46781  fourierdlem103  46783  fourierdlem104  46784  fourierdlem107  46787  fourierdlem109  46789  fourierdlem111  46791  fouriersw  46805  elaa2lem  46807  etransclem23  46831  rrxtopnfi  46861  rrndistlt  46864  ioorrnopnlem  46878  ioorrnopnxrlem  46880  sge0gtfsumgt  47017  iundjiun  47034  volicorecl  47120  hoiprodcl  47121  hoiprodcl3  47154  volicore  47155  hoidmvcl  47156  hoidmv1lelem2  47166  hoidmv1lelem3  47167  hoidmv1le  47168  hoidmvlelem1  47169  hoidmvlelem2  47170  hoiqssbllem1  47196  hoiqssbllem2  47197  hoiqssbllem3  47198  hspmbllem1  47200  ovolval5lem1  47226  ovolval5lem2  47227  iunhoiioolem  47249  iccvonmbllem  47252  vonicclem1  47257  preimageiingt  47294  salpreimagtge  47299  smfaddlem1  47337  smflimlem4  47348  smfmullem1  47365  smfmullem2  47366  smfmullem3  47367  ltsubsubaddltsub  47895  2elfz2melfz  47912  2tceilhalfelfzo1  47930  flmrecm1  47937  requad01  48243  requad1  48244  requad2  48245  bgoldbtbndlem2  48428  bgoldbtbndlem3  48429  bgoldbtbndlem4  48430  bgoldbtbnd  48431  gpgedgvtx0  48683  gpgedgvtx1  48684  gpg5nbgrvtx03starlem2  48691  gpg5nbgrvtx13starlem2  48694  ply1mulgsumlem2  49009  nnpw2pmod  49205  dignn0flhalflem1  49237  affinecomb1  49324  rrxlinesc  49357  rrxlinec  49358  eenglngeehlnmlem1  49359  eenglngeehlnmlem2  49360  rrx2vlinest  49363  rrx2linest2  49366  2sphere  49371  line2  49374  itsclc0lem2  49379  itsclc0lem3  49380  itscnhlc0yqe  49381  itsclc0yqsollem2  49385  itsclc0yqsol  49386  itscnhlc0xyqsol  49387  itsclinecirc0  49395  itsclinecirc0b  49396  itsclinecirc0in  49397  itsclquadb  49398  2itscp  49403  itscnhlinecirc02plem1  49404  itscnhlinecirc02p  49407  inlinecirc02plem  49408  amgmwlem  50423