Theorem 1red 7971

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

Syntax hints:   -> wi 4   e. wcel 2148   RRcr 7809   1c1 7811

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

This theorem is referenced by:  recgt0  8805  ltrec  8838  recp1lt1  8854  peano5nni  8920  peano2nn  8929  nn0p1gt0  9203  nn0ge2m1nn  9234  peano2z  9287  suprzclex  9349  ledivge1le  9724  iccf1o  10002  zltaddlt1le  10005  fznatpl1  10073  elfz1b  10087  fzonn0p1p1  10210  elfzom1p1elfzo  10211  exbtwnzlemstep  10245  exbtwnz  10248  rebtwn2zlemstep  10250  rebtwn2z  10252  qfraclt1  10277  flqaddz  10294  btwnzge0  10297  2tnp1ge0ge0  10298  flhalf  10299  modqid  10346  m1modge3gt1  10368  modqltm1p1mod  10373  addmodlteq  10395  seq3f1olemqsumkj  10495  ltexp2a  10569  leexp2a  10570  leexp2r  10571  nnlesq  10620  bernneq3  10639  expnbnd  10640  expnlbnd2  10642  nn0ltexp2  10685  expcanlem  10690  expcan  10691  bcval5  10738  cvg1nlemcau  10988  resqrexlem1arp  11009  resqrexlemf1  11012  resqrexlemover  11014  resqrexlemdecn  11016  resqrexlemlo  11017  resqrexlemcalc2  11019  resqrexlemnm  11022  resqrexlemga  11027  reccn2ap  11316  sumsnf  11412  expcnvre  11506  geolim  11514  geolim2  11515  georeclim  11516  geoisumr  11521  geoisum1c  11523  cvgratnnlembern  11526  cvgratnnlemsumlt  11531  cvgratnnlemfm  11532  cvgratnnlemrate  11533  cvgratnn  11534  cvgratz  11535  prodsnf  11595  fprodrecl  11611  fprodreclf  11617  efcllemp  11661  efgt1  11700  eflegeo  11704  eirraplem  11779  p1modz1  11796  oddge22np1  11880  ltoddhalfle  11892  nno  11905  nn0oddm1d2  11908  nnoddm1d2  11909  zssinfcl  11943  uzwodc  12032  coprmgcdb  12082  prmind2  12114  dvdsnprmd  12119  prmdc  12124  isprm5lem  12135  znege1  12172  sqrt2irrap  12174  divdenle  12191  nn0sqrtelqelz  12200  difsqpwdvds  12331  fldivp1  12340  pcfaclem  12341  oddennn  12387  exmidunben  12421  nninfdclemlt  12446  dveflem  14080  reeff1oleme  14086  reeff1o  14087  cosz12  14094  sin0pilem2  14096  cos02pilt1  14165  rplogcl  14193  logdivlti  14195  cxplt  14229  cxple  14230  ltexp2  14253  logbrec  14271  logbgt0b  14277  logbgcd1irr  14278  logbgcd1irraplemexp  14279  logbgcd1irraplemap  14280  zabsle1  14293  lgslem3  14296  lgsdirprm  14328  2sqlem8  14352  iooref1o  14664  trilpolemgt1  14669  trilpolemlt1  14671  trilpo  14673  redcwlpo  14685  neapmkvlem  14696  neapmkv  14697  taupi  14702