Theorem resubcld 11569

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

Syntax hints:   → wi 4   ∈ wcel 2119  (class class class)co 7356  ℝcr 11028   − cmin 11368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-po 5526  df-so 5527  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-ltxr 11175  df-sub 11370  df-neg 11371

This theorem is referenced by:  ltsubadd  11611  lesubadd  11613  lesub1  11635  lesub2  11636  ltsub1  11637  ltsub2  11638  lt2sub  11639  le2sub  11640  ltmul1a  11995  supaddc  12114  cru  12142  ge2halflem1  13050  qbtwnre  13142  lincmb01cmp  13439  iccf1o  13440  xov1plusxeqvd  13442  intfracq  13809  fldiv  13810  modlt  13830  modsubdir  13893  modsumfzodifsn  13897  serle  14010  expmulnbnd  14188  discr  14193  fzsdom2  14381  cshwidxmod  14756  crre  15067  remullem  15081  01sqrexlem7  15201  absrdbnd  15295  fzomaxdiflem  15296  caubnd2  15311  amgm2  15323  icodiamlt  15391  bhmafibid1  15421  mulcn2  15549  reccn2  15550  rlimo1  15570  climle  15593  climsqz  15594  climsqz2  15595  rlimle  15601  isercolllem1  15618  climsup  15623  caucvgrlem  15626  caucvgrlem2  15628  iseraltlem2  15636  iseraltlem3  15637  iseralt  15638  fsumle  15753  cvgcmp  15770  cvgcmpce  15772  bpoly4  16015  eflt  16075  resinhcl  16114  tanhlt1  16118  sin01bnd  16143  sin01gt0  16148  moddvds  16223  bitscmp  16398  bitsinv1lem  16401  smueqlem  16450  modprm0  16767  pcbc  16862  4sqlem15  16921  blss2ps  24386  blss2  24387  blssps  24407  blss  24408  nm2dif  24608  nlmvscnlem2  24668  nrginvrcnlem  24674  iccntr  24805  icccmplem2  24807  metdstri  24835  cnllycmp  24941  evth  24944  lebnumii  24951  ipcnlem2  25229  cncmet  25307  rrxds  25378  rrxmval  25390  rrxmet  25393  rrxdstprj1  25394  rrxdsfi  25396  ehl1eudis  25405  ehl2eudis  25407  minveclem3b  25413  minveclem4  25417  ivthlem2  25437  ivthlem3  25438  ovollb2lem  25473  ovoliunlem1  25487  ovolscalem1  25498  ovolicc1  25501  ovolicc2lem4  25505  ovolicc2  25507  ovolicc  25508  voliunlem2  25536  ovolioo  25553  ioorcl2  25557  uniioovol  25564  uniioombllem2  25568  uniioombllem3a  25569  uniioombllem3  25570  uniioombllem4  25571  uniioombllem6  25573  opnmbllem  25586  volcn  25591  vitalilem2  25594  ismbf3d  25639  mbfaddlem  25645  i1fadd  25680  itg1addlem4  25684  mbfi1fseqlem6  25705  itg2seq  25727  itg2split  25734  itg2cnlem2  25747  itg2cn  25748  itgrevallem1  25780  dvcjbr  25934  dvferm1lem  25969  dvferm2lem  25971  cmvth  25976  mvth  25977  dvlip  25978  dvlip2  25980  c1liplem1  25981  dvgt0  25989  dvlt0  25990  dvge0  25991  dvle  25992  dvivthlem1  25993  lhop1lem  25998  lhop  26001  dvcnvrelem1  26002  dvcnvrelem2  26003  dvcnvre  26004  dvcvx  26005  dvfsumle  26006  dvfsumge  26007  dvfsumrlimf  26010  dvfsumlem2  26012  dvfsumlem3  26013  dvfsumlem4  26014  dvfsum2  26019  ftc1a  26022  ftc1lem4  26024  coe1mul3  26082  ply1divex  26120  plydivex  26281  aalioulem2  26317  aalioulem3  26318  aalioulem4  26319  aalioulem5  26320  aalioulem6  26321  aaliou3lem7  26333  taylthlem2  26357  mtest  26387  pilem2  26435  tangtx  26487  cosordlem  26512  efif1olem2  26525  logcnlem3  26626  logcnlem4  26627  isosctrlem2  26801  chordthmlem2  26815  chordthmlem4  26817  heron  26820  atanlogsublem  26897  atantan  26905  birthdaylem3  26935  logdifbnd  26975  emcllem1  26977  emcllem2  26978  emcllem5  26981  emcllem6  26982  harmonicbnd4  26992  fsumharmonic  26993  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamucov  27019  relgamcl  27043  ftalem2  27055  ftalem5  27058  chpub  27201  logfaclbnd  27203  logfacbnd3  27204  logexprlim  27206  bposlem1  27265  bposlem9  27273  gausslemma2dlem1a  27346  lgseisenlem1  27356  lgsquadlem1  27361  2sqmod  27417  chtppilimlem1  27454  vmadivsum  27463  vmadivsumb  27464  rplogsumlem1  27465  rplogsumlem2  27466  rpvmasumlem  27468  dchrisumlem2  27471  dchrisum0re  27494  rplogsum  27508  mulogsumlem  27512  mulog2sumlem1  27515  vmalogdivsum2  27519  vmalogdivsum  27520  2vmadivsumlem  27521  log2sumbnd  27525  selbergb  27530  selberg2lem  27531  selberg2b  27533  chpdifbndlem1  27534  selberg3lem1  27538  selberg3lem2  27539  selberg3  27540  selberg4lem1  27541  selberg4  27542  pntrf  27544  pntrmax  27545  pntrsumo1  27546  selberg3r  27550  selberg4r  27551  selberg34r  27552  pntrlog2bndlem1  27558  pntrlog2bndlem2  27559  pntrlog2bndlem3  27560  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntrlog2bndlem6  27564  pntrlog2bnd  27565  pntpbnd1a  27566  pntpbnd2  27568  pntibndlem2  27572  pntlemg  27579  pntlemn  27581  pntlemj  27584  pntlemf  27586  pntlemo  27588  pntlem3  27590  pntleml  27592  ttgcontlem1  28971  eqeelen  28991  brbtwn2  28992  colinearalg  28997  axcgrid  29003  axsegconlem1  29004  axsegconlem3  29006  axsegconlem8  29011  axsegconlem9  29012  axsegconlem10  29013  ax5seglem3a  29017  ax5seg  29025  axpaschlem  29027  axcontlem8  29058  nbusgrvtxm1  29466  crctcshwlkn0lem3  29898  crctcshwlkn0lem5  29900  crctcsh  29910  clwlkclwwlklem2fv2  30084  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  nvabs  30761  dipcj  30803  minvecolem4  30969  lt2addrd  32842  xlt2addrd  32851  fzsplit3  32885  bcm1n  32887  sgnsub  32929  ply1degltel  33677  ply1degltlss  33679  iconstr  33950  constrresqrtcl  33961  cos9thpiminplylem1  33966  submateqlem1  33991  cnre2csqlem  34094  tpr2rico  34096  dya2ub  34454  dya2icoseg  34461  ballotlemfcc  34678  ballotlemfrcn0  34714  signslema  34746  ftc2re  34782  subfacval3  35417  dnibndlem8  36791  dnibndlem10  36793  dnibndlem11  36794  dnibndlem12  36795  dnicn  36798  knoppcnlem4  36802  unblimceq0  36813  unbdqndv2lem2  36816  knoppndvlem11  36828  knoppndvlem14  36831  knoppndvlem15  36832  knoppndvlem17  36834  knoppndvlem20  36837  irrdifflemf  37685  qdiff  37687  poimirlem29  38016  broucube  38021  opnmbllem0  38023  mblfinlem3  38026  mblfinlem4  38027  itg2addnclem  38038  itg2addnclem3  38040  itg2gt0cn  38042  ftc1cnnclem  38058  areacirclem1  38075  areacirclem2  38076  areacirclem4  38078  areacirclem5  38079  areacirc  38080  cntotbnd  38163  rrnmet  38196  rrndstprj1  38197  rrndstprj2  38198  lcmineqlem23  42536  intlewftc  42546  aks4d1p1p2  42555  aks4d1p1p4  42556  dvle2  42557  aks4d1p1  42561  primrootlekpowne0  42590  hashscontpow1  42606  aks6d1c2  42615  aks6d1c5lem2  42623  sticksstones10  42640  sticksstones12a  42642  sticksstones12  42643  aks6d1c6lem3  42657  bcled  42663  bcle2d  42664  unitscyglem2  42681  unitscyglem4  42683  readdrcl2d  42750  frlmvscadiccat  42996  fltnlta  43113  3cubeslem2  43134  3cubeslem4  43138  irrapxlem2  43268  irrapxlem3  43269  irrapxlem4  43270  irrapxlem5  43271  pellexlem2  43275  pellexlem6  43279  pell1qrgaplem  43318  rmspecsqrtnq  43351  rmspecfund  43354  rmspecpos  43361  jm2.24nn  43404  jm2.17c  43407  fzmaxdif  43426  acongeq  43428  modabsdifz  43431  jm3.1lem2  43463  areaquad  43661  sqrtcvallem2  44081  sqrtcvallem3  44082  sqrtcval  44085  imo72b2lem0  44609  cvgdvgrat  44757  hashnzfzclim  44766  binomcxplemdvbinom  44797  oddfl  45726  lefldiveq  45740  fperiodmul  45752  fzdifsuc2  45758  suprltrp  45773  supxrgere  45778  supxrgelem  45782  suplesup  45784  infleinflem2  45815  infleinf  45816  xrralrecnnge  45834  iccshift  45963  iooshift  45967  iooiinicc  45987  fmul01lt1lem2  46030  climinf  46051  sumnnodd  46075  ltmod  46081  lptre2pt  46083  climleltrp  46119  limsupgtlem  46220  liminflimsupclim  46250  fperdvper  46362  dvbdfbdioolem1  46371  dvbdfbdioolem2  46372  dvbdfbdioo  46373  ioodvbdlimc1lem1  46374  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnmul  46386  iblspltprt  46416  itgspltprt  46422  itgiccshift  46423  itgperiod  46424  itgsbtaddcnst  46425  sublevolico  46427  stoweidlem1  46444  stoweidlem11  46454  stoweidlem12  46455  stoweidlem13  46456  stoweidlem14  46457  stoweidlem23  46466  stoweidlem24  46467  stoweidlem25  46468  stoweidlem26  46469  stoweidlem34  46477  stoweidlem40  46483  stoweidlem41  46484  stoweidlem42  46485  stoweidlem45  46488  stoweidlem60  46503  stoweidlem62  46505  wallispilem3  46510  wallispilem4  46511  wallispi  46513  wallispi2lem1  46514  stirlinglem5  46521  stirlinglem11  46527  stirlinglem12  46528  dirkercncflem1  46546  fourierdlem4  46554  fourierdlem6  46556  fourierdlem7  46557  fourierdlem9  46559  fourierdlem13  46563  fourierdlem14  46564  fourierdlem15  46565  fourierdlem19  46569  fourierdlem26  46576  fourierdlem35  46585  fourierdlem39  46589  fourierdlem40  46590  fourierdlem41  46591  fourierdlem42  46592  fourierdlem48  46597  fourierdlem49  46598  fourierdlem50  46599  fourierdlem51  46600  fourierdlem56  46605  fourierdlem57  46606  fourierdlem59  46608  fourierdlem60  46609  fourierdlem61  46610  fourierdlem63  46612  fourierdlem64  46613  fourierdlem65  46614  fourierdlem66  46615  fourierdlem68  46617  fourierdlem71  46620  fourierdlem72  46621  fourierdlem73  46622  fourierdlem74  46623  fourierdlem75  46624  fourierdlem76  46625  fourierdlem78  46627  fourierdlem79  46628  fourierdlem81  46630  fourierdlem82  46631  fourierdlem83  46632  fourierdlem84  46633  fourierdlem88  46637  fourierdlem89  46638  fourierdlem90  46639  fourierdlem91  46640  fourierdlem92  46641  fourierdlem93  46642  fourierdlem95  46644  fourierdlem97  46646  fourierdlem101  46650  fourierdlem103  46652  fourierdlem104  46653  fourierdlem107  46656  fourierdlem109  46658  fourierdlem111  46660  fouriersw  46674  elaa2lem  46676  etransclem23  46700  rrxtopnfi  46730  rrndistlt  46733  ioorrnopnlem  46747  ioorrnopnxrlem  46749  sge0gtfsumgt  46886  iundjiun  46903  volicorecl  46989  hoiprodcl  46990  hoiprodcl3  47023  volicore  47024  hoidmvcl  47025  hoidmv1lelem2  47035  hoidmv1lelem3  47036  hoidmv1le  47037  hoidmvlelem1  47038  hoidmvlelem2  47039  hoiqssbllem1  47065  hoiqssbllem2  47066  hoiqssbllem3  47067  hspmbllem1  47069  ovolval5lem1  47095  ovolval5lem2  47096  iunhoiioolem  47118  iccvonmbllem  47121  vonicclem1  47126  preimageiingt  47163  salpreimagtge  47168  smfaddlem1  47206  smflimlem4  47217  smfmullem1  47234  smfmullem2  47235  smfmullem3  47236  ltsubsubaddltsub  47764  2elfz2melfz  47781  2tceilhalfelfzo1  47799  flmrecm1  47806  requad01  48112  requad1  48113  requad2  48114  bgoldbtbndlem2  48297  bgoldbtbndlem3  48298  bgoldbtbndlem4  48299  bgoldbtbnd  48300  gpgedgvtx0  48552  gpgedgvtx1  48553  gpg5nbgrvtx03starlem2  48560  gpg5nbgrvtx13starlem2  48563  ply1mulgsumlem2  48878  nnpw2pmod  49074  dignn0flhalflem1  49106  affinecomb1  49193  rrxlinesc  49226  rrxlinec  49227  eenglngeehlnmlem1  49228  eenglngeehlnmlem2  49229  rrx2vlinest  49232  rrx2linest2  49235  2sphere  49240  line2  49243  itsclc0lem2  49248  itsclc0lem3  49249  itscnhlc0yqe  49250  itsclc0yqsollem2  49254  itsclc0yqsol  49255  itscnhlc0xyqsol  49256  itsclinecirc0  49264  itsclinecirc0b  49265  itsclinecirc0in  49266  itsclquadb  49267  2itscp  49272  itscnhlinecirc02plem1  49273  itscnhlinecirc02p  49276  inlinecirc02plem  49277  amgmwlem  50292