Theorem 1red 8289

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

Syntax hints:   -> wi 4   e. wcel 2203   RRcr 8126   1c1 8128

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

This theorem is referenced by:  recgt0  9124  ltrec  9157  recp1lt1  9173  peano5nni  9240  peano2nn  9249  nn0p1gt0  9525  nn0ge2m1nn  9560  peano2z  9613  suprzclex  9676  ledivge1le  10059  lincmble  10337  iccf1o  10338  zltaddlt1le  10341  fznatpl1  10410  elfz1b  10424  fzonn0p1p1  10558  elfzom1p1elfzo  10559  zssinfcl  10592  exbtwnzlemstep  10607  exbtwnz  10610  rebtwn2zlemstep  10612  rebtwn2z  10614  qfraclt1  10640  flqaddz  10657  btwnzge0  10660  2tnp1ge0ge0  10661  flhalf  10662  fldiv4lem1div2uz2  10666  modqid  10711  m1modge3gt1  10733  modqltm1p1mod  10738  addmodlteq  10760  seq3f1olemqsumkj  10873  ltexp2a  10953  leexp2a  10954  leexp2r  10955  nnlesq  11005  bernneq3  11024  expnbnd  11025  expnlbnd2  11027  nn0ltexp2  11071  expcanlem  11077  expcan  11078  bcval5  11125  ssenneg  11204  wrdlenge2n0  11260  cvg1nlemcau  11669  resqrexlem1arp  11690  resqrexlemf1  11693  resqrexlemover  11695  resqrexlemdecn  11697  resqrexlemlo  11698  resqrexlemcalc2  11700  resqrexlemnm  11703  resqrexlemga  11708  reccn2ap  11998  sumsnf  12095  expcnvre  12189  geolim  12197  geolim2  12198  georeclim  12199  geoisumr  12204  geoisum1c  12206  cvgratnnlembern  12209  cvgratnnlemsumlt  12214  cvgratnnlemfm  12215  cvgratnnlemrate  12216  cvgratnn  12217  cvgratz  12218  prodsnf  12278  fprodrecl  12294  fprodreclf  12300  efcllemp  12344  efgt1  12383  eflegeo  12387  sinltxirr  12447  eirraplem  12463  p1modz1  12480  oddge22np1  12567  ltoddhalfle  12579  nno  12592  nn0oddm1d2  12595  nnoddm1d2  12596  bitsfzolem  12640  bitsfzo  12641  bitsmod  12642  bitscmp  12644  bitsinv1lem  12647  uzwodc  12733  coprmgcdb  12785  prmind2  12817  dvdsnprmd  12822  prmdc  12827  isprm5lem  12838  znege1  12875  sqrt2irrap  12877  divdenle  12894  nn0sqrtelqelz  12903  difsqpwdvds  13036  fldivp1  13046  pcfaclem  13047  4sqlem11  13099  4sqlem12  13100  2expltfac  13137  oddennn  13143  exmidunben  13177  nninfdclemlt  13202  znidomb  14806  psrbaglesuppg  14821  hoverlt1  15514  ivthdichlem  15516  dveflem  15591  reeff1oleme  15637  reeff1o  15638  cosz12  15645  sin0pilem2  15647  cos02pilt1  15716  rplogcl  15744  logdivlti  15746  cxplt  15781  cxple  15782  ltexp2  15806  logbrec  15825  logbgt0b  15831  logbgcd1irr  15832  logbgcd1irraplemexp  15833  logbgcd1irraplemap  15834  pellexlem2  15846  mersenne  15865  perfectlem2  15868  zabsle1  15872  lgslem3  15875  lgsdirprm  15907  gausslemma2dlem1a  15931  lgseisen  15947  lgsquadlem2  15951  2sqlem8  15996  clwwlkext2edg  16417  clwwlknonex2lem2  16433  iooref1o  16818  trilpolemgt1  16823  trilpolemlt1  16825  trilpo  16827  redcwlpo  16840  neapmkvlem  16853  neapmkv  16854  taupi  16859  gsumgfsumlem  16865