Theorem 1red 8157

Description: 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
1red	|- ( ph -> 1 e. RR )

Proof of Theorem 1red

Step	Hyp	Ref	Expression
1		1re 8141	. 2 |- 1 e. RR
2	1	a1i 9	1 |- ( ph -> 1 e. RR )

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 7994   1c1 7996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1re 8089

This theorem is referenced by:  recgt0  8993  ltrec  9026  recp1lt1  9042  peano5nni  9109  peano2nn  9118  nn0p1gt0  9394  nn0ge2m1nn  9425  peano2z  9478  suprzclex  9541  ledivge1le  9918  iccf1o  10196  zltaddlt1le  10199  fznatpl1  10268  elfz1b  10282  fzonn0p1p1  10414  elfzom1p1elfzo  10415  zssinfcl  10447  exbtwnzlemstep  10462  exbtwnz  10465  rebtwn2zlemstep  10467  rebtwn2z  10469  qfraclt1  10495  flqaddz  10512  btwnzge0  10515  2tnp1ge0ge0  10516  flhalf  10517  fldiv4lem1div2uz2  10521  modqid  10566  m1modge3gt1  10588  modqltm1p1mod  10593  addmodlteq  10615  seq3f1olemqsumkj  10728  ltexp2a  10808  leexp2a  10809  leexp2r  10810  nnlesq  10860  bernneq3  10879  expnbnd  10880  expnlbnd2  10882  nn0ltexp2  10926  expcanlem  10932  expcan  10933  bcval5  10980  wrdlenge2n0  11102  cvg1nlemcau  11490  resqrexlem1arp  11511  resqrexlemf1  11514  resqrexlemover  11516  resqrexlemdecn  11518  resqrexlemlo  11519  resqrexlemcalc2  11521  resqrexlemnm  11524  resqrexlemga  11529  reccn2ap  11819  sumsnf  11915  expcnvre  12009  geolim  12017  geolim2  12018  georeclim  12019  geoisumr  12024  geoisum1c  12026  cvgratnnlembern  12029  cvgratnnlemsumlt  12034  cvgratnnlemfm  12035  cvgratnnlemrate  12036  cvgratnn  12037  cvgratz  12038  prodsnf  12098  fprodrecl  12114  fprodreclf  12120  efcllemp  12164  efgt1  12203  eflegeo  12207  sinltxirr  12267  eirraplem  12283  p1modz1  12300  oddge22np1  12387  ltoddhalfle  12399  nno  12412  nn0oddm1d2  12415  nnoddm1d2  12416  bitsfzolem  12460  bitsfzo  12461  bitsmod  12462  bitscmp  12464  bitsinv1lem  12467  uzwodc  12553  coprmgcdb  12605  prmind2  12637  dvdsnprmd  12642  prmdc  12647  isprm5lem  12658  znege1  12695  sqrt2irrap  12697  divdenle  12714  nn0sqrtelqelz  12723  difsqpwdvds  12856  fldivp1  12866  pcfaclem  12867  4sqlem11  12919  4sqlem12  12920  2expltfac  12957  oddennn  12958  exmidunben  12992  nninfdclemlt  13017  znidomb  14616  psrbaglesuppg  14630  hoverlt1  15317  ivthdichlem  15319  dveflem  15394  reeff1oleme  15440  reeff1o  15441  cosz12  15448  sin0pilem2  15450  cos02pilt1  15519  rplogcl  15547  logdivlti  15549  cxplt  15584  cxple  15585  ltexp2  15609  logbrec  15628  logbgt0b  15634  logbgcd1irr  15635  logbgcd1irraplemexp  15636  logbgcd1irraplemap  15637  mersenne  15665  perfectlem2  15668  zabsle1  15672  lgslem3  15675  lgsdirprm  15707  gausslemma2dlem1a  15731  lgseisen  15747  lgsquadlem2  15751  2sqlem8  15796  iooref1o  16361  trilpolemgt1  16366  trilpolemlt1  16368  trilpo  16370  redcwlpo  16382  neapmkvlem  16394  neapmkv  16395  taupi  16400