Theorem 1red 8237

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

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8074   1c1 8076

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

This theorem is referenced by:  recgt0  9072  ltrec  9105  recp1lt1  9121  peano5nni  9188  peano2nn  9197  nn0p1gt0  9473  nn0ge2m1nn  9506  peano2z  9559  suprzclex  9622  ledivge1le  10005  lincmble  10283  iccf1o  10284  zltaddlt1le  10287  fznatpl1  10356  elfz1b  10370  fzonn0p1p1  10504  elfzom1p1elfzo  10505  zssinfcl  10538  exbtwnzlemstep  10553  exbtwnz  10556  rebtwn2zlemstep  10558  rebtwn2z  10560  qfraclt1  10586  flqaddz  10603  btwnzge0  10606  2tnp1ge0ge0  10607  flhalf  10608  fldiv4lem1div2uz2  10612  modqid  10657  m1modge3gt1  10679  modqltm1p1mod  10684  addmodlteq  10706  seq3f1olemqsumkj  10819  ltexp2a  10899  leexp2a  10900  leexp2r  10901  nnlesq  10951  bernneq3  10970  expnbnd  10971  expnlbnd2  10973  nn0ltexp2  11017  expcanlem  11023  expcan  11024  bcval5  11071  wrdlenge2n0  11198  cvg1nlemcau  11607  resqrexlem1arp  11628  resqrexlemf1  11631  resqrexlemover  11633  resqrexlemdecn  11635  resqrexlemlo  11636  resqrexlemcalc2  11638  resqrexlemnm  11641  resqrexlemga  11646  reccn2ap  11936  sumsnf  12033  expcnvre  12127  geolim  12135  geolim2  12136  georeclim  12137  geoisumr  12142  geoisum1c  12144  cvgratnnlembern  12147  cvgratnnlemsumlt  12152  cvgratnnlemfm  12153  cvgratnnlemrate  12154  cvgratnn  12155  cvgratz  12156  prodsnf  12216  fprodrecl  12232  fprodreclf  12238  efcllemp  12282  efgt1  12321  eflegeo  12325  sinltxirr  12385  eirraplem  12401  p1modz1  12418  oddge22np1  12505  ltoddhalfle  12517  nno  12530  nn0oddm1d2  12533  nnoddm1d2  12534  bitsfzolem  12578  bitsfzo  12579  bitsmod  12580  bitscmp  12582  bitsinv1lem  12585  uzwodc  12671  coprmgcdb  12723  prmind2  12755  dvdsnprmd  12760  prmdc  12765  isprm5lem  12776  znege1  12813  sqrt2irrap  12815  divdenle  12832  nn0sqrtelqelz  12841  difsqpwdvds  12974  fldivp1  12984  pcfaclem  12985  4sqlem11  13037  4sqlem12  13038  2expltfac  13075  oddennn  13076  exmidunben  13110  nninfdclemlt  13135  znidomb  14737  psrbaglesuppg  14751  hoverlt1  15443  ivthdichlem  15445  dveflem  15520  reeff1oleme  15566  reeff1o  15567  cosz12  15574  sin0pilem2  15576  cos02pilt1  15645  rplogcl  15673  logdivlti  15675  cxplt  15710  cxple  15711  ltexp2  15735  logbrec  15754  logbgt0b  15760  logbgcd1irr  15761  logbgcd1irraplemexp  15762  logbgcd1irraplemap  15763  pellexlem2  15775  mersenne  15794  perfectlem2  15797  zabsle1  15801  lgslem3  15804  lgsdirprm  15836  gausslemma2dlem1a  15860  lgseisen  15876  lgsquadlem2  15880  2sqlem8  15925  clwwlkext2edg  16346  clwwlknonex2lem2  16362  iooref1o  16749  trilpolemgt1  16754  trilpolemlt1  16756  trilpo  16758  redcwlpo  16771  neapmkvlem  16783  neapmkv  16784  taupi  16789  gsumgfsumlem  16795