MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  resubcld Structured version   Visualization version   GIF version

Theorem resubcld 10621
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
StepHypRef Expression
1 renegcld.1 . 2 (𝜑𝐴 ∈ ℝ)
2 resubcld.2 . 2 (𝜑𝐵 ∈ ℝ)
3 resubcl 10508 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵) ∈ ℝ)
41, 2, 3syl2anc 696 1 (𝜑 → (𝐴𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2127  (class class class)co 6801  cr 10098  cmin 10429
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102  ax-resscn 10156  ax-1cn 10157  ax-icn 10158  ax-addcl 10159  ax-addrcl 10160  ax-mulcl 10161  ax-mulrcl 10162  ax-mulcom 10163  ax-addass 10164  ax-mulass 10165  ax-distr 10166  ax-i2m1 10167  ax-1ne0 10168  ax-1rid 10169  ax-rnegex 10170  ax-rrecex 10171  ax-cnre 10172  ax-pre-lttri 10173  ax-pre-lttrn 10174  ax-pre-ltadd 10175
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-nel 3024  df-ral 3043  df-rex 3044  df-reu 3045  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-opab 4853  df-mpt 4870  df-id 5162  df-po 5175  df-so 5176  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-riota 6762  df-ov 6804  df-oprab 6805  df-mpt2 6806  df-er 7899  df-en 8110  df-dom 8111  df-sdom 8112  df-pnf 10239  df-mnf 10240  df-ltxr 10242  df-sub 10431  df-neg 10432
This theorem is referenced by:  ltsubadd  10661  lesubadd  10663  lesub1  10685  lesub2  10686  ltsub1  10687  ltsub2  10688  lt2sub  10689  le2sub  10690  ltmul1a  11035  supaddc  11153  cru  11175  qbtwnre  12194  lincmb01cmp  12479  iccf1o  12480  xov1plusxeqvd  12482  intfracq  12823  fldiv  12824  modlt  12844  modsubdir  12904  modsumfzodifsn  12908  serle  13021  expmulnbnd  13161  discr  13166  fzsdom2  13378  cshwidxmod  13720  crre  14024  remullem  14038  sqrlem7  14159  absrdbnd  14251  fzomaxdiflem  14252  caubnd2  14267  amgm2  14279  icodiamlt  14344  mulcn2  14496  reccn2  14497  rlimo1  14517  climle  14540  climsqz  14541  climsqz2  14542  rlimle  14548  isercolllem1  14565  climsup  14570  caucvgrlem  14573  caucvgrlem2  14575  iseraltlem2  14583  iseraltlem3  14584  iseralt  14585  fsumle  14701  cvgcmp  14718  cvgcmpce  14720  bpoly4  14960  eflt  15017  resinhcl  15056  tanhlt1  15060  sin01bnd  15085  sin01gt0  15090  moddvds  15164  bitscmp  15333  bitsinv1lem  15336  smueqlem  15385  modprm0  15683  pcbc  15777  4sqlem15  15836  blss2ps  22380  blss2  22381  blssps  22401  blss  22402  nm2dif  22601  nlmvscnlem2  22661  nrginvrcnlem  22667  iccntr  22796  icccmplem2  22798  metdstri  22826  cnllycmp  22927  evth  22930  lebnumii  22937  ipcnlem2  23214  cncmet  23290  rrxds  23352  rrxmval  23359  rrxmet  23362  rrxdstprj1  23363  minveclem3b  23370  minveclem4  23374  ivthlem2  23392  ivthlem3  23393  ovollb2lem  23427  ovoliunlem1  23441  ovolscalem1  23452  ovolicc1  23455  ovolicc2lem4  23459  ovolicc2  23461  ovolicc  23462  voliunlem2  23490  ovolioo  23507  ioorcl2  23511  uniioovol  23518  uniioombllem2  23522  uniioombllem3a  23523  uniioombllem3  23524  uniioombllem4  23525  uniioombllem6  23527  opnmbllem  23540  volcn  23545  vitalilem2  23548  ismbf3d  23591  mbfaddlem  23597  i1fadd  23632  itg1addlem4  23636  mbfi1fseqlem6  23657  itg2seq  23679  itg2split  23686  itg2cnlem2  23699  itg2cn  23700  itgrevallem1  23731  dvcjbr  23882  dvferm1lem  23917  dvferm2lem  23919  cmvth  23924  mvth  23925  dvlip  23926  dvlip2  23928  c1liplem1  23929  dvgt0  23937  dvlt0  23938  dvge0  23939  dvle  23940  dvivthlem1  23941  lhop1lem  23946  lhop  23949  dvcnvrelem1  23950  dvcnvrelem2  23951  dvcnvre  23952  dvcvx  23953  dvfsumle  23954  dvfsumge  23955  dvfsumrlimf  23958  dvfsumlem2  23960  dvfsumlem3  23961  dvfsumlem4  23962  dvfsum2  23967  ftc1a  23970  ftc1lem4  23972  coe1mul3  24029  ply1divex  24066  plydivex  24222  aalioulem2  24258  aalioulem3  24259  aalioulem4  24260  aalioulem5  24261  aalioulem6  24262  aaliou3lem7  24274  taylthlem2  24298  mtest  24328  pilem2  24376  tangtx  24427  cosordlem  24447  efif1olem2  24459  logcnlem3  24560  logcnlem4  24561  isosctrlem2  24719  chordthmlem2  24730  chordthmlem4  24732  heron  24735  atanlogsublem  24812  atantan  24820  birthdaylem3  24850  logdifbnd  24890  emcllem1  24892  emcllem2  24893  emcllem5  24896  emcllem6  24897  harmonicbnd4  24907  fsumharmonic  24908  lgamgulmlem2  24926  lgamgulmlem3  24927  lgamucov  24934  relgamcl  24958  ftalem2  24970  ftalem5  24973  chpub  25115  logfaclbnd  25117  logfacbnd3  25118  logexprlim  25120  bposlem1  25179  bposlem9  25187  gausslemma2dlem1a  25260  lgseisenlem1  25270  lgsquadlem1  25275  chtppilimlem1  25332  vmadivsum  25341  vmadivsumb  25342  rplogsumlem1  25343  rplogsumlem2  25344  rpvmasumlem  25346  dchrisumlem2  25349  dchrisum0re  25372  rplogsum  25386  mulogsumlem  25390  mulog2sumlem1  25393  vmalogdivsum2  25397  vmalogdivsum  25398  2vmadivsumlem  25399  log2sumbnd  25403  selbergb  25408  selberg2lem  25409  selberg2b  25411  chpdifbndlem1  25412  selberg3lem1  25416  selberg3lem2  25417  selberg3  25418  selberg4lem1  25419  selberg4  25420  pntrf  25422  pntrmax  25423  pntrsumo1  25424  selberg3r  25428  selberg4r  25429  selberg34r  25430  pntrlog2bndlem1  25436  pntrlog2bndlem2  25437  pntrlog2bndlem3  25438  pntrlog2bndlem4  25439  pntrlog2bndlem5  25440  pntrlog2bndlem6  25442  pntrlog2bnd  25443  pntpbnd1a  25444  pntpbnd2  25446  pntibndlem2  25450  pntlemg  25457  pntlemn  25459  pntlemj  25462  pntlemf  25464  pntlemo  25466  pntlem3  25468  pntleml  25470  ttgcontlem1  25935  eqeelen  25954  brbtwn2  25955  colinearalg  25960  axcgrid  25966  axsegconlem1  25967  axsegconlem3  25969  axsegconlem8  25974  axsegconlem9  25975  axsegconlem10  25976  ax5seglem3a  25980  ax5seg  25988  axpaschlem  25990  axcontlem8  26021  nbusgrvtxm1  26450  crctcshwlkn0lem3  26886  crctcshwlkn0lem5  26888  crctcsh  26898  clwlkclwwlklem2fv2  27090  clwlkclwwlklem2a4  27091  clwlkclwwlklem2a  27092  nvabs  27807  dipcj  27849  minvecolem4  28016  lt2addrd  29796  xlt2addrd  29803  fzsplit3  29833  bcm1n  29834  bhmafibid1  29924  2sqmod  29928  submateqlem1  30153  cnre2csqlem  30236  tpr2rico  30238  dya2ub  30612  dya2icoseg  30619  ballotlemfcc  30835  ballotlemfrcn0  30871  sgnsub  30886  signslema  30919  ftc2re  30956  subfacval3  31449  dnibndlem8  32752  dnibndlem10  32754  dnibndlem11  32755  dnibndlem12  32756  dnicn  32759  knoppcnlem4  32763  unblimceq0  32775  unbdqndv2lem2  32778  knoppndvlem11  32790  knoppndvlem14  32793  knoppndvlem15  32794  knoppndvlem17  32796  knoppndvlem20  32799  poimirlem29  33720  broucube  33725  opnmbllem0  33727  mblfinlem3  33730  mblfinlem4  33731  itg2addnclem  33743  itg2addnclem3  33745  itg2gt0cn  33747  ftc1cnnclem  33765  areacirclem1  33782  areacirclem2  33783  areacirclem4  33785  areacirclem5  33786  areacirc  33787  cntotbnd  33877  rrnmet  33910  rrndstprj1  33911  rrndstprj2  33912  irrapxlem2  37858  irrapxlem3  37859  irrapxlem4  37860  irrapxlem5  37861  pellexlem2  37865  pellexlem6  37869  pell1qrgaplem  37908  rmspecsqrtnq  37941  rmspecfund  37945  rmspecpos  37952  jm2.24nn  37997  jm2.17c  38000  fzmaxdif  38019  acongeq  38021  modabsdifz  38024  jm3.1lem2  38056  areaquad  38273  imo72b2lem0  38936  cvgdvgrat  38983  hashnzfzclim  38992  binomcxplemdvbinom  39023  oddfl  39957  lefldiveq  39973  fperiodmul  39986  fzdifsuc2  39992  suprltrp  40011  supxrgere  40016  supxrgelem  40020  suplesup  40022  infleinflem2  40054  infleinf  40055  xrralrecnnge  40080  iccshift  40216  iooshift  40220  iooiinicc  40241  fmul01lt1lem2  40289  climinf  40310  sumnnodd  40334  ltmod  40342  lptre2pt  40344  climleltrp  40380  limsupgtlem  40481  liminflimsupclim  40511  fperdvper  40605  dvbdfbdioolem1  40615  dvbdfbdioolem2  40616  dvbdfbdioo  40617  ioodvbdlimc1lem1  40618  ioodvbdlimc1lem2  40619  ioodvbdlimc2lem  40621  dvnmul  40630  iblspltprt  40661  itgspltprt  40667  itgiccshift  40668  itgperiod  40669  itgsbtaddcnst  40670  sublevolico  40673  stoweidlem1  40690  stoweidlem11  40700  stoweidlem12  40701  stoweidlem13  40702  stoweidlem14  40703  stoweidlem23  40712  stoweidlem24  40713  stoweidlem25  40714  stoweidlem26  40715  stoweidlem34  40723  stoweidlem40  40729  stoweidlem41  40730  stoweidlem42  40731  stoweidlem45  40734  stoweidlem60  40749  stoweidlem62  40751  wallispilem3  40756  wallispilem4  40757  wallispi  40759  wallispi2lem1  40760  stirlinglem5  40767  stirlinglem11  40773  stirlinglem12  40774  dirkercncflem1  40792  fourierdlem4  40800  fourierdlem6  40802  fourierdlem7  40803  fourierdlem9  40805  fourierdlem13  40809  fourierdlem14  40810  fourierdlem15  40811  fourierdlem19  40815  fourierdlem26  40822  fourierdlem35  40831  fourierdlem39  40835  fourierdlem40  40836  fourierdlem41  40837  fourierdlem42  40838  fourierdlem48  40843  fourierdlem49  40844  fourierdlem50  40845  fourierdlem51  40846  fourierdlem56  40851  fourierdlem57  40852  fourierdlem59  40854  fourierdlem60  40855  fourierdlem61  40856  fourierdlem63  40858  fourierdlem64  40859  fourierdlem65  40860  fourierdlem66  40861  fourierdlem68  40863  fourierdlem71  40866  fourierdlem72  40867  fourierdlem73  40868  fourierdlem74  40869  fourierdlem75  40870  fourierdlem76  40871  fourierdlem78  40873  fourierdlem79  40874  fourierdlem81  40876  fourierdlem82  40877  fourierdlem83  40878  fourierdlem84  40879  fourierdlem88  40883  fourierdlem89  40884  fourierdlem90  40885  fourierdlem91  40886  fourierdlem92  40887  fourierdlem93  40888  fourierdlem95  40890  fourierdlem97  40892  fourierdlem101  40896  fourierdlem103  40898  fourierdlem104  40899  fourierdlem107  40902  fourierdlem109  40904  fourierdlem111  40906  fouriersw  40920  elaa2lem  40922  etransclem23  40946  rrxdsfi  40977  rrxtopnfi  40978  rrndistlt  40982  ioorrnopnlem  40996  ioorrnopnxrlem  40998  sge0gtfsumgt  41132  iundjiun  41149  volicorecl  41235  hoiprodcl  41236  hoiprodcl3  41269  volicore  41270  hoidmvcl  41271  hoidmv1lelem2  41281  hoidmv1lelem3  41282  hoidmv1le  41283  hoidmvlelem1  41284  hoidmvlelem2  41285  hoiqssbllem1  41311  hoiqssbllem2  41312  hoiqssbllem3  41313  hspmbllem1  41315  ovolval5lem1  41341  ovolval5lem2  41342  iunhoiioolem  41364  iccvonmbllem  41367  vonicclem1  41372  preimageiingt  41405  salpreimagtge  41409  smfaddlem1  41446  smflimlem4  41457  smfmullem1  41473  smfmullem2  41474  smfmullem3  41475  ltsubsubaddltsub  41794  2elfz2melfz  41807  bgoldbtbndlem2  42173  bgoldbtbndlem3  42174  bgoldbtbndlem4  42175  bgoldbtbnd  42176  ply1mulgsumlem2  42654  difmodm1lt  42796  nnpw2pmod  42856  dignn0flhalflem1  42888  amgmwlem  43030
  Copyright terms: Public domain W3C validator