Theorem 1red 7910

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

Syntax hints:   -> wi 4   e. wcel 2136   RRcr 7748   1c1 7750

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

This theorem is referenced by:  recgt0  8741  ltrec  8774  recp1lt1  8790  peano5nni  8856  peano2nn  8865  nn0p1gt0  9139  nn0ge2m1nn  9170  peano2z  9223  suprzclex  9285  ledivge1le  9658  iccf1o  9936  zltaddlt1le  9939  fznatpl1  10007  elfz1b  10021  fzonn0p1p1  10144  elfzom1p1elfzo  10145  exbtwnzlemstep  10179  exbtwnz  10182  rebtwn2zlemstep  10184  rebtwn2z  10186  qfraclt1  10211  flqaddz  10228  btwnzge0  10231  2tnp1ge0ge0  10232  flhalf  10233  modqid  10280  m1modge3gt1  10302  modqltm1p1mod  10307  addmodlteq  10329  seq3f1olemqsumkj  10429  ltexp2a  10503  leexp2a  10504  leexp2r  10505  nnlesq  10554  bernneq3  10573  expnbnd  10574  expnlbnd2  10576  nn0ltexp2  10619  expcanlem  10624  expcan  10625  bcval5  10672  cvg1nlemcau  10922  resqrexlem1arp  10943  resqrexlemf1  10946  resqrexlemover  10948  resqrexlemdecn  10950  resqrexlemlo  10951  resqrexlemcalc2  10953  resqrexlemnm  10956  resqrexlemga  10961  reccn2ap  11250  sumsnf  11346  expcnvre  11440  geolim  11448  geolim2  11449  georeclim  11450  geoisumr  11455  geoisum1c  11457  cvgratnnlembern  11460  cvgratnnlemsumlt  11465  cvgratnnlemfm  11466  cvgratnnlemrate  11467  cvgratnn  11468  cvgratz  11469  prodsnf  11529  fprodrecl  11545  fprodreclf  11551  efcllemp  11595  efgt1  11634  eflegeo  11638  eirraplem  11713  p1modz1  11730  oddge22np1  11814  ltoddhalfle  11826  nno  11839  nn0oddm1d2  11842  nnoddm1d2  11843  zssinfcl  11877  uzwodc  11966  coprmgcdb  12016  prmind2  12048  dvdsnprmd  12053  prmdc  12058  isprm5lem  12069  znege1  12106  sqrt2irrap  12108  divdenle  12125  nn0sqrtelqelz  12134  difsqpwdvds  12265  fldivp1  12274  pcfaclem  12275  oddennn  12321  exmidunben  12355  nninfdclemlt  12380  dveflem  13287  reeff1oleme  13293  reeff1o  13294  cosz12  13301  sin0pilem2  13303  cos02pilt1  13372  rplogcl  13400  logdivlti  13402  cxplt  13436  cxple  13437  ltexp2  13460  logbrec  13478  logbgt0b  13484  logbgcd1irr  13485  logbgcd1irraplemexp  13486  logbgcd1irraplemap  13487  zabsle1  13500  lgslem3  13503  lgsdirprm  13535  2sqlem8  13559  iooref1o  13873  trilpolemgt1  13878  trilpolemlt1  13880  trilpo  13882  redcwlpo  13894  neapmkvlem  13905  neapmkv  13906  taupi  13909