Theorem 1red 8122

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

Syntax hints:   -> wi 4   e. wcel 2178   RRcr 7959   1c1 7961

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

This theorem is referenced by:  recgt0  8958  ltrec  8991  recp1lt1  9007  peano5nni  9074  peano2nn  9083  nn0p1gt0  9359  nn0ge2m1nn  9390  peano2z  9443  suprzclex  9506  ledivge1le  9883  iccf1o  10161  zltaddlt1le  10164  fznatpl1  10233  elfz1b  10247  fzonn0p1p1  10379  elfzom1p1elfzo  10380  zssinfcl  10412  exbtwnzlemstep  10427  exbtwnz  10430  rebtwn2zlemstep  10432  rebtwn2z  10434  qfraclt1  10460  flqaddz  10477  btwnzge0  10480  2tnp1ge0ge0  10481  flhalf  10482  fldiv4lem1div2uz2  10486  modqid  10531  m1modge3gt1  10553  modqltm1p1mod  10558  addmodlteq  10580  seq3f1olemqsumkj  10693  ltexp2a  10773  leexp2a  10774  leexp2r  10775  nnlesq  10825  bernneq3  10844  expnbnd  10845  expnlbnd2  10847  nn0ltexp2  10891  expcanlem  10897  expcan  10898  bcval5  10945  wrdlenge2n0  11066  cvg1nlemcau  11410  resqrexlem1arp  11431  resqrexlemf1  11434  resqrexlemover  11436  resqrexlemdecn  11438  resqrexlemlo  11439  resqrexlemcalc2  11441  resqrexlemnm  11444  resqrexlemga  11449  reccn2ap  11739  sumsnf  11835  expcnvre  11929  geolim  11937  geolim2  11938  georeclim  11939  geoisumr  11944  geoisum1c  11946  cvgratnnlembern  11949  cvgratnnlemsumlt  11954  cvgratnnlemfm  11955  cvgratnnlemrate  11956  cvgratnn  11957  cvgratz  11958  prodsnf  12018  fprodrecl  12034  fprodreclf  12040  efcllemp  12084  efgt1  12123  eflegeo  12127  sinltxirr  12187  eirraplem  12203  p1modz1  12220  oddge22np1  12307  ltoddhalfle  12319  nno  12332  nn0oddm1d2  12335  nnoddm1d2  12336  bitsfzolem  12380  bitsfzo  12381  bitsmod  12382  bitscmp  12384  bitsinv1lem  12387  uzwodc  12473  coprmgcdb  12525  prmind2  12557  dvdsnprmd  12562  prmdc  12567  isprm5lem  12578  znege1  12615  sqrt2irrap  12617  divdenle  12634  nn0sqrtelqelz  12643  difsqpwdvds  12776  fldivp1  12786  pcfaclem  12787  4sqlem11  12839  4sqlem12  12840  2expltfac  12877  oddennn  12878  exmidunben  12912  nninfdclemlt  12937  znidomb  14535  psrbaglesuppg  14549  hoverlt1  15236  ivthdichlem  15238  dveflem  15313  reeff1oleme  15359  reeff1o  15360  cosz12  15367  sin0pilem2  15369  cos02pilt1  15438  rplogcl  15466  logdivlti  15468  cxplt  15503  cxple  15504  ltexp2  15528  logbrec  15547  logbgt0b  15553  logbgcd1irr  15554  logbgcd1irraplemexp  15555  logbgcd1irraplemap  15556  mersenne  15584  perfectlem2  15587  zabsle1  15591  lgslem3  15594  lgsdirprm  15626  gausslemma2dlem1a  15650  lgseisen  15666  lgsquadlem2  15670  2sqlem8  15715  iooref1o  16175  trilpolemgt1  16180  trilpolemlt1  16182  trilpo  16184  redcwlpo  16196  neapmkvlem  16208  neapmkv  16209  taupi  16214