Theorem resubcld 11667

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7414  ℝcr 11124   − cmin 11466

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-resscn 11182  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-mulcom 11189  ax-addass 11190  ax-mulass 11191  ax-distr 11192  ax-i2m1 11193  ax-1ne0 11194  ax-1rid 11195  ax-rnegex 11196  ax-rrecex 11197  ax-cnre 11198  ax-pre-lttri 11199  ax-pre-lttrn 11200  ax-pre-ltadd 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-er 8697  df-en 8954  df-dom 8955  df-sdom 8956  df-pnf 11270  df-mnf 11271  df-ltxr 11273  df-sub 11468  df-neg 11469

This theorem is used by:  ltsubadd  11709  lesubadd  11711  lesub1  11733  lesub2  11734  ltsub1  11735  ltsub2  11736  lt2sub  11737  le2sub  11738  ltmul1a  12089  supaddc  12207  cru  12235  ge2halflem1  13160  qbtwnre  13252  lincmb01cmp  13549  iccf1o  13550  xov1plusxeqvd  13552  intfracq  13921  fldiv  13922  modlt  13942  modsubdir  14005  modsumfzodifsn  14009  serle  14122  expmulnbnd  14300  discr  14305  fzsdom2  14494  cshwidxmod  14875  sgnsub  15180  crre  15202  remullem  15216  01sqrexlem7  15336  absrdbnd  15430  fzomaxdiflem  15431  caubnd2  15446  amgm2  15458  icodiamlt  15526  bhmafibid1  15556  mulcn2  15684  reccn2  15685  rlimo1  15705  climle  15728  climsqz  15729  climsqz2  15730  rlimle  15736  isercolllem1  15753  climsup  15758  caucvgrlem  15761  caucvgrlem2  15763  iseraltlem2  15771  iseraltlem3  15772  iseralt  15773  fsumle  15887  cvgcmp  15904  cvgcmpce  15906  bpoly4  16146  eflt  16206  resinhcl  16245  tanhlt1  16249  sin01bnd  16274  sin01gt0  16279  moddvds  16354  bitscmp  16529  bitsinv1lem  16532  smueqlem  16581  modprm0  16898  pcbc  16993  4sqlem15  17052  blss2ps  24630  blss2  24631  blssps  24651  blss  24652  nm2dif  24852  nlmvscnlem2  24912  nrginvrcnlem  24918  iccntr  25049  icccmplem2  25051  metdstri  25079  cnllycmp  25185  evth  25188  lebnumii  25195  ipcnlem2  25473  cncmet  25551  rrxds  25622  rrxmval  25634  rrxmet  25637  rrxdstprj1  25638  rrxdsfi  25640  ehl1eudis  25649  ehl2eudis  25651  minveclem3b  25657  minveclem4  25661  ivthlem2  25681  ivthlem3  25682  ovollb2lem  25717  ovoliunlem1  25731  ovolscalem1  25742  ovolicc1  25745  ovolicc2lem4  25749  ovolicc2  25751  ovolicc  25752  voliunlem2  25780  ovolioo  25797  ioorcl2  25801  uniioovol  25808  uniioombllem2  25812  uniioombllem3a  25813  uniioombllem3  25814  uniioombllem4  25815  uniioombllem6  25817  opnmbllem  25830  volcn  25835  vitalilem2  25838  ismbf3d  25883  mbfaddlem  25889  i1fadd  25924  itg1addlem4  25928  mbfi1fseqlem6  25949  itg2seq  25971  itg2split  25978  itg2cnlem2  25991  itg2cn  25992  itgrevallem1  26023  dvcjbr  26177  dvferm1lem  26212  dvferm2lem  26214  cmvth  26219  mvth  26220  dvlip  26221  dvlip2  26223  c1liplem1  26224  dvgt0  26232  dvlt0  26233  dvge0  26234  dvle  26235  dvivthlem1  26236  lhop1lem  26241  lhop  26244  dvcnvrelem1  26245  dvcnvrelem2  26246  dvcnvre  26247  dvcvx  26248  dvfsumle  26249  dvfsumge  26250  dvfsumrlimf  26253  dvfsumlem2  26255  dvfsumlem3  26256  dvfsumlem4  26257  dvfsum2  26262  ftc1a  26265  ftc1lem4  26267  coe1mul3  26325  ply1divex  26363  plydivex  26528  aalioulem2  26570  aalioulem3  26571  aalioulem4  26572  aalioulem5  26573  aalioulem6  26574  aaliou3lem7  26586  taylthlem2  26611  mtest  26641  pilem2  26689  tangtx  26744  cosordlem  26768  efif1olem2  26781  logcnlem3  26882  logcnlem4  26883  isosctrlem2  27057  chordthmlem2  27071  chordthmlem4  27073  heron  27076  atanlogsublem  27153  atantan  27161  birthdaylem3  27191  logdifbnd  27231  emcllem1  27233  emcllem2  27234  emcllem5  27237  emcllem6  27238  harmonicbnd4  27248  fsumharmonic  27249  lgamgulmlem2  27267  lgamgulmlem3  27268  lgamucov  27275  relgamcl  27299  ftalem2  27311  ftalem5  27314  chpub  27457  logfaclbnd  27459  logfacbnd3  27460  logexprlim  27462  bposlem1  27521  bposlem9  27529  gausslemma2dlem1a  27602  lgseisenlem1  27612  lgsquadlem1  27617  2sqmod  27673  chtppilimlem1  27710  vmadivsum  27719  vmadivsumb  27720  rplogsumlem1  27721  rplogsumlem2  27722  rpvmasumlem  27724  dchrisumlem2  27727  dchrisum0re  27750  rplogsum  27764  mulogsumlem  27768  mulog2sumlem1  27771  vmalogdivsum2  27775  vmalogdivsum  27776  2vmadivsumlem  27777  log2sumbnd  27781  selbergb  27786  selberg2lem  27787  selberg2b  27789  chpdifbndlem1  27790  selberg3lem1  27794  selberg3lem2  27795  selberg3  27796  selberg4lem1  27797  selberg4  27798  pntrf  27800  pntrmax  27801  pntrsumo1  27802  selberg3r  27806  selberg4r  27807  selberg34r  27808  pntrlog2bndlem1  27814  pntrlog2bndlem2  27815  pntrlog2bndlem3  27816  pntrlog2bndlem4  27817  pntrlog2bndlem5  27818  pntrlog2bndlem6  27820  pntrlog2bnd  27821  pntpbnd1a  27822  pntpbnd2  27824  pntibndlem2  27828  pntlemg  27835  pntlemn  27837  pntlemj  27840  pntlemf  27842  pntlemo  27844  pntlem3  27846  pntleml  27848  ttgcontlem1  29342  eqeelen  29362  brbtwn2  29363  colinearalg  29368  axcgrid  29374  axsegconlem1  29375  axsegconlem3  29377  axsegconlem8  29382  axsegconlem9  29383  axsegconlem10  29384  ax5seglem3a  29388  ax5seg  29396  axpaschlem  29398  axcontlem8  29429  nbusgrvtxm1  29840  crctcshwlkn0lem3  30281  crctcshwlkn0lem5  30283  crctcsh  30293  clwlkclwwlklem2fv2  30467  clwlkclwwlklem2a4  30468  clwlkclwwlklem2a  30469  nvabs  31154  dipcj  31196  minvecolem4  31362  lt2addrd  33222  xlt2addrd  33231  fzsplit3  33265  bcm1n  33267  ply1degltel  34005  ply1degltlss  34007  iconstr  34277  constrresqrtcl  34288  cos9thpiminplylem1  34293  submateqlem1  34318  cnre2csqlem  34421  tpr2rico  34423  dya2ub  34782  dya2icoseg  34789  ballotlemfcc  35006  ballotlemfrcn0  35042  signslema  35071  ftc2re  35107  subfacval3  35769  dnibndlem8  37183  dnibndlem10  37185  dnibndlem11  37186  dnibndlem12  37187  dnicn  37190  knoppcnlem4  37194  unblimceq0  37205  unbdqndv2lem2  37208  knoppndvlem11  37220  knoppndvlem14  37223  knoppndvlem15  37224  knoppndvlem17  37226  knoppndvlem20  37229  irrdifflemf  38078  qdiff  38080  poimirlem29  38399  broucube  38404  opnmbllem0  38406  mblfinlem3  38409  mblfinlem4  38410  itg2addnclem  38421  itg2addnclem3  38423  itg2gt0cn  38425  ftc1cnnclem  38441  areacirclem1  38458  areacirclem2  38459  areacirclem4  38461  areacirclem5  38462  areacirc  38463  cntotbnd  38547  rrnmet  38580  rrndstprj1  38581  rrndstprj2  38582  lcmineqlem23  42918  intlewftc  42928  aks4d1p1p2  42937  aks4d1p1p4  42938  dvle2  42939  aks4d1p1  42943  primrootlekpowne0  42972  hashscontpow1  42988  aks6d1c2  42997  aks6d1c5lem2  43005  sticksstones10  43022  sticksstones12a  43024  sticksstones12  43025  aks6d1c6lem3  43039  bcled  43045  bcle2d  43046  unitscyglem2  43063  unitscyglem4  43065  readdrcl2d  43149  frlmvscadiccat  43395  fltnlta  43510  3cubeslem2  43531  3cubeslem4  43535  irrapxlem2  43665  irrapxlem3  43666  irrapxlem4  43667  irrapxlem5  43668  pellexlem2  43672  pellexlem6  43676  pell1qrgaplem  43715  rmspecsqrtnq  43748  rmspecfund  43751  rmspecpos  43758  jm2.24nn  43801  jm2.17c  43804  fzmaxdif  43823  acongeq  43825  modabsdifz  43828  jm3.1lem2  43860  areaquad  44058  sqrtcvallem2  44478  sqrtcvallem3  44479  sqrtcval  44482  imo72b2lem0  45006  cvgdvgrat  45138  hashnzfzclim  45147  binomcxplemdvbinom  45178  oddfl  46112  lefldiveq  46126  fperiodmul  46138  fzdifsuc2  46144  suprltrp  46159  supxrgere  46164  supxrgelem  46168  suplesup  46170  infleinflem2  46201  infleinf  46202  xrralrecnnge  46220  iccshift  46349  iooshift  46353  iooiinicc  46373  fmul01lt1lem2  46416  climinf  46437  sumnnodd  46461  ltmod  46467  lptre2pt  46469  climleltrp  46505  limsupgtlem  46606  liminflimsupclim  46636  fperdvper  46748  dvbdfbdioolem1  46757  dvbdfbdioolem2  46758  dvbdfbdioo  46759  ioodvbdlimc1lem1  46760  ioodvbdlimc1lem2  46761  ioodvbdlimc2lem  46763  dvnmul  46772  iblspltprt  46802  itgspltprt  46808  itgiccshift  46809  itgperiod  46810  itgsbtaddcnst  46811  sublevolico  46813  stoweidlem1  46830  stoweidlem11  46840  stoweidlem12  46841  stoweidlem13  46842  stoweidlem14  46843  stoweidlem23  46852  stoweidlem24  46853  stoweidlem25  46854  stoweidlem26  46855  stoweidlem34  46863  stoweidlem40  46869  stoweidlem41  46870  stoweidlem42  46871  stoweidlem45  46874  stoweidlem60  46889  stoweidlem62  46891  wallispilem3  46896  wallispilem4  46897  wallispi  46899  wallispi2lem1  46900  stirlinglem5  46907  stirlinglem11  46913  stirlinglem12  46914  dirkercncflem1  46932  fourierdlem4  46940  fourierdlem6  46942  fourierdlem7  46943  fourierdlem9  46945  fourierdlem13  46949  fourierdlem14  46950  fourierdlem15  46951  fourierdlem19  46955  fourierdlem26  46962  fourierdlem35  46971  fourierdlem39  46975  fourierdlem40  46976  fourierdlem41  46977  fourierdlem42  46978  fourierdlem48  46983  fourierdlem49  46984  fourierdlem50  46985  fourierdlem51  46986  fourierdlem56  46991  fourierdlem57  46992  fourierdlem59  46994  fourierdlem60  46995  fourierdlem61  46996  fourierdlem63  46998  fourierdlem64  46999  fourierdlem65  47000  fourierdlem66  47001  fourierdlem68  47003  fourierdlem71  47006  fourierdlem72  47007  fourierdlem73  47008  fourierdlem74  47009  fourierdlem75  47010  fourierdlem76  47011  fourierdlem78  47013  fourierdlem79  47014  fourierdlem81  47016  fourierdlem82  47017  fourierdlem83  47018  fourierdlem84  47019  fourierdlem88  47023  fourierdlem89  47024  fourierdlem90  47025  fourierdlem91  47026  fourierdlem92  47027  fourierdlem93  47028  fourierdlem95  47030  fourierdlem97  47032  fourierdlem101  47036  fourierdlem103  47038  fourierdlem104  47039  fourierdlem107  47042  fourierdlem109  47044  fourierdlem111  47046  fouriersw  47060  elaa2lem  47062  etransclem23  47086  rrxtopnfi  47116  rrndistlt  47119  ioorrnopnlem  47133  ioorrnopnxrlem  47135  sge0gtfsumgt  47272  iundjiun  47289  volicorecl  47375  hoiprodcl  47376  hoiprodcl3  47409  volicore  47410  hoidmvcl  47411  hoidmv1lelem2  47421  hoidmv1lelem3  47422  hoidmv1le  47423  hoidmvlelem1  47424  hoidmvlelem2  47425  hoiqssbllem1  47451  hoiqssbllem2  47452  hoiqssbllem3  47453  hspmbllem1  47455  ovolval5lem1  47481  ovolval5lem2  47482  iunhoiioolem  47504  iccvonmbllem  47507  vonicclem1  47512  preimageiingt  47549  salpreimagtge  47554  smfaddlem1  47592  smflimlem4  47603  smfmullem1  47620  smfmullem2  47621  smfmullem3  47622  ltsubsubaddltsub  48190  2elfz2melfz  48207  2tceilhalfelfzo1  48225  flmrecm1  48232  requad01  48538  requad1  48539  requad2  48540  bgoldbtbndlem2  48723  bgoldbtbndlem3  48724  bgoldbtbndlem4  48725  bgoldbtbnd  48726  gpgedgvtx0  48978  gpgedgvtx1  48979  gpg5nbgrvtx03starlem2  48986  gpg5nbgrvtx13starlem2  48989  ply1mulgsumlem2  49318  nnpw2pmod  49514  dignn0flhalflem1  49546  affinecomb1  49633  rrxlinesc  49666  rrxlinec  49667  eenglngeehlnmlem1  49668  eenglngeehlnmlem2  49669  rrx2vlinest  49672  rrx2linest2  49675  2sphere  49680  line2  49683  itsclc0lem2  49688  itsclc0lem3  49689  itscnhlc0yqe  49690  itsclc0yqsollem2  49694  itsclc0yqsol  49695  itscnhlc0xyqsol  49696  itsclinecirc0  49704  itsclinecirc0b  49705  itsclinecirc0in  49706  itsclquadb  49707  2itscp  49712  itscnhlinecirc02plem1  49713  itscnhlinecirc02p  49716  inlinecirc02plem  49717  crosspcle1d  50789  crosspcle2d  50790  crosspcle3d  50791  crossp3d  50801  amgmwlem  50821