Theorem 1red 8184

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 8168	. 2 |- 1 e. RR
2	1	a1i 9	1 |- ( ph -> 1 e. RR )

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 8021   1c1 8023

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

This theorem is referenced by:  recgt0  9020  ltrec  9053  recp1lt1  9069  peano5nni  9136  peano2nn  9145  nn0p1gt0  9421  nn0ge2m1nn  9452  peano2z  9505  suprzclex  9568  ledivge1le  9951  iccf1o  10229  zltaddlt1le  10232  fznatpl1  10301  elfz1b  10315  fzonn0p1p1  10448  elfzom1p1elfzo  10449  zssinfcl  10482  exbtwnzlemstep  10497  exbtwnz  10500  rebtwn2zlemstep  10502  rebtwn2z  10504  qfraclt1  10530  flqaddz  10547  btwnzge0  10550  2tnp1ge0ge0  10551  flhalf  10552  fldiv4lem1div2uz2  10556  modqid  10601  m1modge3gt1  10623  modqltm1p1mod  10628  addmodlteq  10650  seq3f1olemqsumkj  10763  ltexp2a  10843  leexp2a  10844  leexp2r  10845  nnlesq  10895  bernneq3  10914  expnbnd  10915  expnlbnd2  10917  nn0ltexp2  10961  expcanlem  10967  expcan  10968  bcval5  11015  wrdlenge2n0  11139  cvg1nlemcau  11535  resqrexlem1arp  11556  resqrexlemf1  11559  resqrexlemover  11561  resqrexlemdecn  11563  resqrexlemlo  11564  resqrexlemcalc2  11566  resqrexlemnm  11569  resqrexlemga  11574  reccn2ap  11864  sumsnf  11960  expcnvre  12054  geolim  12062  geolim2  12063  georeclim  12064  geoisumr  12069  geoisum1c  12071  cvgratnnlembern  12074  cvgratnnlemsumlt  12079  cvgratnnlemfm  12080  cvgratnnlemrate  12081  cvgratnn  12082  cvgratz  12083  prodsnf  12143  fprodrecl  12159  fprodreclf  12165  efcllemp  12209  efgt1  12248  eflegeo  12252  sinltxirr  12312  eirraplem  12328  p1modz1  12345  oddge22np1  12432  ltoddhalfle  12444  nno  12457  nn0oddm1d2  12460  nnoddm1d2  12461  bitsfzolem  12505  bitsfzo  12506  bitsmod  12507  bitscmp  12509  bitsinv1lem  12512  uzwodc  12598  coprmgcdb  12650  prmind2  12682  dvdsnprmd  12687  prmdc  12692  isprm5lem  12703  znege1  12740  sqrt2irrap  12742  divdenle  12759  nn0sqrtelqelz  12768  difsqpwdvds  12901  fldivp1  12911  pcfaclem  12912  4sqlem11  12964  4sqlem12  12965  2expltfac  13002  oddennn  13003  exmidunben  13037  nninfdclemlt  13062  znidomb  14662  psrbaglesuppg  14676  hoverlt1  15363  ivthdichlem  15365  dveflem  15440  reeff1oleme  15486  reeff1o  15487  cosz12  15494  sin0pilem2  15496  cos02pilt1  15565  rplogcl  15593  logdivlti  15595  cxplt  15630  cxple  15631  ltexp2  15655  logbrec  15674  logbgt0b  15680  logbgcd1irr  15681  logbgcd1irraplemexp  15682  logbgcd1irraplemap  15683  mersenne  15711  perfectlem2  15714  zabsle1  15718  lgslem3  15721  lgsdirprm  15753  gausslemma2dlem1a  15777  lgseisen  15793  lgsquadlem2  15797  2sqlem8  15842  clwwlkext2edg  16217  clwwlknonex2lem2  16233  iooref1o  16574  trilpolemgt1  16579  trilpolemlt1  16581  trilpo  16583  redcwlpo  16595  neapmkvlem  16607  neapmkv  16608  taupi  16613