Theorem resubcld 11606

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7387  ℝcr 11067   − cmin 11405

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-ltxr 11213  df-sub 11407  df-neg 11408

This theorem is referenced by:  ltsubadd  11648  lesubadd  11650  lesub1  11672  lesub2  11673  ltsub1  11674  ltsub2  11675  lt2sub  11676  le2sub  11677  ltmul1a  12031  supaddc  12150  cru  12178  ge2halflem1  13068  qbtwnre  13159  lincmb01cmp  13456  iccf1o  13457  xov1plusxeqvd  13459  intfracq  13821  fldiv  13822  modlt  13842  modsubdir  13905  modsumfzodifsn  13909  serle  14022  expmulnbnd  14200  discr  14205  fzsdom2  14393  cshwidxmod  14768  crre  15080  remullem  15094  01sqrexlem7  15214  absrdbnd  15308  fzomaxdiflem  15309  caubnd2  15324  amgm2  15336  icodiamlt  15404  bhmafibid1  15434  mulcn2  15562  reccn2  15563  rlimo1  15583  climle  15606  climsqz  15607  climsqz2  15608  rlimle  15614  isercolllem1  15631  climsup  15636  caucvgrlem  15639  caucvgrlem2  15641  iseraltlem2  15649  iseraltlem3  15650  iseralt  15651  fsumle  15765  cvgcmp  15782  cvgcmpce  15784  bpoly4  16025  eflt  16085  resinhcl  16124  tanhlt1  16128  sin01bnd  16153  sin01gt0  16158  moddvds  16233  bitscmp  16408  bitsinv1lem  16411  smueqlem  16460  modprm0  16776  pcbc  16871  4sqlem15  16930  blss2ps  24291  blss2  24292  blssps  24312  blss  24313  nm2dif  24513  nlmvscnlem2  24573  nrginvrcnlem  24579  iccntr  24710  icccmplem2  24712  metdstri  24740  cnllycmp  24855  evth  24858  lebnumii  24865  ipcnlem2  25144  cncmet  25222  rrxds  25293  rrxmval  25305  rrxmet  25308  rrxdstprj1  25309  rrxdsfi  25311  ehl1eudis  25320  ehl2eudis  25322  minveclem3b  25328  minveclem4  25332  ivthlem2  25353  ivthlem3  25354  ovollb2lem  25389  ovoliunlem1  25403  ovolscalem1  25414  ovolicc1  25417  ovolicc2lem4  25421  ovolicc2  25423  ovolicc  25424  voliunlem2  25452  ovolioo  25469  ioorcl2  25473  uniioovol  25480  uniioombllem2  25484  uniioombllem3a  25485  uniioombllem3  25486  uniioombllem4  25487  uniioombllem6  25489  opnmbllem  25502  volcn  25507  vitalilem2  25510  ismbf3d  25555  mbfaddlem  25561  i1fadd  25596  itg1addlem4  25600  mbfi1fseqlem6  25621  itg2seq  25643  itg2split  25650  itg2cnlem2  25663  itg2cn  25664  itgrevallem1  25696  dvcjbr  25853  dvferm1lem  25888  dvferm2lem  25890  cmvth  25895  cmvthOLD  25896  mvth  25897  dvlip  25898  dvlip2  25900  c1liplem1  25901  dvgt0  25909  dvlt0  25910  dvge0  25911  dvle  25912  dvivthlem1  25913  lhop1lem  25918  lhop  25921  dvcnvrelem1  25922  dvcnvrelem2  25923  dvcnvre  25924  dvcvx  25925  dvfsumle  25926  dvfsumleOLD  25927  dvfsumge  25928  dvfsumrlimf  25931  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem3  25935  dvfsumlem4  25936  dvfsum2  25941  ftc1a  25944  ftc1lem4  25946  coe1mul3  26004  ply1divex  26042  plydivex  26205  aalioulem2  26241  aalioulem3  26242  aalioulem4  26243  aalioulem5  26244  aalioulem6  26245  aaliou3lem7  26257  taylthlem2  26282  taylthlem2OLD  26283  mtest  26313  pilem2  26362  tangtx  26414  cosordlem  26439  efif1olem2  26452  logcnlem3  26553  logcnlem4  26554  isosctrlem2  26729  chordthmlem2  26743  chordthmlem4  26745  heron  26748  atanlogsublem  26825  atantan  26833  birthdaylem3  26863  logdifbnd  26904  emcllem1  26906  emcllem2  26907  emcllem5  26910  emcllem6  26911  harmonicbnd4  26921  fsumharmonic  26922  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamucov  26948  relgamcl  26972  ftalem2  26984  ftalem5  26987  chpub  27131  logfaclbnd  27133  logfacbnd3  27134  logexprlim  27136  bposlem1  27195  bposlem9  27203  gausslemma2dlem1a  27276  lgseisenlem1  27286  lgsquadlem1  27291  2sqmod  27347  chtppilimlem1  27384  vmadivsum  27393  vmadivsumb  27394  rplogsumlem1  27395  rplogsumlem2  27396  rpvmasumlem  27398  dchrisumlem2  27401  dchrisum0re  27424  rplogsum  27438  mulogsumlem  27442  mulog2sumlem1  27445  vmalogdivsum2  27449  vmalogdivsum  27450  2vmadivsumlem  27451  log2sumbnd  27455  selbergb  27460  selberg2lem  27461  selberg2b  27463  chpdifbndlem1  27464  selberg3lem1  27468  selberg3lem2  27469  selberg3  27470  selberg4lem1  27471  selberg4  27472  pntrf  27474  pntrmax  27475  pntrsumo1  27476  selberg3r  27480  selberg4r  27481  selberg34r  27482  pntrlog2bndlem1  27488  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntrlog2bnd  27495  pntpbnd1a  27496  pntpbnd2  27498  pntibndlem2  27502  pntlemg  27509  pntlemn  27511  pntlemj  27514  pntlemf  27516  pntlemo  27518  pntlem3  27520  pntleml  27522  ttgcontlem1  28812  eqeelen  28831  brbtwn2  28832  colinearalg  28837  axcgrid  28843  axsegconlem1  28844  axsegconlem3  28846  axsegconlem8  28851  axsegconlem9  28852  axsegconlem10  28853  ax5seglem3a  28857  ax5seg  28865  axpaschlem  28867  axcontlem8  28898  nbusgrvtxm1  29306  crctcshwlkn0lem3  29742  crctcshwlkn0lem5  29744  crctcsh  29754  clwlkclwwlklem2fv2  29925  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  nvabs  30601  dipcj  30643  minvecolem4  30809  lt2addrd  32674  xlt2addrd  32682  fzsplit3  32716  bcm1n  32718  sgnsub  32762  ply1degltel  33560  ply1degltlss  33562  iconstr  33756  constrresqrtcl  33767  cos9thpiminplylem1  33772  submateqlem1  33797  cnre2csqlem  33900  tpr2rico  33902  dya2ub  34261  dya2icoseg  34268  ballotlemfcc  34485  ballotlemfrcn0  34521  signslema  34553  ftc2re  34589  subfacval3  35176  dnibndlem8  36473  dnibndlem10  36475  dnibndlem11  36476  dnibndlem12  36477  dnicn  36480  knoppcnlem4  36484  unblimceq0  36495  unbdqndv2lem2  36498  knoppndvlem11  36510  knoppndvlem14  36513  knoppndvlem15  36514  knoppndvlem17  36516  knoppndvlem20  36519  irrdifflemf  37313  poimirlem29  37643  broucube  37648  opnmbllem0  37650  mblfinlem3  37653  mblfinlem4  37654  itg2addnclem  37665  itg2addnclem3  37667  itg2gt0cn  37669  ftc1cnnclem  37685  areacirclem1  37702  areacirclem2  37703  areacirclem4  37705  areacirclem5  37706  areacirc  37707  cntotbnd  37790  rrnmet  37823  rrndstprj1  37824  rrndstprj2  37825  lcmineqlem23  42039  intlewftc  42049  aks4d1p1p2  42058  aks4d1p1p4  42059  dvle2  42060  aks4d1p1  42064  primrootlekpowne0  42093  hashscontpow1  42109  aks6d1c2  42118  aks6d1c5lem2  42126  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  aks6d1c6lem3  42160  bcled  42166  bcle2d  42167  unitscyglem2  42184  unitscyglem4  42186  readdrcl2d  42261  frlmvscadiccat  42494  fltnlta  42651  3cubeslem2  42673  3cubeslem4  42677  irrapxlem2  42811  irrapxlem3  42812  irrapxlem4  42813  irrapxlem5  42814  pellexlem2  42818  pellexlem6  42822  pell1qrgaplem  42861  rmspecsqrtnq  42894  rmspecfund  42897  rmspecpos  42905  jm2.24nn  42948  jm2.17c  42951  fzmaxdif  42970  acongeq  42972  modabsdifz  42975  jm3.1lem2  43007  areaquad  43205  sqrtcvallem2  43626  sqrtcvallem3  43627  sqrtcval  43630  imo72b2lem0  44154  cvgdvgrat  44302  hashnzfzclim  44311  binomcxplemdvbinom  44342  oddfl  45276  lefldiveq  45290  fperiodmul  45302  fzdifsuc2  45308  suprltrp  45324  supxrgere  45329  supxrgelem  45333  suplesup  45335  infleinflem2  45367  infleinf  45368  xrralrecnnge  45386  iccshift  45516  iooshift  45520  iooiinicc  45540  fmul01lt1lem2  45583  climinf  45604  sumnnodd  45628  ltmod  45636  lptre2pt  45638  climleltrp  45674  limsupgtlem  45775  liminflimsupclim  45805  fperdvper  45917  dvbdfbdioolem1  45926  dvbdfbdioolem2  45927  dvbdfbdioo  45928  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnmul  45941  iblspltprt  45971  itgspltprt  45977  itgiccshift  45978  itgperiod  45979  itgsbtaddcnst  45980  sublevolico  45982  stoweidlem1  45999  stoweidlem11  46009  stoweidlem12  46010  stoweidlem13  46011  stoweidlem14  46012  stoweidlem23  46021  stoweidlem24  46022  stoweidlem25  46023  stoweidlem26  46024  stoweidlem34  46032  stoweidlem40  46038  stoweidlem41  46039  stoweidlem42  46040  stoweidlem45  46043  stoweidlem60  46058  stoweidlem62  46060  wallispilem3  46065  wallispilem4  46066  wallispi  46068  wallispi2lem1  46069  stirlinglem5  46076  stirlinglem11  46082  stirlinglem12  46083  dirkercncflem1  46101  fourierdlem4  46109  fourierdlem6  46111  fourierdlem7  46112  fourierdlem9  46114  fourierdlem13  46118  fourierdlem14  46119  fourierdlem15  46120  fourierdlem19  46124  fourierdlem26  46131  fourierdlem35  46140  fourierdlem39  46144  fourierdlem40  46145  fourierdlem41  46146  fourierdlem42  46147  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem51  46155  fourierdlem56  46160  fourierdlem57  46161  fourierdlem59  46163  fourierdlem60  46164  fourierdlem61  46165  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem66  46170  fourierdlem68  46172  fourierdlem71  46175  fourierdlem72  46176  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem78  46182  fourierdlem79  46183  fourierdlem81  46185  fourierdlem82  46186  fourierdlem83  46187  fourierdlem84  46188  fourierdlem88  46192  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem92  46196  fourierdlem93  46197  fourierdlem95  46199  fourierdlem97  46201  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fourierdlem107  46211  fourierdlem109  46213  fourierdlem111  46215  fouriersw  46229  elaa2lem  46231  etransclem23  46255  rrxtopnfi  46285  rrndistlt  46288  ioorrnopnlem  46302  ioorrnopnxrlem  46304  sge0gtfsumgt  46441  iundjiun  46458  volicorecl  46544  hoiprodcl  46545  hoiprodcl3  46578  volicore  46579  hoidmvcl  46580  hoidmv1lelem2  46590  hoidmv1lelem3  46591  hoidmv1le  46592  hoidmvlelem1  46593  hoidmvlelem2  46594  hoiqssbllem1  46620  hoiqssbllem2  46621  hoiqssbllem3  46622  hspmbllem1  46624  ovolval5lem1  46650  ovolval5lem2  46651  iunhoiioolem  46673  iccvonmbllem  46676  vonicclem1  46681  preimageiingt  46718  salpreimagtge  46723  smfaddlem1  46761  smflimlem4  46772  smfmullem1  46789  smfmullem2  46790  smfmullem3  46791  ltsubsubaddltsub  47302  2elfz2melfz  47319  2tceilhalfelfzo1  47333  requad01  47622  requad1  47623  requad2  47624  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbndlem4  47809  bgoldbtbnd  47810  gpgedgvtx0  48052  gpgedgvtx1  48053  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx13starlem2  48063  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