Theorem resubcld 11691

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7431  ℝcr 11154   − cmin 11492

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-ltxr 11300  df-sub 11494  df-neg 11495

This theorem is referenced by:  ltsubadd  11733  lesubadd  11735  lesub1  11757  lesub2  11758  ltsub1  11759  ltsub2  11760  lt2sub  11761  le2sub  11762  ltmul1a  12116  supaddc  12235  cru  12258  ge2halflem1  13150  qbtwnre  13241  lincmb01cmp  13535  iccf1o  13536  xov1plusxeqvd  13538  intfracq  13899  fldiv  13900  modlt  13920  modsubdir  13981  modsumfzodifsn  13985  serle  14098  expmulnbnd  14274  discr  14279  fzsdom2  14467  cshwidxmod  14841  crre  15153  remullem  15167  01sqrexlem7  15287  absrdbnd  15380  fzomaxdiflem  15381  caubnd2  15396  amgm2  15408  icodiamlt  15474  bhmafibid1  15504  mulcn2  15632  reccn2  15633  rlimo1  15653  climle  15676  climsqz  15677  climsqz2  15678  rlimle  15684  isercolllem1  15701  climsup  15706  caucvgrlem  15709  caucvgrlem2  15711  iseraltlem2  15719  iseraltlem3  15720  iseralt  15721  fsumle  15835  cvgcmp  15852  cvgcmpce  15854  bpoly4  16095  eflt  16153  resinhcl  16192  tanhlt1  16196  sin01bnd  16221  sin01gt0  16226  moddvds  16301  bitscmp  16475  bitsinv1lem  16478  smueqlem  16527  modprm0  16843  pcbc  16938  4sqlem15  16997  blss2ps  24413  blss2  24414  blssps  24434  blss  24435  nm2dif  24638  nlmvscnlem2  24706  nrginvrcnlem  24712  iccntr  24843  icccmplem2  24845  metdstri  24873  cnllycmp  24988  evth  24991  lebnumii  24998  ipcnlem2  25278  cncmet  25356  rrxds  25427  rrxmval  25439  rrxmet  25442  rrxdstprj1  25443  rrxdsfi  25445  ehl1eudis  25454  ehl2eudis  25456  minveclem3b  25462  minveclem4  25466  ivthlem2  25487  ivthlem3  25488  ovollb2lem  25523  ovoliunlem1  25537  ovolscalem1  25548  ovolicc1  25551  ovolicc2lem4  25555  ovolicc2  25557  ovolicc  25558  voliunlem2  25586  ovolioo  25603  ioorcl2  25607  uniioovol  25614  uniioombllem2  25618  uniioombllem3a  25619  uniioombllem3  25620  uniioombllem4  25621  uniioombllem6  25623  opnmbllem  25636  volcn  25641  vitalilem2  25644  ismbf3d  25689  mbfaddlem  25695  i1fadd  25730  itg1addlem4  25734  mbfi1fseqlem6  25755  itg2seq  25777  itg2split  25784  itg2cnlem2  25797  itg2cn  25798  itgrevallem1  25830  dvcjbr  25987  dvferm1lem  26022  dvferm2lem  26024  cmvth  26029  cmvthOLD  26030  mvth  26031  dvlip  26032  dvlip2  26034  c1liplem1  26035  dvgt0  26043  dvlt0  26044  dvge0  26045  dvle  26046  dvivthlem1  26047  lhop1lem  26052  lhop  26055  dvcnvrelem1  26056  dvcnvrelem2  26057  dvcnvre  26058  dvcvx  26059  dvfsumle  26060  dvfsumleOLD  26061  dvfsumge  26062  dvfsumrlimf  26065  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem3  26069  dvfsumlem4  26070  dvfsum2  26075  ftc1a  26078  ftc1lem4  26080  coe1mul3  26138  ply1divex  26176  plydivex  26339  aalioulem2  26375  aalioulem3  26376  aalioulem4  26377  aalioulem5  26378  aalioulem6  26379  aaliou3lem7  26391  taylthlem2  26416  taylthlem2OLD  26417  mtest  26447  pilem2  26496  tangtx  26547  cosordlem  26572  efif1olem2  26585  logcnlem3  26686  logcnlem4  26687  isosctrlem2  26862  chordthmlem2  26876  chordthmlem4  26878  heron  26881  atanlogsublem  26958  atantan  26966  birthdaylem3  26996  logdifbnd  27037  emcllem1  27039  emcllem2  27040  emcllem5  27043  emcllem6  27044  harmonicbnd4  27054  fsumharmonic  27055  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamucov  27081  relgamcl  27105  ftalem2  27117  ftalem5  27120  chpub  27264  logfaclbnd  27266  logfacbnd3  27267  logexprlim  27269  bposlem1  27328  bposlem9  27336  gausslemma2dlem1a  27409  lgseisenlem1  27419  lgsquadlem1  27424  2sqmod  27480  chtppilimlem1  27517  vmadivsum  27526  vmadivsumb  27527  rplogsumlem1  27528  rplogsumlem2  27529  rpvmasumlem  27531  dchrisumlem2  27534  dchrisum0re  27557  rplogsum  27571  mulogsumlem  27575  mulog2sumlem1  27578  vmalogdivsum2  27582  vmalogdivsum  27583  2vmadivsumlem  27584  log2sumbnd  27588  selbergb  27593  selberg2lem  27594  selberg2b  27596  chpdifbndlem1  27597  selberg3lem1  27601  selberg3lem2  27602  selberg3  27603  selberg4lem1  27604  selberg4  27605  pntrf  27607  pntrmax  27608  pntrsumo1  27609  selberg3r  27613  selberg4r  27614  selberg34r  27615  pntrlog2bndlem1  27621  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntrlog2bndlem6  27627  pntrlog2bnd  27628  pntpbnd1a  27629  pntpbnd2  27631  pntibndlem2  27635  pntlemg  27642  pntlemn  27644  pntlemj  27647  pntlemf  27649  pntlemo  27651  pntlem3  27653  pntleml  27655  ttgcontlem1  28899  eqeelen  28919  brbtwn2  28920  colinearalg  28925  axcgrid  28931  axsegconlem1  28932  axsegconlem3  28934  axsegconlem8  28939  axsegconlem9  28940  axsegconlem10  28941  ax5seglem3a  28945  ax5seg  28953  axpaschlem  28955  axcontlem8  28986  nbusgrvtxm1  29396  crctcshwlkn0lem3  29832  crctcshwlkn0lem5  29834  crctcsh  29844  clwlkclwwlklem2fv2  30015  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  nvabs  30691  dipcj  30733  minvecolem4  30899  lt2addrd  32755  xlt2addrd  32762  fzsplit3  32795  bcm1n  32797  ply1degltel  33615  ply1degltlss  33617  submateqlem1  33806  cnre2csqlem  33909  tpr2rico  33911  dya2ub  34272  dya2icoseg  34279  ballotlemfcc  34496  ballotlemfrcn0  34532  sgnsub  34547  signslema  34577  ftc2re  34613  subfacval3  35194  dnibndlem8  36486  dnibndlem10  36488  dnibndlem11  36489  dnibndlem12  36490  dnicn  36493  knoppcnlem4  36497  unblimceq0  36508  unbdqndv2lem2  36511  knoppndvlem11  36523  knoppndvlem14  36526  knoppndvlem15  36527  knoppndvlem17  36529  knoppndvlem20  36532  irrdifflemf  37326  poimirlem29  37656  broucube  37661  opnmbllem0  37663  mblfinlem3  37666  mblfinlem4  37667  itg2addnclem  37678  itg2addnclem3  37680  itg2gt0cn  37682  ftc1cnnclem  37698  areacirclem1  37715  areacirclem2  37716  areacirclem4  37718  areacirclem5  37719  areacirc  37720  cntotbnd  37803  rrnmet  37836  rrndstprj1  37837  rrndstprj2  37838  lcmineqlem23  42052  intlewftc  42062  aks4d1p1p2  42071  aks4d1p1p4  42072  dvle2  42073  aks4d1p1  42077  primrootlekpowne0  42106  hashscontpow1  42122  aks6d1c2  42131  aks6d1c5lem2  42139  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  aks6d1c6lem3  42173  bcled  42179  bcle2d  42180  unitscyglem2  42197  unitscyglem4  42199  metakunt1  42206  metakunt7  42212  metakunt16  42221  metakunt18  42223  metakunt28  42233  metakunt29  42234  metakunt30  42235  readdrcl2d  42308  frlmvscadiccat  42516  fltnlta  42673  3cubeslem2  42696  3cubeslem4  42700  irrapxlem2  42834  irrapxlem3  42835  irrapxlem4  42836  irrapxlem5  42837  pellexlem2  42841  pellexlem6  42845  pell1qrgaplem  42884  rmspecsqrtnq  42917  rmspecfund  42920  rmspecpos  42928  jm2.24nn  42971  jm2.17c  42974  fzmaxdif  42993  acongeq  42995  modabsdifz  42998  jm3.1lem2  43030  areaquad  43228  sqrtcvallem2  43650  sqrtcvallem3  43651  sqrtcval  43654  imo72b2lem0  44178  cvgdvgrat  44332  hashnzfzclim  44341  binomcxplemdvbinom  44372  oddfl  45289  lefldiveq  45304  fperiodmul  45316  fzdifsuc2  45322  suprltrp  45339  supxrgere  45344  supxrgelem  45348  suplesup  45350  infleinflem2  45382  infleinf  45383  xrralrecnnge  45401  iccshift  45531  iooshift  45535  iooiinicc  45555  fmul01lt1lem2  45600  climinf  45621  sumnnodd  45645  ltmod  45653  lptre2pt  45655  climleltrp  45691  limsupgtlem  45792  liminflimsupclim  45822  fperdvper  45934  dvbdfbdioolem1  45943  dvbdfbdioolem2  45944  dvbdfbdioo  45945  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnmul  45958  iblspltprt  45988  itgspltprt  45994  itgiccshift  45995  itgperiod  45996  itgsbtaddcnst  45997  sublevolico  45999  stoweidlem1  46016  stoweidlem11  46026  stoweidlem12  46027  stoweidlem13  46028  stoweidlem14  46029  stoweidlem23  46038  stoweidlem24  46039  stoweidlem25  46040  stoweidlem26  46041  stoweidlem34  46049  stoweidlem40  46055  stoweidlem41  46056  stoweidlem42  46057  stoweidlem45  46060  stoweidlem60  46075  stoweidlem62  46077  wallispilem3  46082  wallispilem4  46083  wallispi  46085  wallispi2lem1  46086  stirlinglem5  46093  stirlinglem11  46099  stirlinglem12  46100  dirkercncflem1  46118  fourierdlem4  46126  fourierdlem6  46128  fourierdlem7  46129  fourierdlem9  46131  fourierdlem13  46135  fourierdlem14  46136  fourierdlem15  46137  fourierdlem19  46141  fourierdlem26  46148  fourierdlem35  46157  fourierdlem39  46161  fourierdlem40  46162  fourierdlem41  46163  fourierdlem42  46164  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem51  46172  fourierdlem56  46177  fourierdlem57  46178  fourierdlem59  46180  fourierdlem60  46181  fourierdlem61  46182  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem66  46187  fourierdlem68  46189  fourierdlem71  46192  fourierdlem72  46193  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem78  46199  fourierdlem79  46200  fourierdlem81  46202  fourierdlem82  46203  fourierdlem83  46204  fourierdlem84  46205  fourierdlem88  46209  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem92  46213  fourierdlem93  46214  fourierdlem95  46216  fourierdlem97  46218  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fourierdlem107  46228  fourierdlem109  46230  fourierdlem111  46232  fouriersw  46246  elaa2lem  46248  etransclem23  46272  rrxtopnfi  46302  rrndistlt  46305  ioorrnopnlem  46319  ioorrnopnxrlem  46321  sge0gtfsumgt  46458  iundjiun  46475  volicorecl  46561  hoiprodcl  46562  hoiprodcl3  46595  volicore  46596  hoidmvcl  46597  hoidmv1lelem2  46607  hoidmv1lelem3  46608  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem2  46611  hoiqssbllem1  46637  hoiqssbllem2  46638  hoiqssbllem3  46639  hspmbllem1  46641  ovolval5lem1  46667  ovolval5lem2  46668  iunhoiioolem  46690  iccvonmbllem  46693  vonicclem1  46698  preimageiingt  46735  salpreimagtge  46740  smfaddlem1  46778  smflimlem4  46789  smfmullem1  46806  smfmullem2  46807  smfmullem3  46808  ltsubsubaddltsub  47313  2elfz2melfz  47330  requad01  47608  requad1  47609  requad2  47610  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  bgoldbtbndlem4  47795  bgoldbtbnd  47796  2tceilhalfelfzo1  48018  gpgedgvtx0  48019  gpgedgvtx1  48020  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx13starlem2  48028  ply1mulgsumlem2  48304  difmodm1lt  48443  nnpw2pmod  48504  dignn0flhalflem1  48536  affinecomb1  48623  rrxlinesc  48656  rrxlinec  48657  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659  rrx2vlinest  48662  rrx2linest2  48665  2sphere  48670  line2  48673  itsclc0lem2  48678  itsclc0lem3  48679  itscnhlc0yqe  48680  itsclc0yqsollem2  48684  itsclc0yqsol  48685  itscnhlc0xyqsol  48686  itsclinecirc0  48694  itsclinecirc0b  48695  itsclinecirc0in  48696  itsclquadb  48697  2itscp  48702  itscnhlinecirc02plem1  48703  itscnhlinecirc02p  48706  inlinecirc02plem  48707  amgmwlem  49321