Theorem resubcld 11754

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7427  ℝcr 11209   − cmin 11551

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758  ax-resscn 11267  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-addrcl 11271  ax-mulcl 11272  ax-mulrcl 11273  ax-mulcom 11274  ax-addass 11275  ax-mulass 11276  ax-distr 11277  ax-i2m1 11278  ax-1ne0 11279  ax-1rid 11280  ax-rnegex 11281  ax-rrecex 11282  ax-cnre 11283  ax-pre-lttri 11284  ax-pre-lttrn 11285  ax-pre-ltadd 11286

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3369  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-po 5562  df-so 5563  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-riota 7384  df-ov 7430  df-oprab 7431  df-mpo 7432  df-er 8728  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11355  df-mnf 11356  df-ltxr 11358  df-sub 11553  df-neg 11554

This theorem is used by:  ltsubadd  11796  lesubadd  11798  lesub1  11820  lesub2  11821  ltsub1  11822  ltsub2  11823  lt2sub  11824  le2sub  11825  ltmul1a  12176  supaddc  12294  cru  12322  ge2halflem1  13247  qbtwnre  13339  lincmb01cmp  13636  iccf1o  13637  xov1plusxeqvd  13639  intfracq  14009  fldiv  14010  modlt  14030  modsubdir  14093  modsumfzodifsn  14097  serle  14210  expmulnbnd  14389  discr  14394  fzsdom2  14583  cshwidxmod  14965  sgnsub  15271  crre  15293  remullem  15307  01sqrexlem7  15427  absrdbnd  15521  fzomaxdiflem  15522  caubnd2  15537  amgm2  15549  icodiamlt  15617  bhmafibid1  15647  mulcn2  15775  reccn2  15776  rlimo1  15796  climle  15819  climsqz  15820  climsqz2  15821  rlimle  15827  isercolllem1  15844  climsup  15849  caucvgrlem  15852  caucvgrlem2  15854  iseraltlem2  15862  iseraltlem3  15863  iseralt  15864  fsumle  15978  cvgcmp  15995  cvgcmpce  15997  bpoly4  16237  eflt  16297  resinhcl  16336  tanhlt1  16340  sin01bnd  16365  sin01gt0  16370  moddvds  16445  bitscmp  16620  bitsinv1lem  16623  smueqlem  16672  modprm0  16995  pcbc  17090  4sqlem15  17149  blss2ps  24734  blss2  24735  blssps  24755  blss  24756  nm2dif  24956  nlmvscnlem2  25016  nrginvrcnlem  25022  iccntr  25153  icccmplem2  25155  metdstri  25183  cnllycmp  25289  evth  25292  lebnumii  25299  ipcnlem2  25577  cncmet  25655  rrxds  25726  rrxmval  25738  rrxmet  25741  rrxdstprj1  25742  rrxdsfi  25744  ehl1eudis  25753  ehl2eudis  25755  minveclem3b  25761  minveclem4  25765  ivthlem2  25785  ivthlem3  25786  ovollb2lem  25821  ovoliunlem1  25835  ovolscalem1  25846  ovolicc1  25849  ovolicc2lem4  25853  ovolicc2  25855  ovolicc  25856  voliunlem2  25884  ovolioo  25901  ioorcl2  25905  uniioovol  25912  uniioombllem2  25916  uniioombllem3a  25917  uniioombllem3  25918  uniioombllem4  25919  uniioombllem6  25921  opnmbllem  25934  volcn  25939  vitalilem2  25942  ismbf3d  25987  mbfaddlem  25993  i1fadd  26028  itg1addlem4  26032  mbfi1fseqlem6  26053  itg2seq  26075  itg2split  26082  itg2cnlem2  26095  itg2cn  26096  itgrevallem1  26127  dvcjbr  26281  dvferm1lem  26316  dvferm2lem  26318  cmvth  26323  mvth  26324  dvlip  26325  dvlip2  26327  c1liplem1  26328  dvgt0  26336  dvlt0  26337  dvge0  26338  dvle  26339  dvivthlem1  26340  lhop1lem  26345  lhop  26348  dvcnvrelem1  26349  dvcnvrelem2  26350  dvcnvre  26351  dvcvx  26352  dvfsumle  26353  dvfsumge  26354  dvfsumrlimf  26357  dvfsumlem2  26359  dvfsumlem3  26360  dvfsumlem4  26361  dvfsum2  26366  ftc1a  26369  ftc1lem4  26371  coe1mul3  26429  ply1divex  26467  plydivex  26630  aalioulem2  26672  aalioulem3  26673  aalioulem4  26674  aalioulem5  26675  aalioulem6  26676  aaliou3lem7  26688  taylthlem2  26713  mtest  26743  pilem2  26791  tangtx  26846  cosordlem  26870  efif1olem2  26883  logcnlem3  26984  logcnlem4  26985  isosctrlem2  27159  chordthmlem2  27173  chordthmlem4  27175  heron  27178  atanlogsublem  27255  atantan  27263  birthdaylem3  27293  logdifbnd  27333  emcllem1  27335  emcllem2  27336  emcllem5  27339  emcllem6  27340  harmonicbnd4  27350  fsumharmonic  27351  lgamgulmlem2  27369  lgamgulmlem3  27370  lgamucov  27377  relgamcl  27401  ftalem2  27413  ftalem5  27416  chpub  27559  logfaclbnd  27561  logfacbnd3  27562  logexprlim  27564  bposlem1  27623  bposlem9  27631  gausslemma2dlem1a  27704  lgseisenlem1  27714  lgsquadlem1  27719  2sqmod  27775  chtppilimlem1  27812  vmadivsum  27821  vmadivsumb  27822  rplogsumlem1  27823  rplogsumlem2  27824  rpvmasumlem  27826  dchrisumlem2  27829  dchrisum0re  27852  rplogsum  27866  mulogsumlem  27870  mulog2sumlem1  27873  vmalogdivsum2  27877  vmalogdivsum  27878  2vmadivsumlem  27879  log2sumbnd  27883  selbergb  27888  selberg2lem  27889  selberg2b  27891  chpdifbndlem1  27892  selberg3lem1  27896  selberg3lem2  27897  selberg3  27898  selberg4lem1  27899  selberg4  27900  pntrf  27902  pntrmax  27903  pntrsumo1  27904  selberg3r  27908  selberg4r  27909  selberg34r  27910  pntrlog2bndlem1  27916  pntrlog2bndlem2  27917  pntrlog2bndlem3  27918  pntrlog2bndlem4  27919  pntrlog2bndlem5  27920  pntrlog2bndlem6  27922  pntrlog2bnd  27923  pntpbnd1a  27924  pntpbnd2  27926  pntibndlem2  27930  pntlemg  27937  pntlemn  27939  pntlemj  27942  pntlemf  27944  pntlemo  27946  pntlem3  27948  pntleml  27950  ttgcontlem1  29474  eqeelen  29494  brbtwn2  29495  colinearalg  29500  axcgrid  29506  axsegconlem1  29507  axsegconlem3  29509  axsegconlem8  29514  axsegconlem9  29515  axsegconlem10  29516  ax5seglem3a  29520  ax5seg  29528  axpaschlem  29530  axcontlem8  29561  nbusgrvtxm1  29972  crctcshwlkn0lem3  30413  crctcshwlkn0lem5  30415  crctcsh  30425  clwlkclwwlklem2fv2  30599  clwlkclwwlklem2a4  30600  clwlkclwwlklem2a  30601  nvabs  31286  dipcj  31328  minvecolem4  31494  lt2addrd  33395  xlt2addrd  33404  fzsplit3  33438  bcm1n  33440  ply1degltel  34179  ply1degltlss  34181  iconstr  34451  constrresqrtcl  34462  cos9thpiminplylem1  34467  submateqlem1  34492  cnre2csqlem  34595  tpr2rico  34597  dya2ub  34955  dya2icoseg  34962  ballotlemfcc  35179  ballotlemfrcn0  35215  signslema  35244  ftc2re  35280  subfacval3  36075  dnibndlem8  37478  dnibndlem10  37480  dnibndlem11  37481  dnibndlem12  37482  dnicn  37485  knoppcnlem4  37489  unblimceq0  37500  unbdqndv2lem2  37503  knoppndvlem11  37515  knoppndvlem14  37518  knoppndvlem15  37519  knoppndvlem17  37521  knoppndvlem20  37524  irrdifflemf  38386  qdiff  38388  poimirlem29  38707  broucube  38712  opnmbllem0  38714  mblfinlem3  38717  mblfinlem4  38718  itg2addnclem  38729  itg2addnclem3  38731  itg2gt0cn  38733  ftc1cnnclem  38749  areacirclem1  38766  areacirclem2  38767  areacirclem4  38769  areacirclem5  38770  areacirc  38771  cntotbnd  38870  rrnmet  38903  rrndstprj1  38904  rrndstprj2  38905  lcmineqlem23  43241  intlewftc  43251  aks4d1p1p2  43260  aks4d1p1p4  43261  dvle2  43262  aks4d1p1  43266  primrootlekpowne0  43295  hashscontpow1  43311  aks6d1c2  43320  aks6d1c5lem2  43328  sticksstones10  43345  sticksstones12a  43347  sticksstones12  43348  aks6d1c6lem3  43362  bcled  43368  bcle2d  43369  unitscyglem2  43386  unitscyglem4  43388  readdrcl2d  43472  frlmvscadiccat  43713  fltnlta  43814  3cubeslem2  43835  3cubeslem4  43839  irrapxlem2  43970  irrapxlem3  43971  irrapxlem4  43972  irrapxlem5  43973  pellexlem2  43977  pellexlem6  43981  pell1qrgaplem  44020  rmspecsqrtnq  44053  rmspecfund  44056  rmspecpos  44063  jm2.24nn  44106  jm2.17c  44109  fzmaxdif  44128  acongeq  44130  modabsdifz  44133  jm3.1lem2  44165  areaquad  44358  sqrtcvallem2  44777  sqrtcvallem3  44778  sqrtcval  44781  imo72b2lem0  45305  cvgdvgrat  45437  hashnzfzclim  45446  binomcxplemdvbinom  45477  oddfl  46433  lefldiveq  46447  fperiodmul  46459  fzdifsuc2  46465  suprltrp  46479  supxrgere  46484  supxrgelem  46488  suplesup  46490  infleinflem2  46521  infleinf  46522  xrralrecnnge  46540  iccshift  46669  iooshift  46673  iooiinicc  46693  fmul01lt1lem2  46736  climinf  46757  sumnnodd  46781  ltmod  46787  lptre2pt  46789  climleltrp  46825  limsupgtlem  46926  liminflimsupclim  46956  fperdvper  47068  dvbdfbdioolem1  47077  dvbdfbdioolem2  47078  dvbdfbdioo  47079  ioodvbdlimc1lem1  47080  ioodvbdlimc1lem2  47081  ioodvbdlimc2lem  47083  dvnmul  47092  iblspltprt  47122  itgspltprt  47128  itgiccshift  47129  itgperiod  47130  itgsbtaddcnst  47131  sublevolico  47133  stoweidlem1  47150  stoweidlem11  47160  stoweidlem12  47161  stoweidlem13  47162  stoweidlem14  47163  stoweidlem23  47172  stoweidlem24  47173  stoweidlem25  47174  stoweidlem26  47175  stoweidlem34  47183  stoweidlem40  47189  stoweidlem41  47190  stoweidlem42  47191  stoweidlem45  47194  stoweidlem60  47209  stoweidlem62  47211  wallispilem3  47216  wallispilem4  47217  wallispi  47219  wallispi2lem1  47220  stirlinglem5  47227  stirlinglem11  47233  stirlinglem12  47234  dirkercncflem1  47252  fourierdlem4  47260  fourierdlem6  47262  fourierdlem7  47263  fourierdlem9  47265  fourierdlem13  47269  fourierdlem14  47270  fourierdlem15  47271  fourierdlem19  47275  fourierdlem26  47282  fourierdlem35  47291  fourierdlem39  47295  fourierdlem40  47296  fourierdlem41  47297  fourierdlem42  47298  fourierdlem48  47303  fourierdlem49  47304  fourierdlem50  47305  fourierdlem51  47306  fourierdlem56  47311  fourierdlem57  47312  fourierdlem59  47314  fourierdlem60  47315  fourierdlem61  47316  fourierdlem63  47318  fourierdlem64  47319  fourierdlem65  47320  fourierdlem66  47321  fourierdlem68  47323  fourierdlem71  47326  fourierdlem72  47327  fourierdlem73  47328  fourierdlem74  47329  fourierdlem75  47330  fourierdlem76  47331  fourierdlem78  47333  fourierdlem79  47334  fourierdlem81  47336  fourierdlem82  47337  fourierdlem83  47338  fourierdlem84  47339  fourierdlem88  47343  fourierdlem89  47344  fourierdlem90  47345  fourierdlem91  47346  fourierdlem92  47347  fourierdlem93  47348  fourierdlem95  47350  fourierdlem97  47352  fourierdlem101  47356  fourierdlem103  47358  fourierdlem104  47359  fourierdlem107  47362  fourierdlem109  47364  fourierdlem111  47366  fouriersw  47380  elaa2lem  47382  etransclem23  47406  rrxtopnfi  47436  rrndistlt  47439  ioorrnopnlem  47453  ioorrnopnxrlem  47455  sge0gtfsumgt  47592  iundjiun  47609  volicorecl  47695  hoiprodcl  47696  hoiprodcl3  47729  volicore  47730  hoidmvcl  47731  hoidmv1lelem2  47741  hoidmv1lelem3  47742  hoidmv1le  47743  hoidmvlelem1  47744  hoidmvlelem2  47745  hoiqssbllem1  47771  hoiqssbllem2  47772  hoiqssbllem3  47773  hspmbllem1  47775  ovolval5lem1  47801  ovolval5lem2  47802  iunhoiioolem  47824  iccvonmbllem  47827  vonicclem1  47832  preimageiingt  47869  salpreimagtge  47874  smfaddlem1  47912  smflimlem4  47923  smfmullem1  47940  smfmullem2  47941  smfmullem3  47942  ltsubsubaddltsub  48510  2elfz2melfz  48527  2tceilhalfelfzo1  48545  flmrecm1  48552  requad01  48858  requad1  48859  requad2  48860  bgoldbtbndlem2  49043  bgoldbtbndlem3  49044  bgoldbtbndlem4  49045  bgoldbtbnd  49046  gpgedgvtx0  49298  gpgedgvtx1  49299  gpg5nbgrvtx03starlem2  49306  gpg5nbgrvtx13starlem2  49309  ply1mulgsumlem2  49638  nnpw2pmod  49834  dignn0flhalflem1  49866  affinecomb1  49953  rrxlinesc  49987  rrxlinec  49988  eenglngeehlnmlem1  49989  eenglngeehlnmlem2  49990  rrx2vlinest  49992  rrx2linest2  49995  2sphere  50000  itsclc0lem2  50008  itsclc0lem3  50009  itscnhlc0yqe  50010  itsclc0yqsollem2  50014  itsclc0yqsol  50015  itscnhlc0xyqsol  50016  itsclinecirc0  50024  itsclinecirc0b  50025  itsclinecirc0in  50026  itsclquadb  50027  2itscp  50032  itscnhlinecirc02plem1  50033  itscnhlinecirc02p  50036  inlinecirc02plem  50037  crosspcle1d  51169  crosspcle2d  51170  crosspcle3d  51171  crossp3d  51181  amgmwlem  51201