Theorem 1red 8342

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   RRcr 8179   1c1 8181

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-1re 8274

This theorem is used by:  recgt0  9183  ltrec  9216  recp1lt1  9232  indfdc  9301  peano5nni  9310  peano2nn  9319  nn0p1gt0  9597  nn0ge2m1nn  9632  peano2z  9685  suprzclex  9749  ledivge1le  10138  lincmble  10417  iccf1o  10418  zltaddlt1le  10421  fznatpl1  10494  elfz1b  10508  fzonn0p1p1  10642  elfzom1p1elfzo  10643  zssinfcl  10676  exbtwnzlemstep  10693  exbtwnz  10696  rebtwn2zlemstep  10698  rebtwn2z  10700  qfraclt1  10728  flqaddz  10747  btwnzge0  10750  2tnp1ge0ge0  10751  flhalf  10752  fldiv4lem1div2uz2  10756  modqid  10801  m1modge3gt1  10823  modqltm1p1mod  10828  addmodlteq  10850  seq3f1olemqsumkj  10963  ltexp2a  11043  leexp2a  11044  leexp2r  11045  nnlesq  11095  resq01  11110  bernneq3  11115  expnbnd  11116  expnlbnd2  11118  nn0ltexp2  11163  expcanlem  11169  expcan  11170  bcval5  11217  ssenneg  11296  wrdlenge2n0  11356  sq01  11676  cvg1nlemcau  11766  resqrexlem1arp  11787  resqrexlemf1  11790  resqrexlemover  11792  resqrexlemdecn  11794  resqrexlemlo  11795  resqrexlemcalc2  11797  resqrexlemnm  11800  resqrexlemga  11805  reccn2ap  12098  sumsnf  12195  expcnvre  12289  geolim  12297  geolim2  12298  georeclim  12299  geoisumr  12304  geoisum1c  12306  cvgratnnlembern  12309  cvgratnnlemsumlt  12314  cvgratnnlemfm  12315  cvgratnnlemrate  12316  cvgratnn  12317  cvgratz  12318  prodsnf  12378  fprodrecl  12394  fprodreclf  12400  efcllemp  12444  efgt1  12483  eflegeo  12487  sinltxirr  12547  eirraplem  12563  p1modz1  12580  oddge22np1  12667  ltoddhalfle  12679  nno  12692  nn0oddm1d2  12695  nnoddm1d2  12696  bitsfzolem  12740  bitsfzo  12741  bitsmod  12742  bitscmp  12744  bitsinv1lem  12747  uzwodc  12833  coprmgcdb  12885  prmind2  12917  dvdsnprmd  12922  prmdc  12927  isprm5lem  12939  znege1  12977  sqrt2irrap  12979  divdenle  12996  nn0sqrtelqelz  13005  difsqpwdvds  13140  fldivp1  13150  pcfaclem  13151  4sqlem11  13203  4sqlem12  13204  2expltfac  13242  ballotfilemsgt1  13306  ballotfilemsel1i  13308  ballotfilemfrcn0  13325  oddennn  13335  exmidunben  13369  nninfdclemlt  13394  gzsumshift  14233  znidomb  15077  psrbaglesuppg  15141  hoverlt1  15841  ivthdichlem  15843  dveflem  15918  reeff1oleme  15964  reeff1o  15965  efap1p  15971  cosz12  15973  sin0pilem2  15975  cos02pilt1  16044  rplogcl  16073  logdivlti  16075  logdivlt  16088  cxplt  16113  cxple  16114  ltexp2  16138  logbrec  16157  logbgt0b  16163  logbgcd1irr  16164  logbgcd1irraplemexp  16165  logbgcd1irraplemap  16166  zprmlogbaplem1  16176  zprmlogbaplem2  16177  log2tlbndlog2  16181  birthdaylem3  16188  pellexlem2  16191  ppiqltx  16242  ppiqub  16254  chtqub  16257  mersenne  16258  perfectlem2  16261  bcmono  16265  bposlem1  16272  bposlem2  16273  zabsle1  16284  lgslem3  16287  lgsdirprm  16319  gausslemma2dlem1a  16343  lgseisen  16359  lgsquadlem2  16363  2sqlem8  16408  clwwlkext2edg  16829  clwwlknonex2lem2  16845  iooref1o  17249  trilpolemgt1  17255  trilpolemlt1  17257  trilpo  17259  redcwlpo  17272  neapmkvlem  17284  neapmkv  17285  taupi  17290