Theorem 1red 8034

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

Syntax hints:   -> wi 4   e. wcel 2164   RRcr 7871   1c1 7873

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

This theorem is referenced by:  recgt0  8869  ltrec  8902  recp1lt1  8918  peano5nni  8985  peano2nn  8994  nn0p1gt0  9269  nn0ge2m1nn  9300  peano2z  9353  suprzclex  9415  ledivge1le  9792  iccf1o  10070  zltaddlt1le  10073  fznatpl1  10142  elfz1b  10156  fzonn0p1p1  10280  elfzom1p1elfzo  10281  exbtwnzlemstep  10316  exbtwnz  10319  rebtwn2zlemstep  10321  rebtwn2z  10323  qfraclt1  10349  flqaddz  10366  btwnzge0  10369  2tnp1ge0ge0  10370  flhalf  10371  fldiv4lem1div2uz2  10375  modqid  10420  m1modge3gt1  10442  modqltm1p1mod  10447  addmodlteq  10469  seq3f1olemqsumkj  10582  ltexp2a  10662  leexp2a  10663  leexp2r  10664  nnlesq  10714  bernneq3  10733  expnbnd  10734  expnlbnd2  10736  nn0ltexp2  10780  expcanlem  10786  expcan  10787  bcval5  10834  wrdlenge2n0  10949  cvg1nlemcau  11128  resqrexlem1arp  11149  resqrexlemf1  11152  resqrexlemover  11154  resqrexlemdecn  11156  resqrexlemlo  11157  resqrexlemcalc2  11159  resqrexlemnm  11162  resqrexlemga  11167  reccn2ap  11456  sumsnf  11552  expcnvre  11646  geolim  11654  geolim2  11655  georeclim  11656  geoisumr  11661  geoisum1c  11663  cvgratnnlembern  11666  cvgratnnlemsumlt  11671  cvgratnnlemfm  11672  cvgratnnlemrate  11673  cvgratnn  11674  cvgratz  11675  prodsnf  11735  fprodrecl  11751  fprodreclf  11757  efcllemp  11801  efgt1  11840  eflegeo  11844  sinltxirr  11904  eirraplem  11920  p1modz1  11937  oddge22np1  12022  ltoddhalfle  12034  nno  12047  nn0oddm1d2  12050  nnoddm1d2  12051  zssinfcl  12085  uzwodc  12174  coprmgcdb  12226  prmind2  12258  dvdsnprmd  12263  prmdc  12268  isprm5lem  12279  znege1  12316  sqrt2irrap  12318  divdenle  12335  nn0sqrtelqelz  12344  difsqpwdvds  12476  fldivp1  12486  pcfaclem  12487  4sqlem11  12539  4sqlem12  12540  oddennn  12549  exmidunben  12583  nninfdclemlt  12608  znidomb  14146  psrbaglesuppg  14158  hoverlt1  14803  ivthdichlem  14805  dveflem  14872  reeff1oleme  14907  reeff1o  14908  cosz12  14915  sin0pilem2  14917  cos02pilt1  14986  rplogcl  15014  logdivlti  15016  cxplt  15050  cxple  15051  ltexp2  15074  logbrec  15092  logbgt0b  15098  logbgcd1irr  15099  logbgcd1irraplemexp  15100  logbgcd1irraplemap  15101  zabsle1  15115  lgslem3  15118  lgsdirprm  15150  gausslemma2dlem1a  15174  lgseisen  15190  2sqlem8  15210  iooref1o  15524  trilpolemgt1  15529  trilpolemlt1  15531  trilpo  15533  redcwlpo  15545  neapmkvlem  15557  neapmkv  15558  taupi  15563