Theorem 1red 8331

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

Syntax hints:   -> wi 4   e. wcel 2209   RRcr 8168   1c1 8170

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

This theorem is referenced by:  recgt0  9170  ltrec  9203  recp1lt1  9219  peano5nni  9286  peano2nn  9295  nn0p1gt0  9571  nn0ge2m1nn  9606  peano2z  9659  suprzclex  9723  ledivge1le  10106  lincmble  10385  iccf1o  10386  zltaddlt1le  10389  fznatpl1  10461  elfz1b  10475  fzonn0p1p1  10609  elfzom1p1elfzo  10610  zssinfcl  10643  exbtwnzlemstep  10660  exbtwnz  10663  rebtwn2zlemstep  10665  rebtwn2z  10667  qfraclt1  10693  flqaddz  10710  btwnzge0  10713  2tnp1ge0ge0  10714  flhalf  10715  fldiv4lem1div2uz2  10719  modqid  10764  m1modge3gt1  10786  modqltm1p1mod  10791  addmodlteq  10813  seq3f1olemqsumkj  10926  ltexp2a  11006  leexp2a  11007  leexp2r  11008  nnlesq  11058  resq01  11073  bernneq3  11078  expnbnd  11079  expnlbnd2  11081  nn0ltexp2  11125  expcanlem  11131  expcan  11132  bcval5  11179  ssenneg  11258  wrdlenge2n0  11318  sq01  11638  cvg1nlemcau  11728  resqrexlem1arp  11749  resqrexlemf1  11752  resqrexlemover  11754  resqrexlemdecn  11756  resqrexlemlo  11757  resqrexlemcalc2  11759  resqrexlemnm  11762  resqrexlemga  11767  reccn2ap  12057  sumsnf  12154  expcnvre  12248  geolim  12256  geolim2  12257  georeclim  12258  geoisumr  12263  geoisum1c  12265  cvgratnnlembern  12268  cvgratnnlemsumlt  12273  cvgratnnlemfm  12274  cvgratnnlemrate  12275  cvgratnn  12276  cvgratz  12277  prodsnf  12337  fprodrecl  12353  fprodreclf  12359  efcllemp  12403  efgt1  12442  eflegeo  12446  sinltxirr  12506  eirraplem  12522  p1modz1  12539  oddge22np1  12626  ltoddhalfle  12638  nno  12651  nn0oddm1d2  12654  nnoddm1d2  12655  bitsfzolem  12699  bitsfzo  12700  bitsmod  12701  bitscmp  12703  bitsinv1lem  12706  uzwodc  12792  coprmgcdb  12844  prmind2  12876  dvdsnprmd  12881  prmdc  12886  isprm5lem  12897  znege1  12934  sqrt2irrap  12936  divdenle  12953  nn0sqrtelqelz  12962  difsqpwdvds  13095  fldivp1  13105  pcfaclem  13106  4sqlem11  13158  4sqlem12  13159  2expltfac  13196  ballotfilemsgt1  13232  ballotfilemsel1i  13234  ballotfilemfrcn0  13251  oddennn  13261  exmidunben  13295  nninfdclemlt  13320  gzsumshift  14126  znidomb  14965  psrbaglesuppg  14980  hoverlt1  15673  ivthdichlem  15675  dveflem  15750  reeff1oleme  15796  reeff1o  15797  cosz12  15804  sin0pilem2  15806  cos02pilt1  15875  rplogcl  15903  logdivlti  15905  cxplt  15941  cxple  15942  ltexp2  15966  logbrec  15985  logbgt0b  15991  logbgcd1irr  15992  logbgcd1irraplemexp  15993  logbgcd1irraplemap  15994  pellexlem2  16006  mersenne  16025  perfectlem2  16028  zabsle1  16032  lgslem3  16035  lgsdirprm  16067  gausslemma2dlem1a  16091  lgseisen  16107  lgsquadlem2  16111  2sqlem8  16156  clwwlkext2edg  16577  clwwlknonex2lem2  16593  iooref1o  16988  trilpolemgt1  16993  trilpolemlt1  16995  trilpo  16997  redcwlpo  17010  neapmkvlem  17022  neapmkv  17023  taupi  17028