Theorem resubcld 11592

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

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7362  ℝcr 11059   − cmin 11394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-resscn 11117  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-mulcom 11124  ax-addass 11125  ax-mulass 11126  ax-distr 11127  ax-i2m1 11128  ax-1ne0 11129  ax-1rid 11130  ax-rnegex 11131  ax-rrecex 11132  ax-cnre 11133  ax-pre-lttri 11134  ax-pre-lttrn 11135  ax-pre-ltadd 11136

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-po 5550  df-so 5551  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11200  df-mnf 11201  df-ltxr 11203  df-sub 11396  df-neg 11397

This theorem is referenced by:  ltsubadd  11634  lesubadd  11636  lesub1  11658  lesub2  11659  ltsub1  11660  ltsub2  11661  lt2sub  11662  le2sub  11663  ltmul1a  12013  supaddc  12131  cru  12154  qbtwnre  13128  lincmb01cmp  13422  iccf1o  13423  xov1plusxeqvd  13425  intfracq  13774  fldiv  13775  modlt  13795  modsubdir  13855  modsumfzodifsn  13859  serle  13973  expmulnbnd  14148  discr  14153  fzsdom2  14338  cshwidxmod  14703  crre  15011  remullem  15025  01sqrexlem7  15145  absrdbnd  15238  fzomaxdiflem  15239  caubnd2  15254  amgm2  15266  icodiamlt  15332  bhmafibid1  15362  mulcn2  15490  reccn2  15491  rlimo1  15511  climle  15534  climsqz  15535  climsqz2  15536  rlimle  15544  isercolllem1  15561  climsup  15566  caucvgrlem  15569  caucvgrlem2  15571  iseraltlem2  15579  iseraltlem3  15580  iseralt  15581  fsumle  15695  cvgcmp  15712  cvgcmpce  15714  bpoly4  15953  eflt  16010  resinhcl  16049  tanhlt1  16053  sin01bnd  16078  sin01gt0  16083  moddvds  16158  bitscmp  16329  bitsinv1lem  16332  smueqlem  16381  modprm0  16688  pcbc  16783  4sqlem15  16842  blss2ps  23793  blss2  23794  blssps  23814  blss  23815  nm2dif  24018  nlmvscnlem2  24086  nrginvrcnlem  24092  iccntr  24221  icccmplem2  24223  metdstri  24251  cnllycmp  24356  evth  24359  lebnumii  24366  ipcnlem2  24645  cncmet  24723  rrxds  24794  rrxmval  24806  rrxmet  24809  rrxdstprj1  24810  rrxdsfi  24812  ehl1eudis  24821  ehl2eudis  24823  minveclem3b  24829  minveclem4  24833  ivthlem2  24853  ivthlem3  24854  ovollb2lem  24889  ovoliunlem1  24903  ovolscalem1  24914  ovolicc1  24917  ovolicc2lem4  24921  ovolicc2  24923  ovolicc  24924  voliunlem2  24952  ovolioo  24969  ioorcl2  24973  uniioovol  24980  uniioombllem2  24984  uniioombllem3a  24985  uniioombllem3  24986  uniioombllem4  24987  uniioombllem6  24989  opnmbllem  25002  volcn  25007  vitalilem2  25010  ismbf3d  25055  mbfaddlem  25061  i1fadd  25096  itg1addlem4  25100  itg1addlem4OLD  25101  mbfi1fseqlem6  25122  itg2seq  25144  itg2split  25151  itg2cnlem2  25164  itg2cn  25165  itgrevallem1  25196  dvcjbr  25350  dvferm1lem  25385  dvferm2lem  25387  cmvth  25392  mvth  25393  dvlip  25394  dvlip2  25396  c1liplem1  25397  dvgt0  25405  dvlt0  25406  dvge0  25407  dvle  25408  dvivthlem1  25409  lhop1lem  25414  lhop  25417  dvcnvrelem1  25418  dvcnvrelem2  25419  dvcnvre  25420  dvcvx  25421  dvfsumle  25422  dvfsumge  25423  dvfsumrlimf  25426  dvfsumlem2  25428  dvfsumlem3  25429  dvfsumlem4  25430  dvfsum2  25435  ftc1a  25438  ftc1lem4  25440  coe1mul3  25501  ply1divex  25538  plydivex  25694  aalioulem2  25730  aalioulem3  25731  aalioulem4  25732  aalioulem5  25733  aalioulem6  25734  aaliou3lem7  25746  taylthlem2  25770  mtest  25800  pilem2  25848  tangtx  25899  cosordlem  25923  efif1olem2  25936  logcnlem3  26036  logcnlem4  26037  isosctrlem2  26206  chordthmlem2  26220  chordthmlem4  26222  heron  26225  atanlogsublem  26302  atantan  26310  birthdaylem3  26340  logdifbnd  26380  emcllem1  26382  emcllem2  26383  emcllem5  26386  emcllem6  26387  harmonicbnd4  26397  fsumharmonic  26398  lgamgulmlem2  26416  lgamgulmlem3  26417  lgamucov  26424  relgamcl  26448  ftalem2  26460  ftalem5  26463  chpub  26605  logfaclbnd  26607  logfacbnd3  26608  logexprlim  26610  bposlem1  26669  bposlem9  26677  gausslemma2dlem1a  26750  lgseisenlem1  26760  lgsquadlem1  26765  2sqmod  26821  chtppilimlem1  26858  vmadivsum  26867  vmadivsumb  26868  rplogsumlem1  26869  rplogsumlem2  26870  rpvmasumlem  26872  dchrisumlem2  26875  dchrisum0re  26898  rplogsum  26912  mulogsumlem  26916  mulog2sumlem1  26919  vmalogdivsum2  26923  vmalogdivsum  26924  2vmadivsumlem  26925  log2sumbnd  26929  selbergb  26934  selberg2lem  26935  selberg2b  26937  chpdifbndlem1  26938  selberg3lem1  26942  selberg3lem2  26943  selberg3  26944  selberg4lem1  26945  selberg4  26946  pntrf  26948  pntrmax  26949  pntrsumo1  26950  selberg3r  26954  selberg4r  26955  selberg34r  26956  pntrlog2bndlem1  26962  pntrlog2bndlem2  26963  pntrlog2bndlem3  26964  pntrlog2bndlem4  26965  pntrlog2bndlem5  26966  pntrlog2bndlem6  26968  pntrlog2bnd  26969  pntpbnd1a  26970  pntpbnd2  26972  pntibndlem2  26976  pntlemg  26983  pntlemn  26985  pntlemj  26988  pntlemf  26990  pntlemo  26992  pntlem3  26994  pntleml  26996  ttgcontlem1  27896  eqeelen  27916  brbtwn2  27917  colinearalg  27922  axcgrid  27928  axsegconlem1  27929  axsegconlem3  27931  axsegconlem8  27936  axsegconlem9  27937  axsegconlem10  27938  ax5seglem3a  27942  ax5seg  27950  axpaschlem  27952  axcontlem8  27983  nbusgrvtxm1  28390  crctcshwlkn0lem3  28820  crctcshwlkn0lem5  28822  crctcsh  28832  clwlkclwwlklem2fv2  29003  clwlkclwwlklem2a4  29004  clwlkclwwlklem2a  29005  nvabs  29677  dipcj  29719  minvecolem4  29885  lt2addrd  31724  xlt2addrd  31731  fzsplit3  31765  bcm1n  31766  ply1degltel  32365  ply1degltlss  32366  submateqlem1  32477  cnre2csqlem  32580  tpr2rico  32582  dya2ub  32959  dya2icoseg  32966  ballotlemfcc  33182  ballotlemfrcn0  33218  sgnsub  33233  signslema  33263  ftc2re  33300  subfacval3  33870  dnibndlem8  35024  dnibndlem10  35026  dnibndlem11  35027  dnibndlem12  35028  dnicn  35031  knoppcnlem4  35035  unblimceq0  35046  unbdqndv2lem2  35049  knoppndvlem11  35061  knoppndvlem14  35064  knoppndvlem15  35065  knoppndvlem17  35067  knoppndvlem20  35070  irrdifflemf  35869  poimirlem29  36180  broucube  36185  opnmbllem0  36187  mblfinlem3  36190  mblfinlem4  36191  itg2addnclem  36202  itg2addnclem3  36204  itg2gt0cn  36206  ftc1cnnclem  36222  areacirclem1  36239  areacirclem2  36240  areacirclem4  36242  areacirclem5  36243  areacirc  36244  cntotbnd  36328  rrnmet  36361  rrndstprj1  36362  rrndstprj2  36363  lcmineqlem23  40581  intlewftc  40591  aks4d1p1p2  40600  aks4d1p1p4  40601  dvle2  40602  aks4d1p1  40606  sticksstones10  40636  sticksstones12a  40638  sticksstones12  40639  metakunt1  40650  metakunt7  40656  metakunt16  40665  metakunt18  40667  metakunt28  40677  metakunt29  40678  metakunt30  40679  frlmvscadiccat  40749  fltnlta  41059  3cubeslem2  41066  3cubeslem4  41070  irrapxlem2  41204  irrapxlem3  41205  irrapxlem4  41206  irrapxlem5  41207  pellexlem2  41211  pellexlem6  41215  pell1qrgaplem  41254  rmspecsqrtnq  41287  rmspecfund  41290  rmspecpos  41298  jm2.24nn  41341  jm2.17c  41344  fzmaxdif  41363  acongeq  41365  modabsdifz  41368  jm3.1lem2  41400  areaquad  41608  sqrtcvallem2  42031  sqrtcvallem3  42032  sqrtcval  42035  imo72b2lem0  42560  cvgdvgrat  42715  hashnzfzclim  42724  binomcxplemdvbinom  42755  oddfl  43632  lefldiveq  43647  fperiodmul  43659  fzdifsuc2  43665  suprltrp  43683  supxrgere  43688  supxrgelem  43692  suplesup  43694  infleinflem2  43726  infleinf  43727  xrralrecnnge  43745  iccshift  43876  iooshift  43880  iooiinicc  43900  fmul01lt1lem2  43946  climinf  43967  sumnnodd  43991  ltmod  43999  lptre2pt  44001  climleltrp  44037  limsupgtlem  44138  liminflimsupclim  44168  fperdvper  44280  dvbdfbdioolem1  44289  dvbdfbdioolem2  44290  dvbdfbdioo  44291  ioodvbdlimc1lem1  44292  ioodvbdlimc1lem2  44293  ioodvbdlimc2lem  44295  dvnmul  44304  iblspltprt  44334  itgspltprt  44340  itgiccshift  44341  itgperiod  44342  itgsbtaddcnst  44343  sublevolico  44345  stoweidlem1  44362  stoweidlem11  44372  stoweidlem12  44373  stoweidlem13  44374  stoweidlem14  44375  stoweidlem23  44384  stoweidlem24  44385  stoweidlem25  44386  stoweidlem26  44387  stoweidlem34  44395  stoweidlem40  44401  stoweidlem41  44402  stoweidlem42  44403  stoweidlem45  44406  stoweidlem60  44421  stoweidlem62  44423  wallispilem3  44428  wallispilem4  44429  wallispi  44431  wallispi2lem1  44432  stirlinglem5  44439  stirlinglem11  44445  stirlinglem12  44446  dirkercncflem1  44464  fourierdlem4  44472  fourierdlem6  44474  fourierdlem7  44475  fourierdlem9  44477  fourierdlem13  44481  fourierdlem14  44482  fourierdlem15  44483  fourierdlem19  44487  fourierdlem26  44494  fourierdlem35  44503  fourierdlem39  44507  fourierdlem40  44508  fourierdlem41  44509  fourierdlem42  44510  fourierdlem48  44515  fourierdlem49  44516  fourierdlem50  44517  fourierdlem51  44518  fourierdlem56  44523  fourierdlem57  44524  fourierdlem59  44526  fourierdlem60  44527  fourierdlem61  44528  fourierdlem63  44530  fourierdlem64  44531  fourierdlem65  44532  fourierdlem66  44533  fourierdlem68  44535  fourierdlem71  44538  fourierdlem72  44539  fourierdlem73  44540  fourierdlem74  44541  fourierdlem75  44542  fourierdlem76  44543  fourierdlem78  44545  fourierdlem79  44546  fourierdlem81  44548  fourierdlem82  44549  fourierdlem83  44550  fourierdlem84  44551  fourierdlem88  44555  fourierdlem89  44556  fourierdlem90  44557  fourierdlem91  44558  fourierdlem92  44559  fourierdlem93  44560  fourierdlem95  44562  fourierdlem97  44564  fourierdlem101  44568  fourierdlem103  44570  fourierdlem104  44571  fourierdlem107  44574  fourierdlem109  44576  fourierdlem111  44578  fouriersw  44592  elaa2lem  44594  etransclem23  44618  rrxtopnfi  44648  rrndistlt  44651  ioorrnopnlem  44665  ioorrnopnxrlem  44667  sge0gtfsumgt  44804  iundjiun  44821  volicorecl  44907  hoiprodcl  44908  hoiprodcl3  44941  volicore  44942  hoidmvcl  44943  hoidmv1lelem2  44953  hoidmv1lelem3  44954  hoidmv1le  44955  hoidmvlelem1  44956  hoidmvlelem2  44957  hoiqssbllem1  44983  hoiqssbllem2  44984  hoiqssbllem3  44985  hspmbllem1  44987  ovolval5lem1  45013  ovolval5lem2  45014  iunhoiioolem  45036  iccvonmbllem  45039  vonicclem1  45044  preimageiingt  45081  salpreimagtge  45086  smfaddlem1  45124  smflimlem4  45135  smfmullem1  45152  smfmullem2  45153  smfmullem3  45154  ltsubsubaddltsub  45653  2elfz2melfz  45670  requad01  45933  requad1  45934  requad2  45935  bgoldbtbndlem2  46118  bgoldbtbndlem3  46119  bgoldbtbndlem4  46120  bgoldbtbnd  46121  ply1mulgsumlem2  46588  difmodm1lt  46728  nnpw2pmod  46789  dignn0flhalflem1  46821  affinecomb1  46908  rrxlinesc  46941  rrxlinec  46942  eenglngeehlnmlem1  46943  eenglngeehlnmlem2  46944  rrx2vlinest  46947  rrx2linest2  46950  2sphere  46955  line2  46958  itsclc0lem2  46963  itsclc0lem3  46964  itscnhlc0yqe  46965  itsclc0yqsollem2  46969  itsclc0yqsol  46970  itscnhlc0xyqsol  46971  itsclinecirc0  46979  itsclinecirc0b  46980  itsclinecirc0in  46981  itsclquadb  46982  2itscp  46987  itscnhlinecirc02plem1  46988  itscnhlinecirc02p  46991  inlinecirc02plem  46992  amgmwlem  47369