Theorem resubcld 11563

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7356  ℝcr 11023   − cmin 11362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-ltxr 11169  df-sub 11364  df-neg 11365

This theorem is referenced by:  ltsubadd  11605  lesubadd  11607  lesub1  11629  lesub2  11630  ltsub1  11631  ltsub2  11632  lt2sub  11633  le2sub  11634  ltmul1a  11988  supaddc  12107  cru  12135  ge2halflem1  13020  qbtwnre  13112  lincmb01cmp  13409  iccf1o  13410  xov1plusxeqvd  13412  intfracq  13777  fldiv  13778  modlt  13798  modsubdir  13861  modsumfzodifsn  13865  serle  13978  expmulnbnd  14156  discr  14161  fzsdom2  14349  cshwidxmod  14724  crre  15035  remullem  15049  01sqrexlem7  15169  absrdbnd  15263  fzomaxdiflem  15264  caubnd2  15279  amgm2  15291  icodiamlt  15359  bhmafibid1  15389  mulcn2  15517  reccn2  15518  rlimo1  15538  climle  15561  climsqz  15562  climsqz2  15563  rlimle  15569  isercolllem1  15586  climsup  15591  caucvgrlem  15594  caucvgrlem2  15596  iseraltlem2  15604  iseraltlem3  15605  iseralt  15606  fsumle  15720  cvgcmp  15737  cvgcmpce  15739  bpoly4  15980  eflt  16040  resinhcl  16079  tanhlt1  16083  sin01bnd  16108  sin01gt0  16113  moddvds  16188  bitscmp  16363  bitsinv1lem  16366  smueqlem  16415  modprm0  16731  pcbc  16826  4sqlem15  16885  blss2ps  24345  blss2  24346  blssps  24366  blss  24367  nm2dif  24567  nlmvscnlem2  24627  nrginvrcnlem  24633  iccntr  24764  icccmplem2  24766  metdstri  24794  cnllycmp  24909  evth  24912  lebnumii  24919  ipcnlem2  25198  cncmet  25276  rrxds  25347  rrxmval  25359  rrxmet  25362  rrxdstprj1  25363  rrxdsfi  25365  ehl1eudis  25374  ehl2eudis  25376  minveclem3b  25382  minveclem4  25386  ivthlem2  25407  ivthlem3  25408  ovollb2lem  25443  ovoliunlem1  25457  ovolscalem1  25468  ovolicc1  25471  ovolicc2lem4  25475  ovolicc2  25477  ovolicc  25478  voliunlem2  25506  ovolioo  25523  ioorcl2  25527  uniioovol  25534  uniioombllem2  25538  uniioombllem3a  25539  uniioombllem3  25540  uniioombllem4  25541  uniioombllem6  25543  opnmbllem  25556  volcn  25561  vitalilem2  25564  ismbf3d  25609  mbfaddlem  25615  i1fadd  25650  itg1addlem4  25654  mbfi1fseqlem6  25675  itg2seq  25697  itg2split  25704  itg2cnlem2  25717  itg2cn  25718  itgrevallem1  25750  dvcjbr  25907  dvferm1lem  25942  dvferm2lem  25944  cmvth  25949  cmvthOLD  25950  mvth  25951  dvlip  25952  dvlip2  25954  c1liplem1  25955  dvgt0  25963  dvlt0  25964  dvge0  25965  dvle  25966  dvivthlem1  25967  lhop1lem  25972  lhop  25975  dvcnvrelem1  25976  dvcnvrelem2  25977  dvcnvre  25978  dvcvx  25979  dvfsumle  25980  dvfsumleOLD  25981  dvfsumge  25982  dvfsumrlimf  25985  dvfsumlem2  25987  dvfsumlem2OLD  25988  dvfsumlem3  25989  dvfsumlem4  25990  dvfsum2  25995  ftc1a  25998  ftc1lem4  26000  coe1mul3  26058  ply1divex  26096  plydivex  26259  aalioulem2  26295  aalioulem3  26296  aalioulem4  26297  aalioulem5  26298  aalioulem6  26299  aaliou3lem7  26311  taylthlem2  26336  taylthlem2OLD  26337  mtest  26367  pilem2  26416  tangtx  26468  cosordlem  26493  efif1olem2  26506  logcnlem3  26607  logcnlem4  26608  isosctrlem2  26783  chordthmlem2  26797  chordthmlem4  26799  heron  26802  atanlogsublem  26879  atantan  26887  birthdaylem3  26917  logdifbnd  26958  emcllem1  26960  emcllem2  26961  emcllem5  26964  emcllem6  26965  harmonicbnd4  26975  fsumharmonic  26976  lgamgulmlem2  26994  lgamgulmlem3  26995  lgamucov  27002  relgamcl  27026  ftalem2  27038  ftalem5  27041  chpub  27185  logfaclbnd  27187  logfacbnd3  27188  logexprlim  27190  bposlem1  27249  bposlem9  27257  gausslemma2dlem1a  27330  lgseisenlem1  27340  lgsquadlem1  27345  2sqmod  27401  chtppilimlem1  27438  vmadivsum  27447  vmadivsumb  27448  rplogsumlem1  27449  rplogsumlem2  27450  rpvmasumlem  27452  dchrisumlem2  27455  dchrisum0re  27478  rplogsum  27492  mulogsumlem  27496  mulog2sumlem1  27499  vmalogdivsum2  27503  vmalogdivsum  27504  2vmadivsumlem  27505  log2sumbnd  27509  selbergb  27514  selberg2lem  27515  selberg2b  27517  chpdifbndlem1  27518  selberg3lem1  27522  selberg3lem2  27523  selberg3  27524  selberg4lem1  27525  selberg4  27526  pntrf  27528  pntrmax  27529  pntrsumo1  27530  selberg3r  27534  selberg4r  27535  selberg34r  27536  pntrlog2bndlem1  27542  pntrlog2bndlem2  27543  pntrlog2bndlem3  27544  pntrlog2bndlem4  27545  pntrlog2bndlem5  27546  pntrlog2bndlem6  27548  pntrlog2bnd  27549  pntpbnd1a  27550  pntpbnd2  27552  pntibndlem2  27556  pntlemg  27563  pntlemn  27565  pntlemj  27568  pntlemf  27570  pntlemo  27572  pntlem3  27574  pntleml  27576  ttgcontlem1  28906  eqeelen  28926  brbtwn2  28927  colinearalg  28932  axcgrid  28938  axsegconlem1  28939  axsegconlem3  28941  axsegconlem8  28946  axsegconlem9  28947  axsegconlem10  28948  ax5seglem3a  28952  ax5seg  28960  axpaschlem  28962  axcontlem8  28993  nbusgrvtxm1  29401  crctcshwlkn0lem3  29834  crctcshwlkn0lem5  29836  crctcsh  29846  clwlkclwwlklem2fv2  30020  clwlkclwwlklem2a4  30021  clwlkclwwlklem2a  30022  nvabs  30696  dipcj  30738  minvecolem4  30904  lt2addrd  32779  xlt2addrd  32788  fzsplit3  32822  bcm1n  32824  sgnsub  32867  ply1degltel  33624  ply1degltlss  33626  iconstr  33872  constrresqrtcl  33883  cos9thpiminplylem1  33888  submateqlem1  33913  cnre2csqlem  34016  tpr2rico  34018  dya2ub  34376  dya2icoseg  34383  ballotlemfcc  34600  ballotlemfrcn0  34636  signslema  34668  ftc2re  34704  subfacval3  35332  dnibndlem8  36628  dnibndlem10  36630  dnibndlem11  36631  dnibndlem12  36632  dnicn  36635  knoppcnlem4  36639  unblimceq0  36650  unbdqndv2lem2  36653  knoppndvlem11  36665  knoppndvlem14  36668  knoppndvlem15  36669  knoppndvlem17  36671  knoppndvlem20  36674  irrdifflemf  37469  poimirlem29  37789  broucube  37794  opnmbllem0  37796  mblfinlem3  37799  mblfinlem4  37800  itg2addnclem  37811  itg2addnclem3  37813  itg2gt0cn  37815  ftc1cnnclem  37831  areacirclem1  37848  areacirclem2  37849  areacirclem4  37851  areacirclem5  37852  areacirc  37853  cntotbnd  37936  rrnmet  37969  rrndstprj1  37970  rrndstprj2  37971  lcmineqlem23  42244  intlewftc  42254  aks4d1p1p2  42263  aks4d1p1p4  42264  dvle2  42265  aks4d1p1  42269  primrootlekpowne0  42298  hashscontpow1  42314  aks6d1c2  42323  aks6d1c5lem2  42331  sticksstones10  42348  sticksstones12a  42350  sticksstones12  42351  aks6d1c6lem3  42365  bcled  42371  bcle2d  42372  unitscyglem2  42389  unitscyglem4  42391  readdrcl2d  42470  frlmvscadiccat  42703  fltnlta  42848  3cubeslem2  42869  3cubeslem4  42873  irrapxlem2  43007  irrapxlem3  43008  irrapxlem4  43009  irrapxlem5  43010  pellexlem2  43014  pellexlem6  43018  pell1qrgaplem  43057  rmspecsqrtnq  43090  rmspecfund  43093  rmspecpos  43100  jm2.24nn  43143  jm2.17c  43146  fzmaxdif  43165  acongeq  43167  modabsdifz  43170  jm3.1lem2  43202  areaquad  43400  sqrtcvallem2  43820  sqrtcvallem3  43821  sqrtcval  43824  imo72b2lem0  44348  cvgdvgrat  44496  hashnzfzclim  44505  binomcxplemdvbinom  44536  oddfl  45468  lefldiveq  45482  fperiodmul  45494  fzdifsuc2  45500  suprltrp  45515  supxrgere  45520  supxrgelem  45524  suplesup  45526  infleinflem2  45557  infleinf  45558  xrralrecnnge  45576  iccshift  45706  iooshift  45710  iooiinicc  45730  fmul01lt1lem2  45773  climinf  45794  sumnnodd  45818  ltmod  45824  lptre2pt  45826  climleltrp  45862  limsupgtlem  45963  liminflimsupclim  45993  fperdvper  46105  dvbdfbdioolem1  46114  dvbdfbdioolem2  46115  dvbdfbdioo  46116  ioodvbdlimc1lem1  46117  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  dvnmul  46129  iblspltprt  46159  itgspltprt  46165  itgiccshift  46166  itgperiod  46167  itgsbtaddcnst  46168  sublevolico  46170  stoweidlem1  46187  stoweidlem11  46197  stoweidlem12  46198  stoweidlem13  46199  stoweidlem14  46200  stoweidlem23  46209  stoweidlem24  46210  stoweidlem25  46211  stoweidlem26  46212  stoweidlem34  46220  stoweidlem40  46226  stoweidlem41  46227  stoweidlem42  46228  stoweidlem45  46231  stoweidlem60  46246  stoweidlem62  46248  wallispilem3  46253  wallispilem4  46254  wallispi  46256  wallispi2lem1  46257  stirlinglem5  46264  stirlinglem11  46270  stirlinglem12  46271  dirkercncflem1  46289  fourierdlem4  46297  fourierdlem6  46299  fourierdlem7  46300  fourierdlem9  46302  fourierdlem13  46306  fourierdlem14  46307  fourierdlem15  46308  fourierdlem19  46312  fourierdlem26  46319  fourierdlem35  46328  fourierdlem39  46332  fourierdlem40  46333  fourierdlem41  46334  fourierdlem42  46335  fourierdlem48  46340  fourierdlem49  46341  fourierdlem50  46342  fourierdlem51  46343  fourierdlem56  46348  fourierdlem57  46349  fourierdlem59  46351  fourierdlem60  46352  fourierdlem61  46353  fourierdlem63  46355  fourierdlem64  46356  fourierdlem65  46357  fourierdlem66  46358  fourierdlem68  46360  fourierdlem71  46363  fourierdlem72  46364  fourierdlem73  46365  fourierdlem74  46366  fourierdlem75  46367  fourierdlem76  46368  fourierdlem78  46370  fourierdlem79  46371  fourierdlem81  46373  fourierdlem82  46374  fourierdlem83  46375  fourierdlem84  46376  fourierdlem88  46380  fourierdlem89  46381  fourierdlem90  46382  fourierdlem91  46383  fourierdlem92  46384  fourierdlem93  46385  fourierdlem95  46387  fourierdlem97  46389  fourierdlem101  46393  fourierdlem103  46395  fourierdlem104  46396  fourierdlem107  46399  fourierdlem109  46401  fourierdlem111  46403  fouriersw  46417  elaa2lem  46419  etransclem23  46443  rrxtopnfi  46473  rrndistlt  46476  ioorrnopnlem  46490  ioorrnopnxrlem  46492  sge0gtfsumgt  46629  iundjiun  46646  volicorecl  46732  hoiprodcl  46733  hoiprodcl3  46766  volicore  46767  hoidmvcl  46768  hoidmv1lelem2  46778  hoidmv1lelem3  46779  hoidmv1le  46780  hoidmvlelem1  46781  hoidmvlelem2  46782  hoiqssbllem1  46808  hoiqssbllem2  46809  hoiqssbllem3  46810  hspmbllem1  46812  ovolval5lem1  46838  ovolval5lem2  46839  iunhoiioolem  46861  iccvonmbllem  46864  vonicclem1  46869  preimageiingt  46906  salpreimagtge  46911  smfaddlem1  46949  smflimlem4  46960  smfmullem1  46977  smfmullem2  46978  smfmullem3  46979  ltsubsubaddltsub  47489  2elfz2melfz  47506  2tceilhalfelfzo1  47520  requad01  47809  requad1  47810  requad2  47811  bgoldbtbndlem2  47994  bgoldbtbndlem3  47995  bgoldbtbndlem4  47996  bgoldbtbnd  47997  gpgedgvtx0  48249  gpgedgvtx1  48250  gpg5nbgrvtx03starlem2  48257  gpg5nbgrvtx13starlem2  48260  ply1mulgsumlem2  48575  nnpw2pmod  48771  dignn0flhalflem1  48803  affinecomb1  48890  rrxlinesc  48923  rrxlinec  48924  eenglngeehlnmlem1  48925  eenglngeehlnmlem2  48926  rrx2vlinest  48929  rrx2linest2  48932  2sphere  48937  line2  48940  itsclc0lem2  48945  itsclc0lem3  48946  itscnhlc0yqe  48947  itsclc0yqsollem2  48951  itsclc0yqsol  48952  itscnhlc0xyqsol  48953  itsclinecirc0  48961  itsclinecirc0b  48962  itsclinecirc0in  48963  itsclquadb  48964  2itscp  48969  itscnhlinecirc02plem1  48970  itscnhlinecirc02p  48973  inlinecirc02plem  48974  amgmwlem  49989