Theorem resubcld 11582

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7369  ℝcr 11043   − cmin 11381

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 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120

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 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-ltxr 11189  df-sub 11383  df-neg 11384

This theorem is referenced by:  ltsubadd  11624  lesubadd  11626  lesub1  11648  lesub2  11649  ltsub1  11650  ltsub2  11651  lt2sub  11652  le2sub  11653  ltmul1a  12007  supaddc  12126  cru  12154  ge2halflem1  13044  qbtwnre  13135  lincmb01cmp  13432  iccf1o  13433  xov1plusxeqvd  13435  intfracq  13797  fldiv  13798  modlt  13818  modsubdir  13881  modsumfzodifsn  13885  serle  13998  expmulnbnd  14176  discr  14181  fzsdom2  14369  cshwidxmod  14744  crre  15056  remullem  15070  01sqrexlem7  15190  absrdbnd  15284  fzomaxdiflem  15285  caubnd2  15300  amgm2  15312  icodiamlt  15380  bhmafibid1  15410  mulcn2  15538  reccn2  15539  rlimo1  15559  climle  15582  climsqz  15583  climsqz2  15584  rlimle  15590  isercolllem1  15607  climsup  15612  caucvgrlem  15615  caucvgrlem2  15617  iseraltlem2  15625  iseraltlem3  15626  iseralt  15627  fsumle  15741  cvgcmp  15758  cvgcmpce  15760  bpoly4  16001  eflt  16061  resinhcl  16100  tanhlt1  16104  sin01bnd  16129  sin01gt0  16134  moddvds  16209  bitscmp  16384  bitsinv1lem  16387  smueqlem  16436  modprm0  16752  pcbc  16847  4sqlem15  16906  blss2ps  24324  blss2  24325  blssps  24345  blss  24346  nm2dif  24546  nlmvscnlem2  24606  nrginvrcnlem  24612  iccntr  24743  icccmplem2  24745  metdstri  24773  cnllycmp  24888  evth  24891  lebnumii  24898  ipcnlem2  25177  cncmet  25255  rrxds  25326  rrxmval  25338  rrxmet  25341  rrxdstprj1  25342  rrxdsfi  25344  ehl1eudis  25353  ehl2eudis  25355  minveclem3b  25361  minveclem4  25365  ivthlem2  25386  ivthlem3  25387  ovollb2lem  25422  ovoliunlem1  25436  ovolscalem1  25447  ovolicc1  25450  ovolicc2lem4  25454  ovolicc2  25456  ovolicc  25457  voliunlem2  25485  ovolioo  25502  ioorcl2  25506  uniioovol  25513  uniioombllem2  25517  uniioombllem3a  25518  uniioombllem3  25519  uniioombllem4  25520  uniioombllem6  25522  opnmbllem  25535  volcn  25540  vitalilem2  25543  ismbf3d  25588  mbfaddlem  25594  i1fadd  25629  itg1addlem4  25633  mbfi1fseqlem6  25654  itg2seq  25676  itg2split  25683  itg2cnlem2  25696  itg2cn  25697  itgrevallem1  25729  dvcjbr  25886  dvferm1lem  25921  dvferm2lem  25923  cmvth  25928  cmvthOLD  25929  mvth  25930  dvlip  25931  dvlip2  25933  c1liplem1  25934  dvgt0  25942  dvlt0  25943  dvge0  25944  dvle  25945  dvivthlem1  25946  lhop1lem  25951  lhop  25954  dvcnvrelem1  25955  dvcnvrelem2  25956  dvcnvre  25957  dvcvx  25958  dvfsumle  25959  dvfsumleOLD  25960  dvfsumge  25961  dvfsumrlimf  25964  dvfsumlem2  25966  dvfsumlem2OLD  25967  dvfsumlem3  25968  dvfsumlem4  25969  dvfsum2  25974  ftc1a  25977  ftc1lem4  25979  coe1mul3  26037  ply1divex  26075  plydivex  26238  aalioulem2  26274  aalioulem3  26275  aalioulem4  26276  aalioulem5  26277  aalioulem6  26278  aaliou3lem7  26290  taylthlem2  26315  taylthlem2OLD  26316  mtest  26346  pilem2  26395  tangtx  26447  cosordlem  26472  efif1olem2  26485  logcnlem3  26586  logcnlem4  26587  isosctrlem2  26762  chordthmlem2  26776  chordthmlem4  26778  heron  26781  atanlogsublem  26858  atantan  26866  birthdaylem3  26896  logdifbnd  26937  emcllem1  26939  emcllem2  26940  emcllem5  26943  emcllem6  26944  harmonicbnd4  26954  fsumharmonic  26955  lgamgulmlem2  26973  lgamgulmlem3  26974  lgamucov  26981  relgamcl  27005  ftalem2  27017  ftalem5  27020  chpub  27164  logfaclbnd  27166  logfacbnd3  27167  logexprlim  27169  bposlem1  27228  bposlem9  27236  gausslemma2dlem1a  27309  lgseisenlem1  27319  lgsquadlem1  27324  2sqmod  27380  chtppilimlem1  27417  vmadivsum  27426  vmadivsumb  27427  rplogsumlem1  27428  rplogsumlem2  27429  rpvmasumlem  27431  dchrisumlem2  27434  dchrisum0re  27457  rplogsum  27471  mulogsumlem  27475  mulog2sumlem1  27478  vmalogdivsum2  27482  vmalogdivsum  27483  2vmadivsumlem  27484  log2sumbnd  27488  selbergb  27493  selberg2lem  27494  selberg2b  27496  chpdifbndlem1  27497  selberg3lem1  27501  selberg3lem2  27502  selberg3  27503  selberg4lem1  27504  selberg4  27505  pntrf  27507  pntrmax  27508  pntrsumo1  27509  selberg3r  27513  selberg4r  27514  selberg34r  27515  pntrlog2bndlem1  27521  pntrlog2bndlem2  27522  pntrlog2bndlem3  27523  pntrlog2bndlem4  27524  pntrlog2bndlem5  27525  pntrlog2bndlem6  27527  pntrlog2bnd  27528  pntpbnd1a  27529  pntpbnd2  27531  pntibndlem2  27535  pntlemg  27542  pntlemn  27544  pntlemj  27547  pntlemf  27549  pntlemo  27551  pntlem3  27553  pntleml  27555  ttgcontlem1  28865  eqeelen  28884  brbtwn2  28885  colinearalg  28890  axcgrid  28896  axsegconlem1  28897  axsegconlem3  28899  axsegconlem8  28904  axsegconlem9  28905  axsegconlem10  28906  ax5seglem3a  28910  ax5seg  28918  axpaschlem  28920  axcontlem8  28951  nbusgrvtxm1  29359  crctcshwlkn0lem3  29792  crctcshwlkn0lem5  29794  crctcsh  29804  clwlkclwwlklem2fv2  29975  clwlkclwwlklem2a4  29976  clwlkclwwlklem2a  29977  nvabs  30651  dipcj  30693  minvecolem4  30859  lt2addrd  32724  xlt2addrd  32732  fzsplit3  32766  bcm1n  32768  sgnsub  32812  ply1degltel  33553  ply1degltlss  33555  iconstr  33749  constrresqrtcl  33760  cos9thpiminplylem1  33765  submateqlem1  33790  cnre2csqlem  33893  tpr2rico  33895  dya2ub  34254  dya2icoseg  34261  ballotlemfcc  34478  ballotlemfrcn0  34514  signslema  34546  ftc2re  34582  subfacval3  35169  dnibndlem8  36466  dnibndlem10  36468  dnibndlem11  36469  dnibndlem12  36470  dnicn  36473  knoppcnlem4  36477  unblimceq0  36488  unbdqndv2lem2  36491  knoppndvlem11  36503  knoppndvlem14  36506  knoppndvlem15  36507  knoppndvlem17  36509  knoppndvlem20  36512  irrdifflemf  37306  poimirlem29  37636  broucube  37641  opnmbllem0  37643  mblfinlem3  37646  mblfinlem4  37647  itg2addnclem  37658  itg2addnclem3  37660  itg2gt0cn  37662  ftc1cnnclem  37678  areacirclem1  37695  areacirclem2  37696  areacirclem4  37698  areacirclem5  37699  areacirc  37700  cntotbnd  37783  rrnmet  37816  rrndstprj1  37817  rrndstprj2  37818  lcmineqlem23  42032  intlewftc  42042  aks4d1p1p2  42051  aks4d1p1p4  42052  dvle2  42053  aks4d1p1  42057  primrootlekpowne0  42086  hashscontpow1  42102  aks6d1c2  42111  aks6d1c5lem2  42119  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  aks6d1c6lem3  42153  bcled  42159  bcle2d  42160  unitscyglem2  42177  unitscyglem4  42179  readdrcl2d  42254  frlmvscadiccat  42487  fltnlta  42644  3cubeslem2  42666  3cubeslem4  42670  irrapxlem2  42804  irrapxlem3  42805  irrapxlem4  42806  irrapxlem5  42807  pellexlem2  42811  pellexlem6  42815  pell1qrgaplem  42854  rmspecsqrtnq  42887  rmspecfund  42890  rmspecpos  42898  jm2.24nn  42941  jm2.17c  42944  fzmaxdif  42963  acongeq  42965  modabsdifz  42968  jm3.1lem2  43000  areaquad  43198  sqrtcvallem2  43619  sqrtcvallem3  43620  sqrtcval  43623  imo72b2lem0  44147  cvgdvgrat  44295  hashnzfzclim  44304  binomcxplemdvbinom  44335  oddfl  45269  lefldiveq  45283  fperiodmul  45295  fzdifsuc2  45301  suprltrp  45317  supxrgere  45322  supxrgelem  45326  suplesup  45328  infleinflem2  45360  infleinf  45361  xrralrecnnge  45379  iccshift  45509  iooshift  45513  iooiinicc  45533  fmul01lt1lem2  45576  climinf  45597  sumnnodd  45621  ltmod  45629  lptre2pt  45631  climleltrp  45667  limsupgtlem  45768  liminflimsupclim  45798  fperdvper  45910  dvbdfbdioolem1  45919  dvbdfbdioolem2  45920  dvbdfbdioo  45921  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnmul  45934  iblspltprt  45964  itgspltprt  45970  itgiccshift  45971  itgperiod  45972  itgsbtaddcnst  45973  sublevolico  45975  stoweidlem1  45992  stoweidlem11  46002  stoweidlem12  46003  stoweidlem13  46004  stoweidlem14  46005  stoweidlem23  46014  stoweidlem24  46015  stoweidlem25  46016  stoweidlem26  46017  stoweidlem34  46025  stoweidlem40  46031  stoweidlem41  46032  stoweidlem42  46033  stoweidlem45  46036  stoweidlem60  46051  stoweidlem62  46053  wallispilem3  46058  wallispilem4  46059  wallispi  46061  wallispi2lem1  46062  stirlinglem5  46069  stirlinglem11  46075  stirlinglem12  46076  dirkercncflem1  46094  fourierdlem4  46102  fourierdlem6  46104  fourierdlem7  46105  fourierdlem9  46107  fourierdlem13  46111  fourierdlem14  46112  fourierdlem15  46113  fourierdlem19  46117  fourierdlem26  46124  fourierdlem35  46133  fourierdlem39  46137  fourierdlem40  46138  fourierdlem41  46139  fourierdlem42  46140  fourierdlem48  46145  fourierdlem49  46146  fourierdlem50  46147  fourierdlem51  46148  fourierdlem56  46153  fourierdlem57  46154  fourierdlem59  46156  fourierdlem60  46157  fourierdlem61  46158  fourierdlem63  46160  fourierdlem64  46161  fourierdlem65  46162  fourierdlem66  46163  fourierdlem68  46165  fourierdlem71  46168  fourierdlem72  46169  fourierdlem73  46170  fourierdlem74  46171  fourierdlem75  46172  fourierdlem76  46173  fourierdlem78  46175  fourierdlem79  46176  fourierdlem81  46178  fourierdlem82  46179  fourierdlem83  46180  fourierdlem84  46181  fourierdlem88  46185  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fourierdlem92  46189  fourierdlem93  46190  fourierdlem95  46192  fourierdlem97  46194  fourierdlem101  46198  fourierdlem103  46200  fourierdlem104  46201  fourierdlem107  46204  fourierdlem109  46206  fourierdlem111  46208  fouriersw  46222  elaa2lem  46224  etransclem23  46248  rrxtopnfi  46278  rrndistlt  46281  ioorrnopnlem  46295  ioorrnopnxrlem  46297  sge0gtfsumgt  46434  iundjiun  46451  volicorecl  46537  hoiprodcl  46538  hoiprodcl3  46571  volicore  46572  hoidmvcl  46573  hoidmv1lelem2  46583  hoidmv1lelem3  46584  hoidmv1le  46585  hoidmvlelem1  46586  hoidmvlelem2  46587  hoiqssbllem1  46613  hoiqssbllem2  46614  hoiqssbllem3  46615  hspmbllem1  46617  ovolval5lem1  46643  ovolval5lem2  46644  iunhoiioolem  46666  iccvonmbllem  46669  vonicclem1  46674  preimageiingt  46711  salpreimagtge  46716  smfaddlem1  46754  smflimlem4  46765  smfmullem1  46782  smfmullem2  46783  smfmullem3  46784  ltsubsubaddltsub  47295  2elfz2melfz  47312  2tceilhalfelfzo1  47326  requad01  47615  requad1  47616  requad2  47617  bgoldbtbndlem2  47800  bgoldbtbndlem3  47801  bgoldbtbndlem4  47802  bgoldbtbnd  47803  gpgedgvtx0  48045  gpgedgvtx1  48046  gpg5nbgrvtx03starlem2  48053  gpg5nbgrvtx13starlem2  48056  ply1mulgsumlem2  48369  nnpw2pmod  48565  dignn0flhalflem1  48597  affinecomb1  48684  rrxlinesc  48717  rrxlinec  48718  eenglngeehlnmlem1  48719  eenglngeehlnmlem2  48720  rrx2vlinest  48723  rrx2linest2  48726  2sphere  48731  line2  48734  itsclc0lem2  48739  itsclc0lem3  48740  itscnhlc0yqe  48741  itsclc0yqsollem2  48745  itsclc0yqsol  48746  itscnhlc0xyqsol  48747  itsclinecirc0  48755  itsclinecirc0b  48756  itsclinecirc0in  48757  itsclquadb  48758  2itscp  48763  itscnhlinecirc02plem1  48764  itscnhlinecirc02p  48767  inlinecirc02plem  48768  amgmwlem  49784