Theorem resubcld 11642

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

Syntax hints:   → wi 4   ∈ wcel 2149  (class class class)co 7411  ℝcr 11099   − cmin 11441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-i2m1 11168  ax-1ne0 11169  ax-1rid 11170  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174  ax-pre-lttrn 11175  ax-pre-ltadd 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-po 5570  df-so 5571  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8694  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11245  df-mnf 11246  df-ltxr 11248  df-sub 11443  df-neg 11444

This theorem is referenced by:  ltsubadd  11684  lesubadd  11686  lesub1  11708  lesub2  11709  ltsub1  11710  ltsub2  11711  lt2sub  11712  le2sub  11713  ltmul1a  12064  supaddc  12182  cru  12210  ge2halflem1  13133  qbtwnre  13225  lincmb01cmp  13522  iccf1o  13523  xov1plusxeqvd  13525  intfracq  13892  fldiv  13893  modlt  13913  modsubdir  13976  modsumfzodifsn  13980  serle  14093  expmulnbnd  14271  discr  14276  fzsdom2  14465  cshwidxmod  14840  sgnsub  15143  crre  15165  remullem  15179  01sqrexlem7  15299  absrdbnd  15393  fzomaxdiflem  15394  caubnd2  15409  amgm2  15421  icodiamlt  15489  bhmafibid1  15519  mulcn2  15647  reccn2  15648  rlimo1  15668  climle  15691  climsqz  15692  climsqz2  15693  rlimle  15699  isercolllem1  15716  climsup  15721  caucvgrlem  15724  caucvgrlem2  15726  iseraltlem2  15734  iseraltlem3  15735  iseralt  15736  fsumle  15851  cvgcmp  15868  cvgcmpce  15870  bpoly4  16113  eflt  16173  resinhcl  16212  tanhlt1  16216  sin01bnd  16241  sin01gt0  16246  moddvds  16321  bitscmp  16496  bitsinv1lem  16499  smueqlem  16548  modprm0  16865  pcbc  16960  4sqlem15  17019  blss2ps  24529  blss2  24530  blssps  24550  blss  24551  nm2dif  24751  nlmvscnlem2  24811  nrginvrcnlem  24817  iccntr  24948  icccmplem2  24950  metdstri  24978  cnllycmp  25084  evth  25087  lebnumii  25094  ipcnlem2  25372  cncmet  25450  rrxds  25521  rrxmval  25533  rrxmet  25536  rrxdstprj1  25537  rrxdsfi  25539  ehl1eudis  25548  ehl2eudis  25550  minveclem3b  25556  minveclem4  25560  ivthlem2  25580  ivthlem3  25581  ovollb2lem  25616  ovoliunlem1  25630  ovolscalem1  25641  ovolicc1  25644  ovolicc2lem4  25648  ovolicc2  25650  ovolicc  25651  voliunlem2  25679  ovolioo  25696  ioorcl2  25700  uniioovol  25707  uniioombllem2  25711  uniioombllem3a  25712  uniioombllem3  25713  uniioombllem4  25714  uniioombllem6  25716  opnmbllem  25729  volcn  25734  vitalilem2  25737  ismbf3d  25782  mbfaddlem  25788  i1fadd  25823  itg1addlem4  25827  mbfi1fseqlem6  25848  itg2seq  25870  itg2split  25877  itg2cnlem2  25890  itg2cn  25891  itgrevallem1  25923  dvcjbr  26077  dvferm1lem  26112  dvferm2lem  26114  cmvth  26119  mvth  26120  dvlip  26121  dvlip2  26123  c1liplem1  26124  dvgt0  26132  dvlt0  26133  dvge0  26134  dvle  26135  dvivthlem1  26136  lhop1lem  26141  lhop  26144  dvcnvrelem1  26145  dvcnvrelem2  26146  dvcnvre  26147  dvcvx  26148  dvfsumle  26149  dvfsumge  26150  dvfsumrlimf  26153  dvfsumlem2  26155  dvfsumlem3  26156  dvfsumlem4  26157  dvfsum2  26162  ftc1a  26165  ftc1lem4  26167  coe1mul3  26225  ply1divex  26263  plydivex  26427  aalioulem2  26463  aalioulem3  26464  aalioulem4  26465  aalioulem5  26466  aalioulem6  26467  aaliou3lem7  26479  taylthlem2  26503  mtest  26533  pilem2  26581  tangtx  26636  cosordlem  26661  efif1olem2  26674  logcnlem3  26775  logcnlem4  26776  isosctrlem2  26950  chordthmlem2  26964  chordthmlem4  26966  heron  26969  atanlogsublem  27046  atantan  27054  birthdaylem3  27084  logdifbnd  27124  emcllem1  27126  emcllem2  27127  emcllem5  27130  emcllem6  27131  harmonicbnd4  27141  fsumharmonic  27142  lgamgulmlem2  27160  lgamgulmlem3  27161  lgamucov  27168  relgamcl  27192  ftalem2  27204  ftalem5  27207  chpub  27350  logfaclbnd  27352  logfacbnd3  27353  logexprlim  27355  bposlem1  27414  bposlem9  27422  gausslemma2dlem1a  27495  lgseisenlem1  27505  lgsquadlem1  27510  2sqmod  27566  chtppilimlem1  27603  vmadivsum  27612  vmadivsumb  27613  rplogsumlem1  27614  rplogsumlem2  27615  rpvmasumlem  27617  dchrisumlem2  27620  dchrisum0re  27643  rplogsum  27657  mulogsumlem  27661  mulog2sumlem1  27664  vmalogdivsum2  27668  vmalogdivsum  27669  2vmadivsumlem  27670  log2sumbnd  27674  selbergb  27679  selberg2lem  27680  selberg2b  27682  chpdifbndlem1  27683  selberg3lem1  27687  selberg3lem2  27688  selberg3  27689  selberg4lem1  27690  selberg4  27691  pntrf  27693  pntrmax  27694  pntrsumo1  27695  selberg3r  27699  selberg4r  27700  selberg34r  27701  pntrlog2bndlem1  27707  pntrlog2bndlem2  27708  pntrlog2bndlem3  27709  pntrlog2bndlem4  27710  pntrlog2bndlem5  27711  pntrlog2bndlem6  27713  pntrlog2bnd  27714  pntpbnd1a  27715  pntpbnd2  27717  pntibndlem2  27721  pntlemg  27728  pntlemn  27730  pntlemj  27733  pntlemf  27735  pntlemo  27737  pntlem3  27739  pntleml  27741  ttgcontlem1  29175  eqeelen  29195  brbtwn2  29196  colinearalg  29201  axcgrid  29207  axsegconlem1  29208  axsegconlem3  29210  axsegconlem8  29215  axsegconlem9  29216  axsegconlem10  29217  ax5seglem3a  29221  ax5seg  29229  axpaschlem  29231  axcontlem8  29262  nbusgrvtxm1  29670  crctcshwlkn0lem3  30102  crctcshwlkn0lem5  30104  crctcsh  30114  clwlkclwwlklem2fv2  30288  clwlkclwwlklem2a4  30289  clwlkclwwlklem2a  30290  nvabs  30965  dipcj  31007  minvecolem4  31173  lt2addrd  33036  xlt2addrd  33045  fzsplit3  33079  bcm1n  33081  ply1degltel  33829  ply1degltlss  33831  iconstr  34101  constrresqrtcl  34112  cos9thpiminplylem1  34117  submateqlem1  34142  cnre2csqlem  34245  tpr2rico  34247  dya2ub  34605  dya2icoseg  34612  ballotlemfcc  34829  ballotlemfrcn0  34865  signslema  34894  ftc2re  34930  subfacval3  35580  dnibndlem8  36963  dnibndlem10  36965  dnibndlem11  36966  dnibndlem12  36967  dnicn  36970  knoppcnlem4  36974  unblimceq0  36985  unbdqndv2lem2  36988  knoppndvlem11  37000  knoppndvlem14  37003  knoppndvlem15  37004  knoppndvlem17  37006  knoppndvlem20  37009  irrdifflemf  37857  qdiff  37859  poimirlem29  38188  broucube  38193  opnmbllem0  38195  mblfinlem3  38198  mblfinlem4  38199  itg2addnclem  38210  itg2addnclem3  38212  itg2gt0cn  38214  ftc1cnnclem  38230  areacirclem1  38247  areacirclem2  38248  areacirclem4  38250  areacirclem5  38251  areacirc  38252  cntotbnd  38335  rrnmet  38368  rrndstprj1  38369  rrndstprj2  38370  lcmineqlem23  42708  intlewftc  42718  aks4d1p1p2  42727  aks4d1p1p4  42728  dvle2  42729  aks4d1p1  42733  primrootlekpowne0  42762  hashscontpow1  42778  aks6d1c2  42787  aks6d1c5lem2  42795  sticksstones10  42812  sticksstones12a  42814  sticksstones12  42815  aks6d1c6lem3  42829  bcled  42835  bcle2d  42836  unitscyglem2  42853  unitscyglem4  42855  readdrcl2d  42924  frlmvscadiccat  43170  fltnlta  43287  3cubeslem2  43308  3cubeslem4  43312  irrapxlem2  43442  irrapxlem3  43443  irrapxlem4  43444  irrapxlem5  43445  pellexlem2  43449  pellexlem6  43453  pell1qrgaplem  43492  rmspecsqrtnq  43525  rmspecfund  43528  rmspecpos  43535  jm2.24nn  43578  jm2.17c  43581  fzmaxdif  43600  acongeq  43602  modabsdifz  43605  jm3.1lem2  43637  areaquad  43835  sqrtcvallem2  44255  sqrtcvallem3  44256  sqrtcval  44259  imo72b2lem0  44783  cvgdvgrat  44915  hashnzfzclim  44924  binomcxplemdvbinom  44955  oddfl  45889  lefldiveq  45903  fperiodmul  45915  fzdifsuc2  45921  suprltrp  45936  supxrgere  45941  supxrgelem  45945  suplesup  45947  infleinflem2  45978  infleinf  45979  xrralrecnnge  45997  iccshift  46126  iooshift  46130  iooiinicc  46150  fmul01lt1lem2  46193  climinf  46214  sumnnodd  46238  ltmod  46244  lptre2pt  46246  climleltrp  46282  limsupgtlem  46383  liminflimsupclim  46413  fperdvper  46525  dvbdfbdioolem1  46534  dvbdfbdioolem2  46535  dvbdfbdioo  46536  ioodvbdlimc1lem1  46537  ioodvbdlimc1lem2  46538  ioodvbdlimc2lem  46540  dvnmul  46549  iblspltprt  46579  itgspltprt  46585  itgiccshift  46586  itgperiod  46587  itgsbtaddcnst  46588  sublevolico  46590  stoweidlem1  46607  stoweidlem11  46617  stoweidlem12  46618  stoweidlem13  46619  stoweidlem14  46620  stoweidlem23  46629  stoweidlem24  46630  stoweidlem25  46631  stoweidlem26  46632  stoweidlem34  46640  stoweidlem40  46646  stoweidlem41  46647  stoweidlem42  46648  stoweidlem45  46651  stoweidlem60  46666  stoweidlem62  46668  wallispilem3  46673  wallispilem4  46674  wallispi  46676  wallispi2lem1  46677  stirlinglem5  46684  stirlinglem11  46690  stirlinglem12  46691  dirkercncflem1  46709  fourierdlem4  46717  fourierdlem6  46719  fourierdlem7  46720  fourierdlem9  46722  fourierdlem13  46726  fourierdlem14  46727  fourierdlem15  46728  fourierdlem19  46732  fourierdlem26  46739  fourierdlem35  46748  fourierdlem39  46752  fourierdlem40  46753  fourierdlem41  46754  fourierdlem42  46755  fourierdlem48  46760  fourierdlem49  46761  fourierdlem50  46762  fourierdlem51  46763  fourierdlem56  46768  fourierdlem57  46769  fourierdlem59  46771  fourierdlem60  46772  fourierdlem61  46773  fourierdlem63  46775  fourierdlem64  46776  fourierdlem65  46777  fourierdlem66  46778  fourierdlem68  46780  fourierdlem71  46783  fourierdlem72  46784  fourierdlem73  46785  fourierdlem74  46786  fourierdlem75  46787  fourierdlem76  46788  fourierdlem78  46790  fourierdlem79  46791  fourierdlem81  46793  fourierdlem82  46794  fourierdlem83  46795  fourierdlem84  46796  fourierdlem88  46800  fourierdlem89  46801  fourierdlem90  46802  fourierdlem91  46803  fourierdlem92  46804  fourierdlem93  46805  fourierdlem95  46807  fourierdlem97  46809  fourierdlem101  46813  fourierdlem103  46815  fourierdlem104  46816  fourierdlem107  46819  fourierdlem109  46821  fourierdlem111  46823  fouriersw  46837  elaa2lem  46839  etransclem23  46863  rrxtopnfi  46893  rrndistlt  46896  ioorrnopnlem  46910  ioorrnopnxrlem  46912  sge0gtfsumgt  47049  iundjiun  47066  volicorecl  47152  hoiprodcl  47153  hoiprodcl3  47186  volicore  47187  hoidmvcl  47188  hoidmv1lelem2  47198  hoidmv1lelem3  47199  hoidmv1le  47200  hoidmvlelem1  47201  hoidmvlelem2  47202  hoiqssbllem1  47228  hoiqssbllem2  47229  hoiqssbllem3  47230  hspmbllem1  47232  ovolval5lem1  47258  ovolval5lem2  47259  iunhoiioolem  47281  iccvonmbllem  47284  vonicclem1  47289  preimageiingt  47326  salpreimagtge  47331  smfaddlem1  47369  smflimlem4  47380  smfmullem1  47397  smfmullem2  47398  smfmullem3  47399  ltsubsubaddltsub  47927  2elfz2melfz  47944  2tceilhalfelfzo1  47962  flmrecm1  47969  requad01  48275  requad1  48276  requad2  48277  bgoldbtbndlem2  48460  bgoldbtbndlem3  48461  bgoldbtbndlem4  48462  bgoldbtbnd  48463  gpgedgvtx0  48715  gpgedgvtx1  48716  gpg5nbgrvtx03starlem2  48723  gpg5nbgrvtx13starlem2  48726  ply1mulgsumlem2  49052  nnpw2pmod  49248  dignn0flhalflem1  49280  affinecomb1  49367  rrxlinesc  49400  rrxlinec  49401  eenglngeehlnmlem1  49402  eenglngeehlnmlem2  49403  rrx2vlinest  49406  rrx2linest2  49409  2sphere  49414  line2  49417  itsclc0lem2  49422  itsclc0lem3  49423  itscnhlc0yqe  49424  itsclc0yqsollem2  49428  itsclc0yqsol  49429  itscnhlc0xyqsol  49430  itsclinecirc0  49438  itsclinecirc0b  49439  itsclinecirc0in  49440  itsclquadb  49441  2itscp  49446  itscnhlinecirc02plem1  49447  itscnhlinecirc02p  49450  inlinecirc02plem  49451  amgmwlem  50476