Theorem resubcld 11068

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7156  ℝcr 10536   − cmin 10870

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-po 5474  df-so 5475  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-ltxr 10680  df-sub 10872  df-neg 10873

This theorem is referenced by:  ltsubadd  11110  lesubadd  11112  lesub1  11134  lesub2  11135  ltsub1  11136  ltsub2  11137  lt2sub  11138  le2sub  11139  ltmul1a  11489  supaddc  11608  cru  11630  qbtwnre  12593  lincmb01cmp  12882  iccf1o  12883  xov1plusxeqvd  12885  intfracq  13228  fldiv  13229  modlt  13249  modsubdir  13309  modsumfzodifsn  13313  serle  13426  expmulnbnd  13597  discr  13602  fzsdom2  13790  cshwidxmod  14165  crre  14473  remullem  14487  sqrlem7  14608  absrdbnd  14701  fzomaxdiflem  14702  caubnd2  14717  amgm2  14729  icodiamlt  14795  bhmafibid1  14825  mulcn2  14952  reccn2  14953  rlimo1  14973  climle  14996  climsqz  14997  climsqz2  14998  rlimle  15004  isercolllem1  15021  climsup  15026  caucvgrlem  15029  caucvgrlem2  15031  iseraltlem2  15039  iseraltlem3  15040  iseralt  15041  fsumle  15154  cvgcmp  15171  cvgcmpce  15173  bpoly4  15413  eflt  15470  resinhcl  15509  tanhlt1  15513  sin01bnd  15538  sin01gt0  15543  moddvds  15618  bitscmp  15787  bitsinv1lem  15790  smueqlem  15839  modprm0  16142  pcbc  16236  4sqlem15  16295  blss2ps  23013  blss2  23014  blssps  23034  blss  23035  nm2dif  23234  nlmvscnlem2  23294  nrginvrcnlem  23300  iccntr  23429  icccmplem2  23431  metdstri  23459  cnllycmp  23560  evth  23563  lebnumii  23570  ipcnlem2  23847  cncmet  23925  rrxds  23996  rrxmval  24008  rrxmet  24011  rrxdstprj1  24012  rrxdsfi  24014  ehl1eudis  24023  ehl2eudis  24025  minveclem3b  24031  minveclem4  24035  ivthlem2  24053  ivthlem3  24054  ovollb2lem  24089  ovoliunlem1  24103  ovolscalem1  24114  ovolicc1  24117  ovolicc2lem4  24121  ovolicc2  24123  ovolicc  24124  voliunlem2  24152  ovolioo  24169  ioorcl2  24173  uniioovol  24180  uniioombllem2  24184  uniioombllem3a  24185  uniioombllem3  24186  uniioombllem4  24187  uniioombllem6  24189  opnmbllem  24202  volcn  24207  vitalilem2  24210  ismbf3d  24255  mbfaddlem  24261  i1fadd  24296  itg1addlem4  24300  mbfi1fseqlem6  24321  itg2seq  24343  itg2split  24350  itg2cnlem2  24363  itg2cn  24364  itgrevallem1  24395  dvcjbr  24546  dvferm1lem  24581  dvferm2lem  24583  cmvth  24588  mvth  24589  dvlip  24590  dvlip2  24592  c1liplem1  24593  dvgt0  24601  dvlt0  24602  dvge0  24603  dvle  24604  dvivthlem1  24605  lhop1lem  24610  lhop  24613  dvcnvrelem1  24614  dvcnvrelem2  24615  dvcnvre  24616  dvcvx  24617  dvfsumle  24618  dvfsumge  24619  dvfsumrlimf  24622  dvfsumlem2  24624  dvfsumlem3  24625  dvfsumlem4  24626  dvfsum2  24631  ftc1a  24634  ftc1lem4  24636  coe1mul3  24693  ply1divex  24730  plydivex  24886  aalioulem2  24922  aalioulem3  24923  aalioulem4  24924  aalioulem5  24925  aalioulem6  24926  aaliou3lem7  24938  taylthlem2  24962  mtest  24992  pilem2  25040  tangtx  25091  cosordlem  25115  efif1olem2  25127  logcnlem3  25227  logcnlem4  25228  isosctrlem2  25397  chordthmlem2  25411  chordthmlem4  25413  heron  25416  atanlogsublem  25493  atantan  25501  birthdaylem3  25531  logdifbnd  25571  emcllem1  25573  emcllem2  25574  emcllem5  25577  emcllem6  25578  harmonicbnd4  25588  fsumharmonic  25589  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamucov  25615  relgamcl  25639  ftalem2  25651  ftalem5  25654  chpub  25796  logfaclbnd  25798  logfacbnd3  25799  logexprlim  25801  bposlem1  25860  bposlem9  25868  gausslemma2dlem1a  25941  lgseisenlem1  25951  lgsquadlem1  25956  2sqmod  26012  chtppilimlem1  26049  vmadivsum  26058  vmadivsumb  26059  rplogsumlem1  26060  rplogsumlem2  26061  rpvmasumlem  26063  dchrisumlem2  26066  dchrisum0re  26089  rplogsum  26103  mulogsumlem  26107  mulog2sumlem1  26110  vmalogdivsum2  26114  vmalogdivsum  26115  2vmadivsumlem  26116  log2sumbnd  26120  selbergb  26125  selberg2lem  26126  selberg2b  26128  chpdifbndlem1  26129  selberg3lem1  26133  selberg3lem2  26134  selberg3  26135  selberg4lem1  26136  selberg4  26137  pntrf  26139  pntrmax  26140  pntrsumo1  26141  selberg3r  26145  selberg4r  26146  selberg34r  26147  pntrlog2bndlem1  26153  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntrlog2bnd  26160  pntpbnd1a  26161  pntpbnd2  26163  pntibndlem2  26167  pntlemg  26174  pntlemn  26176  pntlemj  26179  pntlemf  26181  pntlemo  26183  pntlem3  26185  pntleml  26187  ttgcontlem1  26671  eqeelen  26690  brbtwn2  26691  colinearalg  26696  axcgrid  26702  axsegconlem1  26703  axsegconlem3  26705  axsegconlem8  26710  axsegconlem9  26711  axsegconlem10  26712  ax5seglem3a  26716  ax5seg  26724  axpaschlem  26726  axcontlem8  26757  nbusgrvtxm1  27161  crctcshwlkn0lem3  27590  crctcshwlkn0lem5  27592  crctcsh  27602  clwlkclwwlklem2fv2  27774  clwlkclwwlklem2a4  27775  clwlkclwwlklem2a  27776  nvabs  28449  dipcj  28491  minvecolem4  28657  lt2addrd  30475  xlt2addrd  30482  fzsplit3  30517  bcm1n  30518  submateqlem1  31072  cnre2csqlem  31153  tpr2rico  31155  dya2ub  31528  dya2icoseg  31535  ballotlemfcc  31751  ballotlemfrcn0  31787  sgnsub  31802  signslema  31832  ftc2re  31869  subfacval3  32436  dnibndlem8  33824  dnibndlem10  33826  dnibndlem11  33827  dnibndlem12  33828  dnicn  33831  knoppcnlem4  33835  unblimceq0  33846  unbdqndv2lem2  33849  knoppndvlem11  33861  knoppndvlem14  33864  knoppndvlem15  33865  knoppndvlem17  33867  knoppndvlem20  33870  poimirlem29  34936  broucube  34941  opnmbllem0  34943  mblfinlem3  34946  mblfinlem4  34947  itg2addnclem  34958  itg2addnclem3  34960  itg2gt0cn  34962  ftc1cnnclem  34980  areacirclem1  34997  areacirclem2  34998  areacirclem4  35000  areacirclem5  35001  areacirc  35002  cntotbnd  35089  rrnmet  35122  rrndstprj1  35123  rrndstprj2  35124  frlmvscadiccat  39194  fltnlta  39324  3cubeslem2  39331  3cubeslem4  39335  irrapxlem2  39469  irrapxlem3  39470  irrapxlem4  39471  irrapxlem5  39472  pellexlem2  39476  pellexlem6  39480  pell1qrgaplem  39519  rmspecsqrtnq  39552  rmspecfund  39555  rmspecpos  39562  jm2.24nn  39605  jm2.17c  39608  fzmaxdif  39627  acongeq  39629  modabsdifz  39632  jm3.1lem2  39664  areaquad  39872  imo72b2lem0  40565  cvgdvgrat  40694  hashnzfzclim  40703  binomcxplemdvbinom  40734  oddfl  41592  lefldiveq  41608  fperiodmul  41620  fzdifsuc2  41626  suprltrp  41645  supxrgere  41650  supxrgelem  41654  suplesup  41656  infleinflem2  41688  infleinf  41689  xrralrecnnge  41711  iccshift  41843  iooshift  41847  iooiinicc  41867  fmul01lt1lem2  41915  climinf  41936  sumnnodd  41960  ltmod  41968  lptre2pt  41970  climleltrp  42006  limsupgtlem  42107  liminflimsupclim  42137  fperdvper  42252  dvbdfbdioolem1  42262  dvbdfbdioolem2  42263  dvbdfbdioo  42264  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvnmul  42277  iblspltprt  42307  itgspltprt  42313  itgiccshift  42314  itgperiod  42315  itgsbtaddcnst  42316  sublevolico  42318  stoweidlem1  42335  stoweidlem11  42345  stoweidlem12  42346  stoweidlem13  42347  stoweidlem14  42348  stoweidlem23  42357  stoweidlem24  42358  stoweidlem25  42359  stoweidlem26  42360  stoweidlem34  42368  stoweidlem40  42374  stoweidlem41  42375  stoweidlem42  42376  stoweidlem45  42379  stoweidlem60  42394  stoweidlem62  42396  wallispilem3  42401  wallispilem4  42402  wallispi  42404  wallispi2lem1  42405  stirlinglem5  42412  stirlinglem11  42418  stirlinglem12  42419  dirkercncflem1  42437  fourierdlem4  42445  fourierdlem6  42447  fourierdlem7  42448  fourierdlem9  42450  fourierdlem13  42454  fourierdlem14  42455  fourierdlem15  42456  fourierdlem19  42460  fourierdlem26  42467  fourierdlem35  42476  fourierdlem39  42480  fourierdlem40  42481  fourierdlem41  42482  fourierdlem42  42483  fourierdlem48  42488  fourierdlem49  42489  fourierdlem50  42490  fourierdlem51  42491  fourierdlem56  42496  fourierdlem57  42497  fourierdlem59  42499  fourierdlem60  42500  fourierdlem61  42501  fourierdlem63  42503  fourierdlem64  42504  fourierdlem65  42505  fourierdlem66  42506  fourierdlem68  42508  fourierdlem71  42511  fourierdlem72  42512  fourierdlem73  42513  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem78  42518  fourierdlem79  42519  fourierdlem81  42521  fourierdlem82  42522  fourierdlem83  42523  fourierdlem84  42524  fourierdlem88  42528  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fourierdlem92  42532  fourierdlem93  42533  fourierdlem95  42535  fourierdlem97  42537  fourierdlem101  42541  fourierdlem103  42543  fourierdlem104  42544  fourierdlem107  42547  fourierdlem109  42549  fourierdlem111  42551  fouriersw  42565  elaa2lem  42567  etransclem23  42591  rrxtopnfi  42621  rrndistlt  42624  ioorrnopnlem  42638  ioorrnopnxrlem  42640  sge0gtfsumgt  42774  iundjiun  42791  volicorecl  42877  hoiprodcl  42878  hoiprodcl3  42911  volicore  42912  hoidmvcl  42913  hoidmv1lelem2  42923  hoidmv1lelem3  42924  hoidmv1le  42925  hoidmvlelem1  42926  hoidmvlelem2  42927  hoiqssbllem1  42953  hoiqssbllem2  42954  hoiqssbllem3  42955  hspmbllem1  42957  ovolval5lem1  42983  ovolval5lem2  42984  iunhoiioolem  43006  iccvonmbllem  43009  vonicclem1  43014  preimageiingt  43047  salpreimagtge  43051  smfaddlem1  43088  smflimlem4  43099  smfmullem1  43115  smfmullem2  43116  smfmullem3  43117  ltsubsubaddltsub  43550  2elfz2melfz  43567  requad01  43835  requad1  43836  requad2  43837  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  bgoldbtbndlem4  44022  bgoldbtbnd  44023  ply1mulgsumlem2  44490  difmodm1lt  44631  nnpw2pmod  44692  dignn0flhalflem1  44724  affinecomb1  44738  rrxlinesc  44771  rrxlinec  44772  eenglngeehlnmlem1  44773  eenglngeehlnmlem2  44774  rrx2vlinest  44777  rrx2linest2  44780  2sphere  44785  line2  44788  itsclc0lem2  44793  itsclc0lem3  44794  itscnhlc0yqe  44795  itsclc0yqsollem2  44799  itsclc0yqsol  44800  itscnhlc0xyqsol  44801  itsclinecirc0  44809  itsclinecirc0b  44810  itsclinecirc0in  44811  itsclquadb  44812  2itscp  44817  itscnhlinecirc02plem1  44818  itscnhlinecirc02p  44821  inlinecirc02plem  44822  amgmwlem  44952