Theorem resubcld 11548

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7349  ℝcr 11008   − cmin 11347

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 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-ltxr 11154  df-sub 11349  df-neg 11350

This theorem is referenced by:  ltsubadd  11590  lesubadd  11592  lesub1  11614  lesub2  11615  ltsub1  11616  ltsub2  11617  lt2sub  11618  le2sub  11619  ltmul1a  11973  supaddc  12092  cru  12120  ge2halflem1  13010  qbtwnre  13101  lincmb01cmp  13398  iccf1o  13399  xov1plusxeqvd  13401  intfracq  13763  fldiv  13764  modlt  13784  modsubdir  13847  modsumfzodifsn  13851  serle  13964  expmulnbnd  14142  discr  14147  fzsdom2  14335  cshwidxmod  14709  crre  15021  remullem  15035  01sqrexlem7  15155  absrdbnd  15249  fzomaxdiflem  15250  caubnd2  15265  amgm2  15277  icodiamlt  15345  bhmafibid1  15375  mulcn2  15503  reccn2  15504  rlimo1  15524  climle  15547  climsqz  15548  climsqz2  15549  rlimle  15555  isercolllem1  15572  climsup  15577  caucvgrlem  15580  caucvgrlem2  15582  iseraltlem2  15590  iseraltlem3  15591  iseralt  15592  fsumle  15706  cvgcmp  15723  cvgcmpce  15725  bpoly4  15966  eflt  16026  resinhcl  16065  tanhlt1  16069  sin01bnd  16094  sin01gt0  16099  moddvds  16174  bitscmp  16349  bitsinv1lem  16352  smueqlem  16401  modprm0  16717  pcbc  16812  4sqlem15  16871  blss2ps  24289  blss2  24290  blssps  24310  blss  24311  nm2dif  24511  nlmvscnlem2  24571  nrginvrcnlem  24577  iccntr  24708  icccmplem2  24710  metdstri  24738  cnllycmp  24853  evth  24856  lebnumii  24863  ipcnlem2  25142  cncmet  25220  rrxds  25291  rrxmval  25303  rrxmet  25306  rrxdstprj1  25307  rrxdsfi  25309  ehl1eudis  25318  ehl2eudis  25320  minveclem3b  25326  minveclem4  25330  ivthlem2  25351  ivthlem3  25352  ovollb2lem  25387  ovoliunlem1  25401  ovolscalem1  25412  ovolicc1  25415  ovolicc2lem4  25419  ovolicc2  25421  ovolicc  25422  voliunlem2  25450  ovolioo  25467  ioorcl2  25471  uniioovol  25478  uniioombllem2  25482  uniioombllem3a  25483  uniioombllem3  25484  uniioombllem4  25485  uniioombllem6  25487  opnmbllem  25500  volcn  25505  vitalilem2  25508  ismbf3d  25553  mbfaddlem  25559  i1fadd  25594  itg1addlem4  25598  mbfi1fseqlem6  25619  itg2seq  25641  itg2split  25648  itg2cnlem2  25661  itg2cn  25662  itgrevallem1  25694  dvcjbr  25851  dvferm1lem  25886  dvferm2lem  25888  cmvth  25893  cmvthOLD  25894  mvth  25895  dvlip  25896  dvlip2  25898  c1liplem1  25899  dvgt0  25907  dvlt0  25908  dvge0  25909  dvle  25910  dvivthlem1  25911  lhop1lem  25916  lhop  25919  dvcnvrelem1  25920  dvcnvrelem2  25921  dvcnvre  25922  dvcvx  25923  dvfsumle  25924  dvfsumleOLD  25925  dvfsumge  25926  dvfsumrlimf  25929  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsumlem3  25933  dvfsumlem4  25934  dvfsum2  25939  ftc1a  25942  ftc1lem4  25944  coe1mul3  26002  ply1divex  26040  plydivex  26203  aalioulem2  26239  aalioulem3  26240  aalioulem4  26241  aalioulem5  26242  aalioulem6  26243  aaliou3lem7  26255  taylthlem2  26280  taylthlem2OLD  26281  mtest  26311  pilem2  26360  tangtx  26412  cosordlem  26437  efif1olem2  26450  logcnlem3  26551  logcnlem4  26552  isosctrlem2  26727  chordthmlem2  26741  chordthmlem4  26743  heron  26746  atanlogsublem  26823  atantan  26831  birthdaylem3  26861  logdifbnd  26902  emcllem1  26904  emcllem2  26905  emcllem5  26908  emcllem6  26909  harmonicbnd4  26919  fsumharmonic  26920  lgamgulmlem2  26938  lgamgulmlem3  26939  lgamucov  26946  relgamcl  26970  ftalem2  26982  ftalem5  26985  chpub  27129  logfaclbnd  27131  logfacbnd3  27132  logexprlim  27134  bposlem1  27193  bposlem9  27201  gausslemma2dlem1a  27274  lgseisenlem1  27284  lgsquadlem1  27289  2sqmod  27345  chtppilimlem1  27382  vmadivsum  27391  vmadivsumb  27392  rplogsumlem1  27393  rplogsumlem2  27394  rpvmasumlem  27396  dchrisumlem2  27399  dchrisum0re  27422  rplogsum  27436  mulogsumlem  27440  mulog2sumlem1  27443  vmalogdivsum2  27447  vmalogdivsum  27448  2vmadivsumlem  27449  log2sumbnd  27453  selbergb  27458  selberg2lem  27459  selberg2b  27461  chpdifbndlem1  27462  selberg3lem1  27466  selberg3lem2  27467  selberg3  27468  selberg4lem1  27469  selberg4  27470  pntrf  27472  pntrmax  27473  pntrsumo1  27474  selberg3r  27478  selberg4r  27479  selberg34r  27480  pntrlog2bndlem1  27486  pntrlog2bndlem2  27487  pntrlog2bndlem3  27488  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  pntrlog2bndlem6  27492  pntrlog2bnd  27493  pntpbnd1a  27494  pntpbnd2  27496  pntibndlem2  27500  pntlemg  27507  pntlemn  27509  pntlemj  27512  pntlemf  27514  pntlemo  27516  pntlem3  27518  pntleml  27520  ttgcontlem1  28830  eqeelen  28849  brbtwn2  28850  colinearalg  28855  axcgrid  28861  axsegconlem1  28862  axsegconlem3  28864  axsegconlem8  28869  axsegconlem9  28870  axsegconlem10  28871  ax5seglem3a  28875  ax5seg  28883  axpaschlem  28885  axcontlem8  28916  nbusgrvtxm1  29324  crctcshwlkn0lem3  29757  crctcshwlkn0lem5  29759  crctcsh  29769  clwlkclwwlklem2fv2  29940  clwlkclwwlklem2a4  29941  clwlkclwwlklem2a  29942  nvabs  30616  dipcj  30658  minvecolem4  30824  lt2addrd  32694  xlt2addrd  32702  fzsplit3  32736  bcm1n  32738  sgnsub  32782  ply1degltel  33527  ply1degltlss  33529  iconstr  33733  constrresqrtcl  33744  cos9thpiminplylem1  33749  submateqlem1  33774  cnre2csqlem  33877  tpr2rico  33879  dya2ub  34238  dya2icoseg  34245  ballotlemfcc  34462  ballotlemfrcn0  34498  signslema  34530  ftc2re  34566  subfacval3  35166  dnibndlem8  36463  dnibndlem10  36465  dnibndlem11  36466  dnibndlem12  36467  dnicn  36470  knoppcnlem4  36474  unblimceq0  36485  unbdqndv2lem2  36488  knoppndvlem11  36500  knoppndvlem14  36503  knoppndvlem15  36504  knoppndvlem17  36506  knoppndvlem20  36509  irrdifflemf  37303  poimirlem29  37633  broucube  37638  opnmbllem0  37640  mblfinlem3  37643  mblfinlem4  37644  itg2addnclem  37655  itg2addnclem3  37657  itg2gt0cn  37659  ftc1cnnclem  37675  areacirclem1  37692  areacirclem2  37693  areacirclem4  37695  areacirclem5  37696  areacirc  37697  cntotbnd  37780  rrnmet  37813  rrndstprj1  37814  rrndstprj2  37815  lcmineqlem23  42028  intlewftc  42038  aks4d1p1p2  42047  aks4d1p1p4  42048  dvle2  42049  aks4d1p1  42053  primrootlekpowne0  42082  hashscontpow1  42098  aks6d1c2  42107  aks6d1c5lem2  42115  sticksstones10  42132  sticksstones12a  42134  sticksstones12  42135  aks6d1c6lem3  42149  bcled  42155  bcle2d  42156  unitscyglem2  42173  unitscyglem4  42175  readdrcl2d  42250  frlmvscadiccat  42483  fltnlta  42640  3cubeslem2  42662  3cubeslem4  42666  irrapxlem2  42800  irrapxlem3  42801  irrapxlem4  42802  irrapxlem5  42803  pellexlem2  42807  pellexlem6  42811  pell1qrgaplem  42850  rmspecsqrtnq  42883  rmspecfund  42886  rmspecpos  42893  jm2.24nn  42936  jm2.17c  42939  fzmaxdif  42958  acongeq  42960  modabsdifz  42963  jm3.1lem2  42995  areaquad  43193  sqrtcvallem2  43614  sqrtcvallem3  43615  sqrtcval  43618  imo72b2lem0  44142  cvgdvgrat  44290  hashnzfzclim  44299  binomcxplemdvbinom  44330  oddfl  45264  lefldiveq  45278  fperiodmul  45290  fzdifsuc2  45296  suprltrp  45312  supxrgere  45317  supxrgelem  45321  suplesup  45323  infleinflem2  45354  infleinf  45355  xrralrecnnge  45373  iccshift  45503  iooshift  45507  iooiinicc  45527  fmul01lt1lem2  45570  climinf  45591  sumnnodd  45615  ltmod  45623  lptre2pt  45625  climleltrp  45661  limsupgtlem  45762  liminflimsupclim  45792  fperdvper  45904  dvbdfbdioolem1  45913  dvbdfbdioolem2  45914  dvbdfbdioo  45915  ioodvbdlimc1lem1  45916  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  dvnmul  45928  iblspltprt  45958  itgspltprt  45964  itgiccshift  45965  itgperiod  45966  itgsbtaddcnst  45967  sublevolico  45969  stoweidlem1  45986  stoweidlem11  45996  stoweidlem12  45997  stoweidlem13  45998  stoweidlem14  45999  stoweidlem23  46008  stoweidlem24  46009  stoweidlem25  46010  stoweidlem26  46011  stoweidlem34  46019  stoweidlem40  46025  stoweidlem41  46026  stoweidlem42  46027  stoweidlem45  46030  stoweidlem60  46045  stoweidlem62  46047  wallispilem3  46052  wallispilem4  46053  wallispi  46055  wallispi2lem1  46056  stirlinglem5  46063  stirlinglem11  46069  stirlinglem12  46070  dirkercncflem1  46088  fourierdlem4  46096  fourierdlem6  46098  fourierdlem7  46099  fourierdlem9  46101  fourierdlem13  46105  fourierdlem14  46106  fourierdlem15  46107  fourierdlem19  46111  fourierdlem26  46118  fourierdlem35  46127  fourierdlem39  46131  fourierdlem40  46132  fourierdlem41  46133  fourierdlem42  46134  fourierdlem48  46139  fourierdlem49  46140  fourierdlem50  46141  fourierdlem51  46142  fourierdlem56  46147  fourierdlem57  46148  fourierdlem59  46150  fourierdlem60  46151  fourierdlem61  46152  fourierdlem63  46154  fourierdlem64  46155  fourierdlem65  46156  fourierdlem66  46157  fourierdlem68  46159  fourierdlem71  46162  fourierdlem72  46163  fourierdlem73  46164  fourierdlem74  46165  fourierdlem75  46166  fourierdlem76  46167  fourierdlem78  46169  fourierdlem79  46170  fourierdlem81  46172  fourierdlem82  46173  fourierdlem83  46174  fourierdlem84  46175  fourierdlem88  46179  fourierdlem89  46180  fourierdlem90  46181  fourierdlem91  46182  fourierdlem92  46183  fourierdlem93  46184  fourierdlem95  46186  fourierdlem97  46188  fourierdlem101  46192  fourierdlem103  46194  fourierdlem104  46195  fourierdlem107  46198  fourierdlem109  46200  fourierdlem111  46202  fouriersw  46216  elaa2lem  46218  etransclem23  46242  rrxtopnfi  46272  rrndistlt  46275  ioorrnopnlem  46289  ioorrnopnxrlem  46291  sge0gtfsumgt  46428  iundjiun  46445  volicorecl  46531  hoiprodcl  46532  hoiprodcl3  46565  volicore  46566  hoidmvcl  46567  hoidmv1lelem2  46577  hoidmv1lelem3  46578  hoidmv1le  46579  hoidmvlelem1  46580  hoidmvlelem2  46581  hoiqssbllem1  46607  hoiqssbllem2  46608  hoiqssbllem3  46609  hspmbllem1  46611  ovolval5lem1  46637  ovolval5lem2  46638  iunhoiioolem  46660  iccvonmbllem  46663  vonicclem1  46668  preimageiingt  46705  salpreimagtge  46710  smfaddlem1  46748  smflimlem4  46759  smfmullem1  46776  smfmullem2  46777  smfmullem3  46778  ltsubsubaddltsub  47289  2elfz2melfz  47306  2tceilhalfelfzo1  47320  requad01  47609  requad1  47610  requad2  47611  bgoldbtbndlem2  47794  bgoldbtbndlem3  47795  bgoldbtbndlem4  47796  bgoldbtbnd  47797  gpgedgvtx0  48049  gpgedgvtx1  48050  gpg5nbgrvtx03starlem2  48057  gpg5nbgrvtx13starlem2  48060  ply1mulgsumlem2  48376  nnpw2pmod  48572  dignn0flhalflem1  48604  affinecomb1  48691  rrxlinesc  48724  rrxlinec  48725  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  rrx2vlinest  48730  rrx2linest2  48733  2sphere  48738  line2  48741  itsclc0lem2  48746  itsclc0lem3  48747  itscnhlc0yqe  48748  itsclc0yqsollem2  48752  itsclc0yqsol  48753  itscnhlc0xyqsol  48754  itsclinecirc0  48762  itsclinecirc0b  48763  itsclinecirc0in  48764  itsclquadb  48765  2itscp  48770  itscnhlinecirc02plem1  48771  itscnhlinecirc02p  48774  inlinecirc02plem  48775  amgmwlem  49791