Theorem resubcld 11659

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7419  ℝcr 11116   − cmin 11458

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-i2m1 11185  ax-1ne0 11186  ax-1rid 11187  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190  ax-pre-lttri 11191  ax-pre-lttrn 11192  ax-pre-ltadd 11193

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 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11262  df-mnf 11263  df-ltxr 11265  df-sub 11460  df-neg 11461

This theorem is used by:  ltsubadd  11701  lesubadd  11703  lesub1  11725  lesub2  11726  ltsub1  11727  ltsub2  11728  lt2sub  11729  le2sub  11730  ltmul1a  12081  supaddc  12199  cru  12227  ge2halflem1  13151  qbtwnre  13243  lincmb01cmp  13540  iccf1o  13541  xov1plusxeqvd  13543  intfracq  13912  fldiv  13913  modlt  13933  modsubdir  13996  modsumfzodifsn  14000  serle  14113  expmulnbnd  14291  discr  14296  fzsdom2  14485  cshwidxmod  14866  sgnsub  15169  crre  15191  remullem  15205  01sqrexlem7  15325  absrdbnd  15419  fzomaxdiflem  15420  caubnd2  15435  amgm2  15447  icodiamlt  15515  bhmafibid1  15545  mulcn2  15673  reccn2  15674  rlimo1  15694  climle  15717  climsqz  15718  climsqz2  15719  rlimle  15725  isercolllem1  15742  climsup  15747  caucvgrlem  15750  caucvgrlem2  15752  iseraltlem2  15760  iseraltlem3  15761  iseralt  15762  fsumle  15876  cvgcmp  15893  cvgcmpce  15895  bpoly4  16137  eflt  16197  resinhcl  16236  tanhlt1  16240  sin01bnd  16265  sin01gt0  16270  moddvds  16345  bitscmp  16520  bitsinv1lem  16523  smueqlem  16572  modprm0  16889  pcbc  16984  4sqlem15  17043  blss2ps  24613  blss2  24614  blssps  24634  blss  24635  nm2dif  24835  nlmvscnlem2  24895  nrginvrcnlem  24901  iccntr  25032  icccmplem2  25034  metdstri  25062  cnllycmp  25168  evth  25171  lebnumii  25178  ipcnlem2  25456  cncmet  25534  rrxds  25605  rrxmval  25617  rrxmet  25620  rrxdstprj1  25621  rrxdsfi  25623  ehl1eudis  25632  ehl2eudis  25634  minveclem3b  25640  minveclem4  25644  ivthlem2  25664  ivthlem3  25665  ovollb2lem  25700  ovoliunlem1  25714  ovolscalem1  25725  ovolicc1  25728  ovolicc2lem4  25732  ovolicc2  25734  ovolicc  25735  voliunlem2  25763  ovolioo  25780  ioorcl2  25784  uniioovol  25791  uniioombllem2  25795  uniioombllem3a  25796  uniioombllem3  25797  uniioombllem4  25798  uniioombllem6  25800  opnmbllem  25813  volcn  25818  vitalilem2  25821  ismbf3d  25866  mbfaddlem  25872  i1fadd  25907  itg1addlem4  25911  mbfi1fseqlem6  25932  itg2seq  25954  itg2split  25961  itg2cnlem2  25974  itg2cn  25975  itgrevallem1  26007  dvcjbr  26161  dvferm1lem  26196  dvferm2lem  26198  cmvth  26203  mvth  26204  dvlip  26205  dvlip2  26207  c1liplem1  26208  dvgt0  26216  dvlt0  26217  dvge0  26218  dvle  26219  dvivthlem1  26220  lhop1lem  26225  lhop  26228  dvcnvrelem1  26229  dvcnvrelem2  26230  dvcnvre  26231  dvcvx  26232  dvfsumle  26233  dvfsumge  26234  dvfsumrlimf  26237  dvfsumlem2  26239  dvfsumlem3  26240  dvfsumlem4  26241  dvfsum2  26246  ftc1a  26249  ftc1lem4  26251  coe1mul3  26309  ply1divex  26347  plydivex  26511  aalioulem2  26549  aalioulem3  26550  aalioulem4  26551  aalioulem5  26552  aalioulem6  26553  aaliou3lem7  26565  taylthlem2  26590  mtest  26620  pilem2  26668  tangtx  26723  cosordlem  26748  efif1olem2  26761  logcnlem3  26862  logcnlem4  26863  isosctrlem2  27037  chordthmlem2  27051  chordthmlem4  27053  heron  27056  atanlogsublem  27133  atantan  27141  birthdaylem3  27171  logdifbnd  27211  emcllem1  27213  emcllem2  27214  emcllem5  27217  emcllem6  27218  harmonicbnd4  27228  fsumharmonic  27229  lgamgulmlem2  27247  lgamgulmlem3  27248  lgamucov  27255  relgamcl  27279  ftalem2  27291  ftalem5  27294  chpub  27437  logfaclbnd  27439  logfacbnd3  27440  logexprlim  27442  bposlem1  27501  bposlem9  27509  gausslemma2dlem1a  27582  lgseisenlem1  27592  lgsquadlem1  27597  2sqmod  27653  chtppilimlem1  27690  vmadivsum  27699  vmadivsumb  27700  rplogsumlem1  27701  rplogsumlem2  27702  rpvmasumlem  27704  dchrisumlem2  27707  dchrisum0re  27730  rplogsum  27744  mulogsumlem  27748  mulog2sumlem1  27751  vmalogdivsum2  27755  vmalogdivsum  27756  2vmadivsumlem  27757  log2sumbnd  27761  selbergb  27766  selberg2lem  27767  selberg2b  27769  chpdifbndlem1  27770  selberg3lem1  27774  selberg3lem2  27775  selberg3  27776  selberg4lem1  27777  selberg4  27778  pntrf  27780  pntrmax  27781  pntrsumo1  27782  selberg3r  27786  selberg4r  27787  selberg34r  27788  pntrlog2bndlem1  27794  pntrlog2bndlem2  27795  pntrlog2bndlem3  27796  pntrlog2bndlem4  27797  pntrlog2bndlem5  27798  pntrlog2bndlem6  27800  pntrlog2bnd  27801  pntpbnd1a  27802  pntpbnd2  27804  pntibndlem2  27808  pntlemg  27815  pntlemn  27817  pntlemj  27820  pntlemf  27822  pntlemo  27824  pntlem3  27826  pntleml  27828  ttgcontlem1  29291  eqeelen  29311  brbtwn2  29312  colinearalg  29317  axcgrid  29323  axsegconlem1  29324  axsegconlem3  29326  axsegconlem8  29331  axsegconlem9  29332  axsegconlem10  29333  ax5seglem3a  29337  ax5seg  29345  axpaschlem  29347  axcontlem8  29378  nbusgrvtxm1  29789  crctcshwlkn0lem3  30230  crctcshwlkn0lem5  30232  crctcsh  30242  clwlkclwwlklem2fv2  30416  clwlkclwwlklem2a4  30417  clwlkclwwlklem2a  30418  nvabs  31097  dipcj  31139  minvecolem4  31305  lt2addrd  33167  xlt2addrd  33176  fzsplit3  33210  bcm1n  33212  ply1degltel  33950  ply1degltlss  33952  iconstr  34222  constrresqrtcl  34233  cos9thpiminplylem1  34238  submateqlem1  34263  cnre2csqlem  34366  tpr2rico  34368  dya2ub  34727  dya2icoseg  34734  ballotlemfcc  34951  ballotlemfrcn0  34987  signslema  35016  ftc2re  35052  subfacval3  35720  dnibndlem8  37133  dnibndlem10  37135  dnibndlem11  37136  dnibndlem12  37137  dnicn  37140  knoppcnlem4  37144  unblimceq0  37155  unbdqndv2lem2  37158  knoppndvlem11  37170  knoppndvlem14  37173  knoppndvlem15  37174  knoppndvlem17  37176  knoppndvlem20  37179  irrdifflemf  38028  qdiff  38030  poimirlem29  38359  broucube  38364  opnmbllem0  38366  mblfinlem3  38369  mblfinlem4  38370  itg2addnclem  38381  itg2addnclem3  38383  itg2gt0cn  38385  ftc1cnnclem  38401  areacirclem1  38418  areacirclem2  38419  areacirclem4  38421  areacirclem5  38422  areacirc  38423  cntotbnd  38507  rrnmet  38540  rrndstprj1  38541  rrndstprj2  38542  lcmineqlem23  42878  intlewftc  42888  aks4d1p1p2  42897  aks4d1p1p4  42898  dvle2  42899  aks4d1p1  42903  primrootlekpowne0  42932  hashscontpow1  42948  aks6d1c2  42957  aks6d1c5lem2  42965  sticksstones10  42982  sticksstones12a  42984  sticksstones12  42985  aks6d1c6lem3  42999  bcled  43005  bcle2d  43006  unitscyglem2  43023  unitscyglem4  43025  readdrcl2d  43094  frlmvscadiccat  43340  fltnlta  43455  3cubeslem2  43476  3cubeslem4  43480  irrapxlem2  43610  irrapxlem3  43611  irrapxlem4  43612  irrapxlem5  43613  pellexlem2  43617  pellexlem6  43621  pell1qrgaplem  43660  rmspecsqrtnq  43693  rmspecfund  43696  rmspecpos  43703  jm2.24nn  43746  jm2.17c  43749  fzmaxdif  43768  acongeq  43770  modabsdifz  43773  jm3.1lem2  43805  areaquad  44003  sqrtcvallem2  44423  sqrtcvallem3  44424  sqrtcval  44427  imo72b2lem0  44951  cvgdvgrat  45083  hashnzfzclim  45092  binomcxplemdvbinom  45123  oddfl  46057  lefldiveq  46071  fperiodmul  46083  fzdifsuc2  46089  suprltrp  46104  supxrgere  46109  supxrgelem  46113  suplesup  46115  infleinflem2  46146  infleinf  46147  xrralrecnnge  46165  iccshift  46294  iooshift  46298  iooiinicc  46318  fmul01lt1lem2  46361  climinf  46382  sumnnodd  46406  ltmod  46412  lptre2pt  46414  climleltrp  46450  limsupgtlem  46551  liminflimsupclim  46581  fperdvper  46693  dvbdfbdioolem1  46702  dvbdfbdioolem2  46703  dvbdfbdioo  46704  ioodvbdlimc1lem1  46705  ioodvbdlimc1lem2  46706  ioodvbdlimc2lem  46708  dvnmul  46717  iblspltprt  46747  itgspltprt  46753  itgiccshift  46754  itgperiod  46755  itgsbtaddcnst  46756  sublevolico  46758  stoweidlem1  46775  stoweidlem11  46785  stoweidlem12  46786  stoweidlem13  46787  stoweidlem14  46788  stoweidlem23  46797  stoweidlem24  46798  stoweidlem25  46799  stoweidlem26  46800  stoweidlem34  46808  stoweidlem40  46814  stoweidlem41  46815  stoweidlem42  46816  stoweidlem45  46819  stoweidlem60  46834  stoweidlem62  46836  wallispilem3  46841  wallispilem4  46842  wallispi  46844  wallispi2lem1  46845  stirlinglem5  46852  stirlinglem11  46858  stirlinglem12  46859  dirkercncflem1  46877  fourierdlem4  46885  fourierdlem6  46887  fourierdlem7  46888  fourierdlem9  46890  fourierdlem13  46894  fourierdlem14  46895  fourierdlem15  46896  fourierdlem19  46900  fourierdlem26  46907  fourierdlem35  46916  fourierdlem39  46920  fourierdlem40  46921  fourierdlem41  46922  fourierdlem42  46923  fourierdlem48  46928  fourierdlem49  46929  fourierdlem50  46930  fourierdlem51  46931  fourierdlem56  46936  fourierdlem57  46937  fourierdlem59  46939  fourierdlem60  46940  fourierdlem61  46941  fourierdlem63  46943  fourierdlem64  46944  fourierdlem65  46945  fourierdlem66  46946  fourierdlem68  46948  fourierdlem71  46951  fourierdlem72  46952  fourierdlem73  46953  fourierdlem74  46954  fourierdlem75  46955  fourierdlem76  46956  fourierdlem78  46958  fourierdlem79  46959  fourierdlem81  46961  fourierdlem82  46962  fourierdlem83  46963  fourierdlem84  46964  fourierdlem88  46968  fourierdlem89  46969  fourierdlem90  46970  fourierdlem91  46971  fourierdlem92  46972  fourierdlem93  46973  fourierdlem95  46975  fourierdlem97  46977  fourierdlem101  46981  fourierdlem103  46983  fourierdlem104  46984  fourierdlem107  46987  fourierdlem109  46989  fourierdlem111  46991  fouriersw  47005  elaa2lem  47007  etransclem23  47031  rrxtopnfi  47061  rrndistlt  47064  ioorrnopnlem  47078  ioorrnopnxrlem  47080  sge0gtfsumgt  47217  iundjiun  47234  volicorecl  47320  hoiprodcl  47321  hoiprodcl3  47354  volicore  47355  hoidmvcl  47356  hoidmv1lelem2  47366  hoidmv1lelem3  47367  hoidmv1le  47368  hoidmvlelem1  47369  hoidmvlelem2  47370  hoiqssbllem1  47396  hoiqssbllem2  47397  hoiqssbllem3  47398  hspmbllem1  47400  ovolval5lem1  47426  ovolval5lem2  47427  iunhoiioolem  47449  iccvonmbllem  47452  vonicclem1  47457  preimageiingt  47494  salpreimagtge  47499  smfaddlem1  47537  smflimlem4  47548  smfmullem1  47565  smfmullem2  47566  smfmullem3  47567  ltsubsubaddltsub  48098  2elfz2melfz  48115  2tceilhalfelfzo1  48133  flmrecm1  48140  requad01  48446  requad1  48447  requad2  48448  bgoldbtbndlem2  48631  bgoldbtbndlem3  48632  bgoldbtbndlem4  48633  bgoldbtbnd  48634  gpgedgvtx0  48886  gpgedgvtx1  48887  gpg5nbgrvtx03starlem2  48894  gpg5nbgrvtx13starlem2  48897  ply1mulgsumlem2  49226  nnpw2pmod  49422  dignn0flhalflem1  49454  affinecomb1  49541  rrxlinesc  49574  rrxlinec  49575  eenglngeehlnmlem1  49576  eenglngeehlnmlem2  49577  rrx2vlinest  49580  rrx2linest2  49583  2sphere  49588  line2  49591  itsclc0lem2  49596  itsclc0lem3  49597  itscnhlc0yqe  49598  itsclc0yqsollem2  49602  itsclc0yqsol  49603  itscnhlc0xyqsol  49604  itsclinecirc0  49612  itsclinecirc0b  49613  itsclinecirc0in  49614  itsclquadb  49615  2itscp  49620  itscnhlinecirc02plem1  49621  itscnhlinecirc02p  49624  inlinecirc02plem  49625  crosspcle1d  50696  crosspcle2d  50697  crosspcle3d  50698  crossp3d  50708  amgmwlem  50709