Theorem resubcld 11578

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7367  ℝcr 11037   − cmin 11377

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 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-ltxr 11184  df-sub 11379  df-neg 11380

This theorem is referenced by:  ltsubadd  11620  lesubadd  11622  lesub1  11644  lesub2  11645  ltsub1  11646  ltsub2  11647  lt2sub  11648  le2sub  11649  ltmul1a  12004  supaddc  12123  cru  12151  ge2halflem1  13059  qbtwnre  13151  lincmb01cmp  13448  iccf1o  13449  xov1plusxeqvd  13451  intfracq  13818  fldiv  13819  modlt  13839  modsubdir  13902  modsumfzodifsn  13906  serle  14019  expmulnbnd  14197  discr  14202  fzsdom2  14390  cshwidxmod  14765  crre  15076  remullem  15090  01sqrexlem7  15210  absrdbnd  15304  fzomaxdiflem  15305  caubnd2  15320  amgm2  15332  icodiamlt  15400  bhmafibid1  15430  mulcn2  15558  reccn2  15559  rlimo1  15579  climle  15602  climsqz  15603  climsqz2  15604  rlimle  15610  isercolllem1  15627  climsup  15632  caucvgrlem  15635  caucvgrlem2  15637  iseraltlem2  15645  iseraltlem3  15646  iseralt  15647  fsumle  15762  cvgcmp  15779  cvgcmpce  15781  bpoly4  16024  eflt  16084  resinhcl  16123  tanhlt1  16127  sin01bnd  16152  sin01gt0  16157  moddvds  16232  bitscmp  16407  bitsinv1lem  16410  smueqlem  16459  modprm0  16776  pcbc  16871  4sqlem15  16930  blss2ps  24368  blss2  24369  blssps  24389  blss  24390  nm2dif  24590  nlmvscnlem2  24650  nrginvrcnlem  24656  iccntr  24787  icccmplem2  24789  metdstri  24817  cnllycmp  24923  evth  24926  lebnumii  24933  ipcnlem2  25211  cncmet  25289  rrxds  25360  rrxmval  25372  rrxmet  25375  rrxdstprj1  25376  rrxdsfi  25378  ehl1eudis  25387  ehl2eudis  25389  minveclem3b  25395  minveclem4  25399  ivthlem2  25419  ivthlem3  25420  ovollb2lem  25455  ovoliunlem1  25469  ovolscalem1  25480  ovolicc1  25483  ovolicc2lem4  25487  ovolicc2  25489  ovolicc  25490  voliunlem2  25518  ovolioo  25535  ioorcl2  25539  uniioovol  25546  uniioombllem2  25550  uniioombllem3a  25551  uniioombllem3  25552  uniioombllem4  25553  uniioombllem6  25555  opnmbllem  25568  volcn  25573  vitalilem2  25576  ismbf3d  25621  mbfaddlem  25627  i1fadd  25662  itg1addlem4  25666  mbfi1fseqlem6  25687  itg2seq  25709  itg2split  25716  itg2cnlem2  25729  itg2cn  25730  itgrevallem1  25762  dvcjbr  25916  dvferm1lem  25951  dvferm2lem  25953  cmvth  25958  mvth  25959  dvlip  25960  dvlip2  25962  c1liplem1  25963  dvgt0  25971  dvlt0  25972  dvge0  25973  dvle  25974  dvivthlem1  25975  lhop1lem  25980  lhop  25983  dvcnvrelem1  25984  dvcnvrelem2  25985  dvcnvre  25986  dvcvx  25987  dvfsumle  25988  dvfsumge  25989  dvfsumrlimf  25992  dvfsumlem2  25994  dvfsumlem3  25995  dvfsumlem4  25996  dvfsum2  26001  ftc1a  26004  ftc1lem4  26006  coe1mul3  26064  ply1divex  26102  plydivex  26263  aalioulem2  26299  aalioulem3  26300  aalioulem4  26301  aalioulem5  26302  aalioulem6  26303  aaliou3lem7  26315  taylthlem2  26339  mtest  26369  pilem2  26417  tangtx  26469  cosordlem  26494  efif1olem2  26507  logcnlem3  26608  logcnlem4  26609  isosctrlem2  26783  chordthmlem2  26797  chordthmlem4  26799  heron  26802  atanlogsublem  26879  atantan  26887  birthdaylem3  26917  logdifbnd  26957  emcllem1  26959  emcllem2  26960  emcllem5  26963  emcllem6  26964  harmonicbnd4  26974  fsumharmonic  26975  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamucov  27001  relgamcl  27025  ftalem2  27037  ftalem5  27040  chpub  27183  logfaclbnd  27185  logfacbnd3  27186  logexprlim  27188  bposlem1  27247  bposlem9  27255  gausslemma2dlem1a  27328  lgseisenlem1  27338  lgsquadlem1  27343  2sqmod  27399  chtppilimlem1  27436  vmadivsum  27445  vmadivsumb  27446  rplogsumlem1  27447  rplogsumlem2  27448  rpvmasumlem  27450  dchrisumlem2  27453  dchrisum0re  27476  rplogsum  27490  mulogsumlem  27494  mulog2sumlem1  27497  vmalogdivsum2  27501  vmalogdivsum  27502  2vmadivsumlem  27503  log2sumbnd  27507  selbergb  27512  selberg2lem  27513  selberg2b  27515  chpdifbndlem1  27516  selberg3lem1  27520  selberg3lem2  27521  selberg3  27522  selberg4lem1  27523  selberg4  27524  pntrf  27526  pntrmax  27527  pntrsumo1  27528  selberg3r  27532  selberg4r  27533  selberg34r  27534  pntrlog2bndlem1  27540  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  pntrlog2bnd  27547  pntpbnd1a  27548  pntpbnd2  27550  pntibndlem2  27554  pntlemg  27561  pntlemn  27563  pntlemj  27566  pntlemf  27568  pntlemo  27570  pntlem3  27572  pntleml  27574  ttgcontlem1  28953  eqeelen  28973  brbtwn2  28974  colinearalg  28979  axcgrid  28985  axsegconlem1  28986  axsegconlem3  28988  axsegconlem8  28993  axsegconlem9  28994  axsegconlem10  28995  ax5seglem3a  28999  ax5seg  29007  axpaschlem  29009  axcontlem8  29040  nbusgrvtxm1  29448  crctcshwlkn0lem3  29880  crctcshwlkn0lem5  29882  crctcsh  29892  clwlkclwwlklem2fv2  30066  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  nvabs  30743  dipcj  30785  minvecolem4  30951  lt2addrd  32823  xlt2addrd  32832  fzsplit3  32866  bcm1n  32868  sgnsub  32910  ply1degltel  33654  ply1degltlss  33656  iconstr  33910  constrresqrtcl  33921  cos9thpiminplylem1  33926  submateqlem1  33951  cnre2csqlem  34054  tpr2rico  34056  dya2ub  34414  dya2icoseg  34421  ballotlemfcc  34638  ballotlemfrcn0  34674  signslema  34706  ftc2re  34742  subfacval3  35371  dnibndlem8  36745  dnibndlem10  36747  dnibndlem11  36748  dnibndlem12  36749  dnicn  36752  knoppcnlem4  36756  unblimceq0  36767  unbdqndv2lem2  36770  knoppndvlem11  36782  knoppndvlem14  36785  knoppndvlem15  36786  knoppndvlem17  36788  knoppndvlem20  36791  irrdifflemf  37639  qdiff  37641  poimirlem29  37970  broucube  37975  opnmbllem0  37977  mblfinlem3  37980  mblfinlem4  37981  itg2addnclem  37992  itg2addnclem3  37994  itg2gt0cn  37996  ftc1cnnclem  38012  areacirclem1  38029  areacirclem2  38030  areacirclem4  38032  areacirclem5  38033  areacirc  38034  cntotbnd  38117  rrnmet  38150  rrndstprj1  38151  rrndstprj2  38152  lcmineqlem23  42490  intlewftc  42500  aks4d1p1p2  42509  aks4d1p1p4  42510  dvle2  42511  aks4d1p1  42515  primrootlekpowne0  42544  hashscontpow1  42560  aks6d1c2  42569  aks6d1c5lem2  42577  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  aks6d1c6lem3  42611  bcled  42617  bcle2d  42618  unitscyglem2  42635  unitscyglem4  42637  readdrcl2d  42705  frlmvscadiccat  42951  fltnlta  43096  3cubeslem2  43117  3cubeslem4  43121  irrapxlem2  43251  irrapxlem3  43252  irrapxlem4  43253  irrapxlem5  43254  pellexlem2  43258  pellexlem6  43262  pell1qrgaplem  43301  rmspecsqrtnq  43334  rmspecfund  43337  rmspecpos  43344  jm2.24nn  43387  jm2.17c  43390  fzmaxdif  43409  acongeq  43411  modabsdifz  43414  jm3.1lem2  43446  areaquad  43644  sqrtcvallem2  44064  sqrtcvallem3  44065  sqrtcval  44068  imo72b2lem0  44592  cvgdvgrat  44740  hashnzfzclim  44749  binomcxplemdvbinom  44780  oddfl  45711  lefldiveq  45725  fperiodmul  45737  fzdifsuc2  45743  suprltrp  45758  supxrgere  45763  supxrgelem  45767  suplesup  45769  infleinflem2  45800  infleinf  45801  xrralrecnnge  45819  iccshift  45948  iooshift  45952  iooiinicc  45972  fmul01lt1lem2  46015  climinf  46036  sumnnodd  46060  ltmod  46066  lptre2pt  46068  climleltrp  46104  limsupgtlem  46205  liminflimsupclim  46235  fperdvper  46347  dvbdfbdioolem1  46356  dvbdfbdioolem2  46357  dvbdfbdioo  46358  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnmul  46371  iblspltprt  46401  itgspltprt  46407  itgiccshift  46408  itgperiod  46409  itgsbtaddcnst  46410  sublevolico  46412  stoweidlem1  46429  stoweidlem11  46439  stoweidlem12  46440  stoweidlem13  46441  stoweidlem14  46442  stoweidlem23  46451  stoweidlem24  46452  stoweidlem25  46453  stoweidlem26  46454  stoweidlem34  46462  stoweidlem40  46468  stoweidlem41  46469  stoweidlem42  46470  stoweidlem45  46473  stoweidlem60  46488  stoweidlem62  46490  wallispilem3  46495  wallispilem4  46496  wallispi  46498  wallispi2lem1  46499  stirlinglem5  46506  stirlinglem11  46512  stirlinglem12  46513  dirkercncflem1  46531  fourierdlem4  46539  fourierdlem6  46541  fourierdlem7  46542  fourierdlem9  46544  fourierdlem13  46548  fourierdlem14  46549  fourierdlem15  46550  fourierdlem19  46554  fourierdlem26  46561  fourierdlem35  46570  fourierdlem39  46574  fourierdlem40  46575  fourierdlem41  46576  fourierdlem42  46577  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem51  46585  fourierdlem56  46590  fourierdlem57  46591  fourierdlem59  46593  fourierdlem60  46594  fourierdlem61  46595  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem66  46600  fourierdlem68  46602  fourierdlem71  46605  fourierdlem72  46606  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem78  46612  fourierdlem79  46613  fourierdlem81  46615  fourierdlem82  46616  fourierdlem83  46617  fourierdlem84  46618  fourierdlem88  46622  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem92  46626  fourierdlem93  46627  fourierdlem95  46629  fourierdlem97  46631  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem107  46641  fourierdlem109  46643  fourierdlem111  46645  fouriersw  46659  elaa2lem  46661  etransclem23  46685  rrxtopnfi  46715  rrndistlt  46718  ioorrnopnlem  46732  ioorrnopnxrlem  46734  sge0gtfsumgt  46871  iundjiun  46888  volicorecl  46974  hoiprodcl  46975  hoiprodcl3  47008  volicore  47009  hoidmvcl  47010  hoidmv1lelem2  47020  hoidmv1lelem3  47021  hoidmv1le  47022  hoidmvlelem1  47023  hoidmvlelem2  47024  hoiqssbllem1  47050  hoiqssbllem2  47051  hoiqssbllem3  47052  hspmbllem1  47054  ovolval5lem1  47080  ovolval5lem2  47081  iunhoiioolem  47103  iccvonmbllem  47106  vonicclem1  47111  preimageiingt  47148  salpreimagtge  47153  smfaddlem1  47191  smflimlem4  47202  smfmullem1  47219  smfmullem2  47220  smfmullem3  47221  ltsubsubaddltsub  47749  2elfz2melfz  47766  2tceilhalfelfzo1  47784  flmrecm1  47791  requad01  48097  requad1  48098  requad2  48099  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  bgoldbtbndlem4  48284  bgoldbtbnd  48285  gpgedgvtx0  48537  gpgedgvtx1  48538  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx13starlem2  48548  ply1mulgsumlem2  48863  nnpw2pmod  49059  dignn0flhalflem1  49091  affinecomb1  49178  rrxlinesc  49211  rrxlinec  49212  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214  rrx2vlinest  49217  rrx2linest2  49220  2sphere  49225  line2  49228  itsclc0lem2  49233  itsclc0lem3  49234  itscnhlc0yqe  49235  itsclc0yqsollem2  49239  itsclc0yqsol  49240  itscnhlc0xyqsol  49241  itsclinecirc0  49249  itsclinecirc0b  49250  itsclinecirc0in  49251  itsclquadb  49252  2itscp  49257  itscnhlinecirc02plem1  49258  itscnhlinecirc02p  49261  inlinecirc02plem  49262  amgmwlem  50277