Theorem 1red 8341

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 8325	. 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 8178   1c1 8180

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

This theorem is used by:  recgt0  9180  ltrec  9213  recp1lt1  9229  indfdc  9298  peano5nni  9307  peano2nn  9316  nn0p1gt0  9592  nn0ge2m1nn  9627  peano2z  9680  suprzclex  9744  ledivge1le  10127  lincmble  10406  iccf1o  10407  zltaddlt1le  10410  fznatpl1  10483  elfz1b  10497  fzonn0p1p1  10631  elfzom1p1elfzo  10632  zssinfcl  10665  exbtwnzlemstep  10682  exbtwnz  10685  rebtwn2zlemstep  10687  rebtwn2z  10689  qfraclt1  10715  flqaddz  10732  btwnzge0  10735  2tnp1ge0ge0  10736  flhalf  10737  fldiv4lem1div2uz2  10741  modqid  10786  m1modge3gt1  10808  modqltm1p1mod  10813  addmodlteq  10835  seq3f1olemqsumkj  10948  ltexp2a  11028  leexp2a  11029  leexp2r  11030  nnlesq  11080  resq01  11095  bernneq3  11100  expnbnd  11101  expnlbnd2  11103  nn0ltexp2  11147  expcanlem  11153  expcan  11154  bcval5  11201  ssenneg  11280  wrdlenge2n0  11340  sq01  11660  cvg1nlemcau  11750  resqrexlem1arp  11771  resqrexlemf1  11774  resqrexlemover  11776  resqrexlemdecn  11778  resqrexlemlo  11779  resqrexlemcalc2  11781  resqrexlemnm  11784  resqrexlemga  11789  reccn2ap  12079  sumsnf  12176  expcnvre  12270  geolim  12278  geolim2  12279  georeclim  12280  geoisumr  12285  geoisum1c  12287  cvgratnnlembern  12290  cvgratnnlemsumlt  12295  cvgratnnlemfm  12296  cvgratnnlemrate  12297  cvgratnn  12298  cvgratz  12299  prodsnf  12359  fprodrecl  12375  fprodreclf  12381  efcllemp  12425  efgt1  12464  eflegeo  12468  sinltxirr  12528  eirraplem  12544  p1modz1  12561  oddge22np1  12648  ltoddhalfle  12660  nno  12673  nn0oddm1d2  12676  nnoddm1d2  12677  bitsfzolem  12721  bitsfzo  12722  bitsmod  12723  bitscmp  12725  bitsinv1lem  12728  uzwodc  12814  coprmgcdb  12866  prmind2  12898  dvdsnprmd  12903  prmdc  12908  isprm5lem  12919  znege1  12956  sqrt2irrap  12958  divdenle  12975  nn0sqrtelqelz  12984  difsqpwdvds  13117  fldivp1  13127  pcfaclem  13128  4sqlem11  13180  4sqlem12  13181  2expltfac  13218  ballotfilemsgt1  13254  ballotfilemsel1i  13256  ballotfilemfrcn0  13273  oddennn  13283  exmidunben  13317  nninfdclemlt  13342  gzsumshift  14149  znidomb  14993  psrbaglesuppg  15057  hoverlt1  15750  ivthdichlem  15752  dveflem  15827  reeff1oleme  15873  reeff1o  15874  cosz12  15881  sin0pilem2  15883  cos02pilt1  15952  rplogcl  15980  logdivlti  15982  cxplt  16018  cxple  16019  ltexp2  16043  logbrec  16062  logbgt0b  16068  logbgcd1irr  16069  logbgcd1irraplemexp  16070  logbgcd1irraplemap  16071  log2tlbndlog2  16082  birthdaylem3  16089  pellexlem2  16092  mersenne  16111  perfectlem2  16114  zabsle1  16118  lgslem3  16121  lgsdirprm  16153  gausslemma2dlem1a  16177  lgseisen  16193  lgsquadlem2  16197  2sqlem8  16242  clwwlkext2edg  16663  clwwlknonex2lem2  16679  iooref1o  17083  trilpolemgt1  17088  trilpolemlt1  17090  trilpo  17092  redcwlpo  17105  neapmkvlem  17117  neapmkv  17118  taupi  17123