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

Theorem 1red 10093
Description: 1 is an real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
1red (𝜑 → 1 ∈ ℝ)

Proof of Theorem 1red
StepHypRef Expression
1 1re 10077 . 2 1 ∈ ℝ
21a1i 11 1 (𝜑 → 1 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  cr 9973  1c1 9975
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rrecex 10046  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693
This theorem is referenced by:  recgt0  10905  ltrec  10943  nn0p1gt0  11360  nn0ge2m1nn  11398  nn0le2is012  11479  suprzcl  11495  ledivge1le  11939  qbtwnre  12068  iccf1o  12354  xov1plusxeqvd  12356  zltaddlt1le  12362  fznatpl1  12433  elfz1b  12447  fzonn0p1p1  12586  elfzom1p1elfzo  12587  elfznelfzo  12613  elfznelfzob  12614  fladdz  12666  2tnp1ge0ge0  12670  flhalf  12671  ltdifltdiv  12675  fldiv4lem1div2uz2  12677  mulp1mod1  12751  m1modge3gt1  12757  modltm1p1mod  12762  addmodlteq  12785  ltexp2a  12952  expcan  12953  ltexp2  12954  leexp2  12955  leexp2a  12956  leexp2r  12958  nnlesq  13008  bernneq3  13032  expnbnd  13033  expnlbnd2  13035  fzsdom2  13253  wrdlenge2n0  13374  swrd2lsw  13741  2swrd2eqwrdeq  13742  rddif  14124  reccn2  14371  rlimo1  14391  o1fsum  14589  abscvgcvg  14595  climcndslem1  14625  flo1  14630  harmonic  14635  geomulcvg  14651  fprodrecl  14727  fprodle  14771  bpoly4  14834  efcllem  14852  efgt1  14890  tanhlt1  14934  sinltx  14963  eirrlem  14976  p1modz1  15034  mod2eq1n2dvds  15118  oddge22np1  15120  ltoddhalfle  15132  nn0o1gt2  15144  nno  15145  nn0oddm1d2  15148  nnoddm1d2  15149  bitsfzolem  15203  bitsfzo  15204  bitsmod  15205  bitscmp  15207  bitsinv1lem  15210  smuval2  15251  coprmgcdb  15409  prmind2  15445  dvdsnprmd  15450  isprm5  15466  isprm7  15467  divdenle  15504  zsqrtelqelz  15513  fermltl  15536  odzdvds  15547  modprm0  15557  iserodd  15587  difsqpwdvds  15638  pcfaclem  15649  prmreclem1  15667  4sqlem11  15706  4sqlem12  15707  ramub1lem1  15777  prmgaplem8  15809  2expltfac  15846  pgpfaclem2  18527  znidomb  19958  chfacfisf  20707  chfacfisfcpmat  20708  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  nrginvrcnlem  22542  nmoid  22593  xrsmopn  22662  metnrmlem1a  22708  iccpnfhmeo  22791  htpycc  22826  pcohtpylem  22865  pcoass  22870  pcorevlem  22872  nmhmcn  22966  cncmet  23165  ovoliunlem1  23316  dyadmaxlem  23411  vitalilem2  23423  mbfi1fseqlem6  23532  itg2mulc  23559  itg2monolem1  23562  itg2monolem3  23564  dveflem  23787  mvth  23800  dvlipcn  23802  lhop1lem  23821  dvfsumlem1  23834  dvfsumlem2  23835  dvfsumlem3  23836  dvfsumlem4  23837  dvfsum2  23842  fta1glem2  23971  plyeq0lem  24011  fta1lem  24107  vieta1lem2  24111  aalioulem3  24134  aalioulem4  24135  radcnvlem1  24212  radcnvlem2  24213  dvradcnv  24220  abelthlem2  24231  abelthlem5  24234  abelthlem7  24237  abelth2  24241  cosne0  24321  rplogcl  24395  logdivlti  24411  logno1  24427  advlog  24445  logtayllem  24450  cxplt  24485  cxple  24486  cxpaddlelem  24537  cxpaddle  24538  relogbf  24574  isosctrlem1  24593  isosctrlem2  24594  heron  24610  atanlogaddlem  24685  bndatandm  24701  leibpi  24714  log2tlbnd  24717  birthdaylem3  24725  rlimcnp  24737  rlimcnp2  24738  efrlim  24741  cxp2limlem  24747  divsqrtsumo1  24755  jensenlem2  24759  logdiflbnd  24766  fsumharmonic  24783  lgamgulmlem2  24801  lgamgulmlem3  24802  lgamgulmlem4  24803  lgamgulmlem5  24804  lgamgulmlem6  24805  lgamcvg2  24826  regamcl  24832  wilthlem2  24840  ftalem2  24845  basellem9  24860  vma1  24937  ppieq0  24947  mumullem2  24951  fsumfldivdiaglem  24960  chpeq0  24978  chtub  24982  chpval2  24988  chpchtsum  24989  chpub  24990  logfacrlim  24994  logexprlim  24995  mersenne  24997  perfectlem2  25000  dchrelbas4  25013  bcmono  25047  bposlem1  25054  bposlem2  25055  zabsle1  25066  lgslem3  25069  lgsmod  25093  lgsdir2lem4  25098  lgsdirprm  25101  gausslemma2dlem1a  25135  gausslemma2d  25144  lgsquadlem2  25151  2sqlem8  25196  chebbnd1lem1  25203  chebbnd1lem2  25204  chtppilimlem1  25207  chebbnd2  25211  chto1lb  25212  chpchtlim  25213  chpo1ubb  25215  vmadivsum  25216  rplogsumlem1  25218  rpvmasumlem  25221  dchrisumlem3  25225  dchrmusumlema  25227  dchrmusum2  25228  dchrvmasumlem2  25232  dchrvmasumlem3  25233  dchrvmasumiflem1  25235  dchrvmasumiflem2  25236  dchrisum0flblem1  25242  dchrisum0flblem2  25243  dchrisum0fno1  25245  dchrisum0re  25247  dchrisum0lema  25248  dchrisum0lem1b  25249  dchrisum0lem2a  25251  dchrisum0lem2  25252  dchrisum0lem3  25253  rplogsum  25261  dirith2  25262  mudivsum  25264  mulogsumlem  25265  mulogsum  25266  mulog2sumlem1  25268  mulog2sumlem2  25269  vmalogdivsum2  25272  vmalogdivsum  25273  2vmadivsumlem  25274  log2sumbnd  25278  selberglem2  25280  selberg2lem  25284  chpdifbnd  25289  selberg3lem1  25291  selberg3  25293  selberg4lem1  25294  selberg4  25295  pntrmax  25298  pntrsumo1  25299  pntrsumbnd  25300  selberg3r  25303  selberg4r  25304  selberg34r  25305  pntrlog2bndlem1  25311  pntrlog2bndlem2  25312  pntrlog2bndlem3  25313  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntrlog2bndlem6  25317  pntrlog2bnd  25318  pntpbnd1a  25319  pntpbnd1  25320  pntibndlem2a  25324  pntibndlem2  25325  pntibnd  25327  pntlemc  25329  pntlemg  25332  pntlemr  25336  pntlemk  25340  qabvle  25359  ostth2lem3  25369  ostth2  25371  trgcgrg  25455  tgcgr4  25471  ttgcontlem1  25810  axpaschlem  25865  axlowdimlem16  25882  axcontlem2  25890  axcontlem7  25895  nbusgrvtxm1  26325  upgrewlkle2  26558  pthdlem1  26718  crctcshwlkn0lem3  26760  crctcshwlkn0lem5  26762  wwlksm1edg  26835  wwlksnextproplem2  26873  clwlkclwwlklem2fv1  26961  clwlkclwwlklem2fv2  26962  clwlkclwwlklem2  26966  clwlkclwwlk2  26969  clwwisshclwwslem  26971  clwwlkf1  27012  clwwlkext2edg  27020  clwwlknonex2lem2  27083  numclwwlk7  27378  frgrreggt1  27380  frgrogt3nreg  27384  smcnlem  27680  nmoub3i  27756  blocnilem  27787  ubthlem2  27855  minvecolem4  27864  htthlem  27902  nmcexi  29013  nmopcoi  29082  stadd3i  29235  cdj1i  29420  nn0sqeq1  29641  nnmulge  29643  nndiffz1  29676  fzsplit3  29681  pmtrto1cl  29977  fzto1st1  29980  fzto1st  29981  psgnfzto1st  29983  1smat1  29998  submateqlem1  30001  madjusmdetlem2  30022  unitdivcld  30075  sqsscirc1  30082  nexple  30199  indf1o  30214  esumdivc  30273  dya2ub  30460  dya2iocress  30464  dya2iocbrsiga  30465  dya2icobrsiga  30466  dya2icoseg  30467  dya2iocucvr  30474  sxbrsigalem2  30476  fibp1  30591  probmeasb  30620  dstrvprob  30661  dstfrvunirn  30664  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemsgt1  30700  ballotlemsel1i  30702  ballotlemfrcn0  30719  signsply0  30756  itgexpif  30812  reprlt  30825  chtvalz  30835  breprexplemc  30838  breprexp  30839  circlemeth  30846  tgoldbachgnn  30865  subfaclim  31296  cvmliftlem2  31394  cvmliftlem13  31404  snmlff  31437  bccolsum  31751  faclim  31758  nn0prpwlem  32442  dnibndlem10  32602  dnibndlem12  32604  knoppcnlem4  32611  unblimceq0  32623  knoppndvlem1  32628  knoppndvlem2  32629  knoppndvlem3  32630  knoppndvlem7  32634  knoppndvlem11  32638  knoppndvlem12  32639  knoppndvlem14  32641  knoppndvlem15  32642  knoppndvlem17  32644  knoppndvlem18  32645  knoppndvlem20  32647  poimirlem6  33545  poimirlem7  33546  poimirlem15  33554  poimirlem19  33558  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  broucube  33573  itg2addnclem2  33592  itg2addnclem3  33593  areacirclem1  33630  areacirclem4  33633  incsequz  33674  totbndbnd  33718  bfplem2  33752  lzenom  37650  irrapxlem1  37703  irrapxlem2  37704  irrapxlem4  37706  irrapxlem5  37707  pellexlem2  37711  pell1qrge1  37751  pell1qr1  37752  elpell1qr2  37753  pell14qrgapw  37757  pellfundgt1  37764  pellfundglb  37766  pellfundex  37767  pellfundrp  37769  pellfundne1  37770  rmspecsqrtnq  37787  rmspecnonsq  37789  rmspecfund  37791  rmspecpos  37798  monotoddzzfi  37824  rmygeid  37848  areaquad  38119  imo72b2lem0  38782  imo72b2lem1  38788  imo72b2  38792  cvgdvgrat  38829  radcnvrat  38830  hashnzfzclim  38838  lhe4.4ex1a  38845  binomcxplemnn0  38865  binomcxplemdvbinom  38869  binomcxplemnotnn0  38872  oddfl  39803  abscosbd  39804  zltlesub  39811  abssinbd  39823  monoords  39825  fzisoeu  39828  fzdifsuc2  39838  suplesup  39868  xralrple2  39883  infxr  39896  infleinflem2  39900  reclt0d  39920  xrralrecnnge  39926  sqrlearg  40098  iooiinioc  40101  fmul01  40130  fmul01lt1lem1  40134  fmul01lt1lem2  40135  climsuselem1  40157  sumnnodd  40180  0ellimcdiv  40199  dvmptidg  40449  dvcosax  40459  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvxpaek  40473  dvnmul  40476  iblspltprt  40507  itgspltprt  40513  stoweidlem5  40540  stoweidlem7  40542  stoweidlem10  40545  stoweidlem11  40546  stoweidlem12  40547  stoweidlem13  40548  stoweidlem14  40549  stoweidlem16  40551  stoweidlem18  40553  stoweidlem20  40555  stoweidlem24  40559  stoweidlem25  40560  stoweidlem34  40569  stoweidlem36  40571  stoweidlem38  40573  stoweidlem40  40575  stoweidlem41  40576  stoweidlem42  40577  stoweidlem45  40580  stoweidlem51  40586  stoweidlem60  40595  wallispilem3  40602  wallispilem4  40603  wallispilem5  40604  wallispi  40605  wallispi2lem1  40606  wallispi2lem2  40607  wallispi2  40608  stirlinglem1  40609  stirlinglem3  40611  stirlinglem5  40613  stirlinglem6  40614  stirlinglem7  40615  stirlinglem8  40616  stirlinglem10  40618  stirlinglem11  40619  stirlinglem12  40620  stirlinglem13  40621  stirlinglem15  40623  dirker2re  40627  dirkerval2  40629  dirkerre  40630  dirkertrigeqlem1  40633  dirkertrigeqlem3  40635  dirkeritg  40637  dirkercncflem1  40638  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem5  40647  fourierdlem6  40648  fourierdlem11  40653  fourierdlem15  40657  fourierdlem19  40661  fourierdlem20  40662  fourierdlem24  40666  fourierdlem26  40668  fourierdlem28  40670  fourierdlem30  40672  fourierdlem39  40681  fourierdlem41  40683  fourierdlem43  40685  fourierdlem47  40688  fourierdlem48  40689  fourierdlem56  40697  fourierdlem60  40701  fourierdlem61  40702  fourierdlem62  40703  fourierdlem64  40705  fourierdlem65  40706  fourierdlem66  40707  fourierdlem68  40709  fourierdlem73  40714  fourierdlem78  40719  fourierdlem79  40720  fourierdlem87  40728  fourierdlem103  40744  fourierdlem104  40745  sqwvfoura  40763  fouriersw  40766  etransclem4  40773  etransclem23  40792  etransclem24  40793  etransclem31  40800  etransclem32  40801  etransclem35  40804  etransclem41  40810  etransclem46  40815  etransclem48  40817  etransc  40818  ioorrnopnxrlem  40844  nnfoctbdjlem  40990  iundjiun  40995  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133  ovnhoilem1  41136  vonioolem2  41216  vonicclem2  41219  pimrecltneg  41254  smfrec  41317  smfmullem1  41319  smfmullem2  41320  smfdiv  41325  sigaradd  41376  p1lep2  41639  zm1nn  41641  m1mod0mod1  41664  iccpartiltu  41683  iccpartlt  41685  iccpartgt  41688  pfx2  41737  fmtnoge3  41767  fmtnodvds  41781  fmtnoprmfac2lem1  41803  2pwp1prm  41828  flsqrt  41833  sfprmdvdsmersenne  41845  lighneallem2  41848  lighneallem4a  41850  proththdlem  41855  proththd  41856  nnoALTV  41931  bgoldbtbndlem4  42021  cznnring  42281  divge1b  42627  divgt1b  42628  m1modmmod  42641  difmodm1lt  42642  nn0eo  42647  regt1loggt0  42655  rege1logbrege0  42677  logblt1b  42683  fllog2  42687  nnolog2flm1  42709  dignn0flhalflem1  42734  reseccl  42822  recsccl  42823  amgmwlem  42876  amgmlemALT  42877
  Copyright terms: Public domain W3C validator