Theorem resubcld 11783

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  (class class class)co 7451  ℝcr 11238   − cmin 11580

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-po 5566  df-so 5567  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-pnf 11384  df-mnf 11385  df-ltxr 11387  df-sub 11582  df-neg 11583

This theorem is used by:  ltsubadd  11826  lesubadd  11828  lesub1  11850  lesub2  11851  ltsub1  11852  ltsub2  11853  lt2sub  11854  le2sub  11855  ltmul1a  12206  supaddc  12324  cru  12352  ge2halflem1  13277  qbtwnre  13369  lincmb01cmp  13666  iccf1o  13667  xov1plusxeqvd  13669  intfracq  14039  fldiv  14040  modlt  14060  modsubdir  14123  modsumfzodifsn  14127  serle  14240  expmulnbnd  14420  discr  14425  fzsdom2  14614  cshwidxmod  14996  sgnsub  15302  crre  15324  remullem  15338  01sqrexlem7  15458  absrdbnd  15553  fzomaxdiflem  15554  caubnd2  15569  amgm2  15581  icodiamlt  15649  bhmafibid1  15679  mulcn2  15807  reccn2  15808  rlimo1  15828  climle  15851  climsqz  15852  climsqz2  15853  rlimle  15859  isercolllem1  15876  climsup  15881  caucvgrlem  15884  caucvgrlem2  15886  iseraltlem2  15894  iseraltlem3  15895  iseralt  15896  fsumle  16010  cvgcmp  16027  cvgcmpce  16029  bpoly4  16269  eflt  16329  resinhcl  16368  tanhlt1  16372  sin01bnd  16397  sin01gt0  16402  moddvds  16477  bitscmp  16652  bitsinv1lem  16655  smueqlem  16704  modprm0  17027  pcbc  17122  4sqlem15  17181  blss2ps  24777  blss2  24778  blssps  24798  blss  24799  nm2dif  24999  nlmvscnlem2  25059  nrginvrcnlem  25065  iccntr  25196  icccmplem2  25198  metdstri  25226  cnllycmp  25332  evth  25335  lebnumii  25342  ipcnlem2  25620  cncmet  25698  rrxds  25769  rrxmval  25781  rrxmet  25784  rrxdstprj1  25785  rrxdsfi  25787  ehl1eudis  25796  ehl2eudis  25798  minveclem3b  25804  minveclem4  25808  ivthlem2  25828  ivthlem3  25829  ovollb2lem  25864  ovoliunlem1  25878  ovolscalem1  25889  ovolicc1  25892  ovolicc2lem4  25896  ovolicc2  25898  ovolicc  25899  voliunlem2  25927  ovolioo  25944  ioorcl2  25948  uniioovol  25955  uniioombllem2  25959  uniioombllem3a  25960  uniioombllem3  25961  uniioombllem4  25962  uniioombllem6  25964  opnmbllem  25977  volcn  25982  vitalilem2  25985  ismbf3d  26030  mbfaddlem  26036  i1fadd  26071  itg1addlem4  26075  mbfi1fseqlem6  26096  itg2seq  26118  itg2split  26125  itg2cnlem2  26138  itg2cn  26139  itgrevallem1  26170  dvcjbr  26324  dvferm1lem  26359  dvferm2lem  26361  cmvth  26366  mvth  26367  dvlip  26368  dvlip2  26370  c1liplem1  26371  dvgt0  26379  dvlt0  26380  dvge0  26381  dvle  26382  dvivthlem1  26383  lhop1lem  26388  lhop  26391  dvcnvrelem1  26392  dvcnvrelem2  26393  dvcnvre  26394  dvcvx  26395  dvfsumle  26396  dvfsumge  26397  dvfsumrlimf  26400  dvfsumlem2  26402  dvfsumlem3  26403  dvfsumlem4  26404  dvfsum2  26409  ftc1a  26412  ftc1lem4  26414  coe1mul3  26472  ply1divex  26510  plydivex  26673  aalioulem2  26717  aalioulem3  26718  aalioulem4  26719  aalioulem5  26720  aalioulem6  26721  aaliou3lem7  26733  taylthlem2  26758  mtest  26788  pilem2  26836  tangtx  26891  cosordlem  26915  efif1olem2  26928  logcnlem3  27029  logcnlem4  27030  isosctrlem2  27204  chordthmlem2  27218  chordthmlem4  27220  heron  27223  atanlogsublem  27300  atantan  27308  birthdaylem3  27338  logdifbnd  27378  emcllem1  27380  emcllem2  27381  emcllem5  27384  emcllem6  27385  harmonicbnd4  27395  fsumharmonic  27396  lgamgulmlem2  27414  lgamgulmlem3  27415  lgamucov  27422  relgamcl  27446  ftalem2  27458  ftalem5  27461  chpub  27604  logfaclbnd  27606  logfacbnd3  27607  logexprlim  27609  bposlem1  27668  bposlem9  27676  gausslemma2dlem1a  27749  lgseisenlem1  27759  lgsquadlem1  27764  2sqmod  27820  chtppilimlem1  27857  vmadivsum  27866  vmadivsumb  27867  rplogsumlem1  27868  rplogsumlem2  27869  rpvmasumlem  27871  dchrisumlem2  27874  dchrisum0re  27897  rplogsum  27911  mulogsumlem  27915  mulog2sumlem1  27918  vmalogdivsum2  27922  vmalogdivsum  27923  2vmadivsumlem  27924  log2sumbnd  27928  selbergb  27933  selberg2lem  27934  selberg2b  27936  chpdifbndlem1  27937  selberg3lem1  27941  selberg3lem2  27942  selberg3  27943  selberg4lem1  27944  selberg4  27945  pntrf  27947  pntrmax  27948  pntrsumo1  27949  selberg3r  27953  selberg4r  27954  selberg34r  27955  pntrlog2bndlem1  27961  pntrlog2bndlem2  27962  pntrlog2bndlem3  27963  pntrlog2bndlem4  27964  pntrlog2bndlem5  27965  pntrlog2bndlem6  27967  pntrlog2bnd  27968  pntpbnd1a  27969  pntpbnd2  27971  pntibndlem2  27975  pntlemg  27982  pntlemn  27984  pntlemj  27987  pntlemf  27989  pntlemo  27991  pntlem3  27993  pntleml  27995  ttgcontlem1  29519  eqeelen  29539  brbtwn2  29540  colinearalg  29545  axcgrid  29551  axsegconlem1  29552  axsegconlem3  29554  axsegconlem8  29559  axsegconlem9  29560  axsegconlem10  29561  ax5seglem3a  29565  ax5seg  29573  axpaschlem  29575  axcontlem8  29606  nbusgrvtxm1  30017  crctcshwlkn0lem3  30458  crctcshwlkn0lem5  30460  crctcsh  30470  clwlkclwwlklem2fv2  30644  clwlkclwwlklem2a4  30645  clwlkclwwlklem2a  30646  nvabs  31331  dipcj  31373  minvecolem4  31539  lt2addrd  33438  xlt2addrd  33447  fzsplit3  33481  bcm1n  33483  ply1degltel  34229  ply1degltlss  34231  iconstr  34509  constrresqrtcl  34520  cos9thpiminplylem1  34525  submateqlem1  34550  cnre2csqlem  34653  tpr2rico  34655  dya2ub  35013  dya2icoseg  35020  ballotlemfcc  35237  ballotlemfrcn0  35273  signslema  35302  ftc2re  35338  subfacval3  36162  dnibndlem8  37566  dnibndlem10  37568  dnibndlem11  37569  dnibndlem12  37570  dnicn  37573  knoppcnlem4  37577  unblimceq0  37588  unbdqndv2lem2  37591  knoppndvlem11  37603  knoppndvlem14  37606  knoppndvlem15  37607  knoppndvlem17  37609  knoppndvlem20  37612  irrdifflemf  38514  qdiff  38516  poimirlem29  38835  broucube  38840  opnmbllem0  38842  mblfinlem3  38845  mblfinlem4  38846  itg2addnclem  38857  itg2addnclem3  38859  itg2gt0cn  38861  ftc1cnnclem  38877  areacirclem1  38894  areacirclem2  38895  areacirclem4  38897  areacirclem5  38898  areacirc  38899  cntotbnd  38996  rrnmet  39029  rrndstprj1  39030  rrndstprj2  39031  lcmineqlem23  43367  intlewftc  43377  aks4d1p1p2  43386  aks4d1p1p4  43387  dvle2  43388  aks4d1p1  43392  primrootlekpowne0  43421  hashscontpow1  43437  aks6d1c2  43446  aks6d1c5lem2  43454  sticksstones10  43471  sticksstones12a  43473  sticksstones12  43474  aks6d1c6lem3  43488  bcled  43494  bcle2d  43495  unitscyglem2  43512  unitscyglem4  43514  readdrcl2d  43598  frlmvscadiccat  43839  fltnlta  43940  3cubeslem2  43961  3cubeslem4  43965  irrapxlem2  44096  irrapxlem3  44097  irrapxlem4  44098  irrapxlem5  44099  pellexlem2  44103  pellexlem6  44107  pell1qrgaplem  44146  rmspecsqrtnq  44179  rmspecfund  44182  rmspecpos  44189  jm2.24nn  44232  jm2.17c  44235  fzmaxdif  44254  acongeq  44256  modabsdifz  44259  jm3.1lem2  44291  areaquad  44479  sqrtcvallem2  44898  sqrtcvallem3  44899  sqrtcval  44902  imo72b2lem0  45426  cvgdvgrat  45558  hashnzfzclim  45567  binomcxplemdvbinom  45598  oddfl  46567  lefldiveq  46581  fperiodmul  46593  fzdifsuc2  46599  suprltrp  46613  supxrgere  46618  supxrgelem  46622  suplesup  46624  infleinflem2  46655  infleinf  46656  xrralrecnnge  46674  iccshift  46803  iooshift  46807  iooiinicc  46827  fmul01lt1lem2  46870  climinf  46891  sumnnodd  46915  ltmod  46921  lptre2pt  46923  climleltrp  46959  limsupgtlem  47060  liminflimsupclim  47090  fperdvper  47202  dvbdfbdioolem1  47211  dvbdfbdioolem2  47212  dvbdfbdioo  47213  ioodvbdlimc1lem1  47214  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  dvnmul  47226  iblspltprt  47256  itgspltprt  47262  itgiccshift  47263  itgperiod  47264  itgsbtaddcnst  47265  sublevolico  47267  stoweidlem1  47284  stoweidlem11  47294  stoweidlem12  47295  stoweidlem13  47296  stoweidlem14  47297  stoweidlem23  47306  stoweidlem24  47307  stoweidlem25  47308  stoweidlem26  47309  stoweidlem34  47317  stoweidlem40  47323  stoweidlem41  47324  stoweidlem42  47325  stoweidlem45  47328  stoweidlem60  47343  stoweidlem62  47345  wallispilem3  47350  wallispilem4  47351  wallispi  47353  wallispi2lem1  47354  stirlinglem5  47361  stirlinglem11  47367  stirlinglem12  47368  dirkercncflem1  47386  fourierdlem4  47394  fourierdlem6  47396  fourierdlem7  47397  fourierdlem9  47399  fourierdlem13  47403  fourierdlem14  47404  fourierdlem15  47405  fourierdlem19  47409  fourierdlem26  47416  fourierdlem35  47425  fourierdlem39  47429  fourierdlem40  47430  fourierdlem41  47431  fourierdlem42  47432  fourierdlem48  47437  fourierdlem49  47438  fourierdlem50  47439  fourierdlem51  47440  fourierdlem56  47445  fourierdlem57  47446  fourierdlem59  47448  fourierdlem60  47449  fourierdlem61  47450  fourierdlem63  47452  fourierdlem64  47453  fourierdlem65  47454  fourierdlem66  47455  fourierdlem68  47457  fourierdlem71  47460  fourierdlem72  47461  fourierdlem73  47462  fourierdlem74  47463  fourierdlem75  47464  fourierdlem76  47465  fourierdlem78  47467  fourierdlem79  47468  fourierdlem81  47470  fourierdlem82  47471  fourierdlem83  47472  fourierdlem84  47473  fourierdlem88  47477  fourierdlem89  47478  fourierdlem90  47479  fourierdlem91  47480  fourierdlem92  47481  fourierdlem93  47482  fourierdlem95  47484  fourierdlem97  47486  fourierdlem101  47490  fourierdlem103  47492  fourierdlem104  47493  fourierdlem107  47496  fourierdlem109  47498  fourierdlem111  47500  fouriersw  47514  elaa2lem  47516  etransclem23  47540  rrxtopnfi  47570  rrndistlt  47573  ioorrnopnlem  47587  ioorrnopnxrlem  47589  sge0gtfsumgt  47726  iundjiun  47743  volicorecl  47829  hoiprodcl  47830  hoiprodcl3  47863  volicore  47864  hoidmvcl  47865  hoidmv1lelem2  47875  hoidmv1lelem3  47876  hoidmv1le  47877  hoidmvlelem1  47878  hoidmvlelem2  47879  hoiqssbllem1  47905  hoiqssbllem2  47906  hoiqssbllem3  47907  hspmbllem1  47909  ovolval5lem1  47935  ovolval5lem2  47936  iunhoiioolem  47958  iccvonmbllem  47961  vonicclem1  47966  preimageiingt  48003  salpreimagtge  48008  smfaddlem1  48046  smflimlem4  48057  smfmullem1  48074  smfmullem2  48075  smfmullem3  48076  ltsubsubaddltsub  48644  2elfz2melfz  48661  2tceilhalfelfzo1  48679  flmrecm1  48686  requad01  48992  requad1  48993  requad2  48994  bgoldbtbndlem2  49177  bgoldbtbndlem3  49178  bgoldbtbndlem4  49179  bgoldbtbnd  49180  gpgedgvtx0  49432  gpgedgvtx1  49433  gpg5nbgrvtx03starlem2  49440  gpg5nbgrvtx13starlem2  49443  ply1mulgsumlem2  49830  nnpw2pmod  50026  dignn0flhalflem1  50058  affinecomb1  50145  rrxlinesc  50179  rrxlinec  50180  eenglngeehlnmlem1  50181  eenglngeehlnmlem2  50182  rrx2vlinest  50184  rrx2linest2  50187  2sphere  50192  itsclc0lem2  50200  itsclc0lem3  50201  itscnhlc0yqe  50202  itsclc0yqsollem2  50206  itsclc0yqsol  50207  itscnhlc0xyqsol  50208  itsclinecirc0  50216  itsclinecirc0b  50217  itsclinecirc0in  50218  itsclquadb  50219  2itscp  50224  itscnhlinecirc02plem1  50225  itscnhlinecirc02p  50228  inlinecirc02plem  50229  crosspcle1d  51383  crosspcle2d  51384  crosspcle3d  51385  crossp3d  51395  amgmwlem  51415