Theorem resubcld 11572

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7361  ℝcr 11031   − cmin 11371

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-ltxr 11178  df-sub 11373  df-neg 11374

This theorem is referenced by:  ltsubadd  11614  lesubadd  11616  lesub1  11638  lesub2  11639  ltsub1  11640  ltsub2  11641  lt2sub  11642  le2sub  11643  ltmul1a  11998  supaddc  12117  cru  12145  ge2halflem1  13053  qbtwnre  13145  lincmb01cmp  13442  iccf1o  13443  xov1plusxeqvd  13445  intfracq  13812  fldiv  13813  modlt  13833  modsubdir  13896  modsumfzodifsn  13900  serle  14013  expmulnbnd  14191  discr  14196  fzsdom2  14384  cshwidxmod  14759  crre  15070  remullem  15084  01sqrexlem7  15204  absrdbnd  15298  fzomaxdiflem  15299  caubnd2  15314  amgm2  15326  icodiamlt  15394  bhmafibid1  15424  mulcn2  15552  reccn2  15553  rlimo1  15573  climle  15596  climsqz  15597  climsqz2  15598  rlimle  15604  isercolllem1  15621  climsup  15626  caucvgrlem  15629  caucvgrlem2  15631  iseraltlem2  15639  iseraltlem3  15640  iseralt  15641  fsumle  15756  cvgcmp  15773  cvgcmpce  15775  bpoly4  16018  eflt  16078  resinhcl  16117  tanhlt1  16121  sin01bnd  16146  sin01gt0  16151  moddvds  16226  bitscmp  16401  bitsinv1lem  16404  smueqlem  16453  modprm0  16770  pcbc  16865  4sqlem15  16924  blss2ps  24381  blss2  24382  blssps  24402  blss  24403  nm2dif  24603  nlmvscnlem2  24663  nrginvrcnlem  24669  iccntr  24800  icccmplem2  24802  metdstri  24830  cnllycmp  24936  evth  24939  lebnumii  24946  ipcnlem2  25224  cncmet  25302  rrxds  25373  rrxmval  25385  rrxmet  25388  rrxdstprj1  25389  rrxdsfi  25391  ehl1eudis  25400  ehl2eudis  25402  minveclem3b  25408  minveclem4  25412  ivthlem2  25432  ivthlem3  25433  ovollb2lem  25468  ovoliunlem1  25482  ovolscalem1  25493  ovolicc1  25496  ovolicc2lem4  25500  ovolicc2  25502  ovolicc  25503  voliunlem2  25531  ovolioo  25548  ioorcl2  25552  uniioovol  25559  uniioombllem2  25563  uniioombllem3a  25564  uniioombllem3  25565  uniioombllem4  25566  uniioombllem6  25568  opnmbllem  25581  volcn  25586  vitalilem2  25589  ismbf3d  25634  mbfaddlem  25640  i1fadd  25675  itg1addlem4  25679  mbfi1fseqlem6  25700  itg2seq  25722  itg2split  25729  itg2cnlem2  25742  itg2cn  25743  itgrevallem1  25775  dvcjbr  25929  dvferm1lem  25964  dvferm2lem  25966  cmvth  25971  mvth  25972  dvlip  25973  dvlip2  25975  c1liplem1  25976  dvgt0  25984  dvlt0  25985  dvge0  25986  dvle  25987  dvivthlem1  25988  lhop1lem  25993  lhop  25996  dvcnvrelem1  25997  dvcnvrelem2  25998  dvcnvre  25999  dvcvx  26000  dvfsumle  26001  dvfsumge  26002  dvfsumrlimf  26005  dvfsumlem2  26007  dvfsumlem3  26008  dvfsumlem4  26009  dvfsum2  26014  ftc1a  26017  ftc1lem4  26019  coe1mul3  26077  ply1divex  26115  plydivex  26277  aalioulem2  26313  aalioulem3  26314  aalioulem4  26315  aalioulem5  26316  aalioulem6  26317  aaliou3lem7  26329  taylthlem2  26354  taylthlem2OLD  26355  mtest  26385  pilem2  26433  tangtx  26485  cosordlem  26510  efif1olem2  26523  logcnlem3  26624  logcnlem4  26625  isosctrlem2  26799  chordthmlem2  26813  chordthmlem4  26815  heron  26818  atanlogsublem  26895  atantan  26903  birthdaylem3  26933  logdifbnd  26974  emcllem1  26976  emcllem2  26977  emcllem5  26980  emcllem6  26981  harmonicbnd4  26991  fsumharmonic  26992  lgamgulmlem2  27010  lgamgulmlem3  27011  lgamucov  27018  relgamcl  27042  ftalem2  27054  ftalem5  27057  chpub  27200  logfaclbnd  27202  logfacbnd3  27203  logexprlim  27205  bposlem1  27264  bposlem9  27272  gausslemma2dlem1a  27345  lgseisenlem1  27355  lgsquadlem1  27360  2sqmod  27416  chtppilimlem1  27453  vmadivsum  27462  vmadivsumb  27463  rplogsumlem1  27464  rplogsumlem2  27465  rpvmasumlem  27467  dchrisumlem2  27470  dchrisum0re  27493  rplogsum  27507  mulogsumlem  27511  mulog2sumlem1  27514  vmalogdivsum2  27518  vmalogdivsum  27519  2vmadivsumlem  27520  log2sumbnd  27524  selbergb  27529  selberg2lem  27530  selberg2b  27532  chpdifbndlem1  27533  selberg3lem1  27537  selberg3lem2  27538  selberg3  27539  selberg4lem1  27540  selberg4  27541  pntrf  27543  pntrmax  27544  pntrsumo1  27545  selberg3r  27549  selberg4r  27550  selberg34r  27551  pntrlog2bndlem1  27557  pntrlog2bndlem2  27558  pntrlog2bndlem3  27559  pntrlog2bndlem4  27560  pntrlog2bndlem5  27561  pntrlog2bndlem6  27563  pntrlog2bnd  27564  pntpbnd1a  27565  pntpbnd2  27567  pntibndlem2  27571  pntlemg  27578  pntlemn  27580  pntlemj  27583  pntlemf  27585  pntlemo  27587  pntlem3  27589  pntleml  27591  ttgcontlem1  28970  eqeelen  28990  brbtwn2  28991  colinearalg  28996  axcgrid  29002  axsegconlem1  29003  axsegconlem3  29005  axsegconlem8  29010  axsegconlem9  29011  axsegconlem10  29012  ax5seglem3a  29016  ax5seg  29024  axpaschlem  29026  axcontlem8  29057  nbusgrvtxm1  29465  crctcshwlkn0lem3  29898  crctcshwlkn0lem5  29900  crctcsh  29910  clwlkclwwlklem2fv2  30084  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  nvabs  30761  dipcj  30803  minvecolem4  30969  lt2addrd  32841  xlt2addrd  32850  fzsplit3  32884  bcm1n  32886  sgnsub  32928  ply1degltel  33672  ply1degltlss  33674  iconstr  33929  constrresqrtcl  33940  cos9thpiminplylem1  33945  submateqlem1  33970  cnre2csqlem  34073  tpr2rico  34075  dya2ub  34433  dya2icoseg  34440  ballotlemfcc  34657  ballotlemfrcn0  34693  signslema  34725  ftc2re  34761  subfacval3  35390  dnibndlem8  36764  dnibndlem10  36766  dnibndlem11  36767  dnibndlem12  36768  dnicn  36771  knoppcnlem4  36775  unblimceq0  36786  unbdqndv2lem2  36789  knoppndvlem11  36801  knoppndvlem14  36804  knoppndvlem15  36805  knoppndvlem17  36807  knoppndvlem20  36810  irrdifflemf  37658  poimirlem29  37987  broucube  37992  opnmbllem0  37994  mblfinlem3  37997  mblfinlem4  37998  itg2addnclem  38009  itg2addnclem3  38011  itg2gt0cn  38013  ftc1cnnclem  38029  areacirclem1  38046  areacirclem2  38047  areacirclem4  38049  areacirclem5  38050  areacirc  38051  cntotbnd  38134  rrnmet  38167  rrndstprj1  38168  rrndstprj2  38169  lcmineqlem23  42507  intlewftc  42517  aks4d1p1p2  42526  aks4d1p1p4  42527  dvle2  42528  aks4d1p1  42532  primrootlekpowne0  42561  hashscontpow1  42577  aks6d1c2  42586  aks6d1c5lem2  42594  sticksstones10  42611  sticksstones12a  42613  sticksstones12  42614  aks6d1c6lem3  42628  bcled  42634  bcle2d  42635  unitscyglem2  42652  unitscyglem4  42654  readdrcl2d  42722  frlmvscadiccat  42968  fltnlta  43113  3cubeslem2  43134  3cubeslem4  43138  irrapxlem2  43272  irrapxlem3  43273  irrapxlem4  43274  irrapxlem5  43275  pellexlem2  43279  pellexlem6  43283  pell1qrgaplem  43322  rmspecsqrtnq  43355  rmspecfund  43358  rmspecpos  43365  jm2.24nn  43408  jm2.17c  43411  fzmaxdif  43430  acongeq  43432  modabsdifz  43435  jm3.1lem2  43467  areaquad  43665  sqrtcvallem2  44085  sqrtcvallem3  44086  sqrtcval  44089  imo72b2lem0  44613  cvgdvgrat  44761  hashnzfzclim  44770  binomcxplemdvbinom  44801  oddfl  45732  lefldiveq  45746  fperiodmul  45758  fzdifsuc2  45764  suprltrp  45779  supxrgere  45784  supxrgelem  45788  suplesup  45790  infleinflem2  45821  infleinf  45822  xrralrecnnge  45840  iccshift  45969  iooshift  45973  iooiinicc  45993  fmul01lt1lem2  46036  climinf  46057  sumnnodd  46081  ltmod  46087  lptre2pt  46089  climleltrp  46125  limsupgtlem  46226  liminflimsupclim  46256  fperdvper  46368  dvbdfbdioolem1  46377  dvbdfbdioolem2  46378  dvbdfbdioo  46379  ioodvbdlimc1lem1  46380  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  dvnmul  46392  iblspltprt  46422  itgspltprt  46428  itgiccshift  46429  itgperiod  46430  itgsbtaddcnst  46431  sublevolico  46433  stoweidlem1  46450  stoweidlem11  46460  stoweidlem12  46461  stoweidlem13  46462  stoweidlem14  46463  stoweidlem23  46472  stoweidlem24  46473  stoweidlem25  46474  stoweidlem26  46475  stoweidlem34  46483  stoweidlem40  46489  stoweidlem41  46490  stoweidlem42  46491  stoweidlem45  46494  stoweidlem60  46509  stoweidlem62  46511  wallispilem3  46516  wallispilem4  46517  wallispi  46519  wallispi2lem1  46520  stirlinglem5  46527  stirlinglem11  46533  stirlinglem12  46534  dirkercncflem1  46552  fourierdlem4  46560  fourierdlem6  46562  fourierdlem7  46563  fourierdlem9  46565  fourierdlem13  46569  fourierdlem14  46570  fourierdlem15  46571  fourierdlem19  46575  fourierdlem26  46582  fourierdlem35  46591  fourierdlem39  46595  fourierdlem40  46596  fourierdlem41  46597  fourierdlem42  46598  fourierdlem48  46603  fourierdlem49  46604  fourierdlem50  46605  fourierdlem51  46606  fourierdlem56  46611  fourierdlem57  46612  fourierdlem59  46614  fourierdlem60  46615  fourierdlem61  46616  fourierdlem63  46618  fourierdlem64  46619  fourierdlem65  46620  fourierdlem66  46621  fourierdlem68  46623  fourierdlem71  46626  fourierdlem72  46627  fourierdlem73  46628  fourierdlem74  46629  fourierdlem75  46630  fourierdlem76  46631  fourierdlem78  46633  fourierdlem79  46634  fourierdlem81  46636  fourierdlem82  46637  fourierdlem83  46638  fourierdlem84  46639  fourierdlem88  46643  fourierdlem89  46644  fourierdlem90  46645  fourierdlem91  46646  fourierdlem92  46647  fourierdlem93  46648  fourierdlem95  46650  fourierdlem97  46652  fourierdlem101  46656  fourierdlem103  46658  fourierdlem104  46659  fourierdlem107  46662  fourierdlem109  46664  fourierdlem111  46666  fouriersw  46680  elaa2lem  46682  etransclem23  46706  rrxtopnfi  46736  rrndistlt  46739  ioorrnopnlem  46753  ioorrnopnxrlem  46755  sge0gtfsumgt  46892  iundjiun  46909  volicorecl  46995  hoiprodcl  46996  hoiprodcl3  47029  volicore  47030  hoidmvcl  47031  hoidmv1lelem2  47041  hoidmv1lelem3  47042  hoidmv1le  47043  hoidmvlelem1  47044  hoidmvlelem2  47045  hoiqssbllem1  47071  hoiqssbllem2  47072  hoiqssbllem3  47073  hspmbllem1  47075  ovolval5lem1  47101  ovolval5lem2  47102  iunhoiioolem  47124  iccvonmbllem  47127  vonicclem1  47132  preimageiingt  47169  salpreimagtge  47174  smfaddlem1  47212  smflimlem4  47223  smfmullem1  47240  smfmullem2  47241  smfmullem3  47242  ltsubsubaddltsub  47764  2elfz2melfz  47781  2tceilhalfelfzo1  47799  flmrecm1  47806  requad01  48112  requad1  48113  requad2  48114  bgoldbtbndlem2  48297  bgoldbtbndlem3  48298  bgoldbtbndlem4  48299  bgoldbtbnd  48300  gpgedgvtx0  48552  gpgedgvtx1  48553  gpg5nbgrvtx03starlem2  48560  gpg5nbgrvtx13starlem2  48563  ply1mulgsumlem2  48878  nnpw2pmod  49074  dignn0flhalflem1  49106  affinecomb1  49193  rrxlinesc  49226  rrxlinec  49227  eenglngeehlnmlem1  49228  eenglngeehlnmlem2  49229  rrx2vlinest  49232  rrx2linest2  49235  2sphere  49240  line2  49243  itsclc0lem2  49248  itsclc0lem3  49249  itscnhlc0yqe  49250  itsclc0yqsollem2  49254  itsclc0yqsol  49255  itscnhlc0xyqsol  49256  itsclinecirc0  49264  itsclinecirc0b  49265  itsclinecirc0in  49266  itsclquadb  49267  2itscp  49272  itscnhlinecirc02plem1  49273  itscnhlinecirc02p  49276  inlinecirc02plem  49277  amgmwlem  50292