Theorem 1red 8193

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

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8030   1c1 8032

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

This theorem is referenced by:  recgt0  9029  ltrec  9062  recp1lt1  9078  peano5nni  9145  peano2nn  9154  nn0p1gt0  9430  nn0ge2m1nn  9461  peano2z  9514  suprzclex  9577  ledivge1le  9960  iccf1o  10238  zltaddlt1le  10241  fznatpl1  10310  elfz1b  10324  fzonn0p1p1  10457  elfzom1p1elfzo  10458  zssinfcl  10491  exbtwnzlemstep  10506  exbtwnz  10509  rebtwn2zlemstep  10511  rebtwn2z  10513  qfraclt1  10539  flqaddz  10556  btwnzge0  10559  2tnp1ge0ge0  10560  flhalf  10561  fldiv4lem1div2uz2  10565  modqid  10610  m1modge3gt1  10632  modqltm1p1mod  10637  addmodlteq  10659  seq3f1olemqsumkj  10772  ltexp2a  10852  leexp2a  10853  leexp2r  10854  nnlesq  10904  bernneq3  10923  expnbnd  10924  expnlbnd2  10926  nn0ltexp2  10970  expcanlem  10976  expcan  10977  bcval5  11024  wrdlenge2n0  11148  cvg1nlemcau  11544  resqrexlem1arp  11565  resqrexlemf1  11568  resqrexlemover  11570  resqrexlemdecn  11572  resqrexlemlo  11573  resqrexlemcalc2  11575  resqrexlemnm  11578  resqrexlemga  11583  reccn2ap  11873  sumsnf  11969  expcnvre  12063  geolim  12071  geolim2  12072  georeclim  12073  geoisumr  12078  geoisum1c  12080  cvgratnnlembern  12083  cvgratnnlemsumlt  12088  cvgratnnlemfm  12089  cvgratnnlemrate  12090  cvgratnn  12091  cvgratz  12092  prodsnf  12152  fprodrecl  12168  fprodreclf  12174  efcllemp  12218  efgt1  12257  eflegeo  12261  sinltxirr  12321  eirraplem  12337  p1modz1  12354  oddge22np1  12441  ltoddhalfle  12453  nno  12466  nn0oddm1d2  12469  nnoddm1d2  12470  bitsfzolem  12514  bitsfzo  12515  bitsmod  12516  bitscmp  12518  bitsinv1lem  12521  uzwodc  12607  coprmgcdb  12659  prmind2  12691  dvdsnprmd  12696  prmdc  12701  isprm5lem  12712  znege1  12749  sqrt2irrap  12751  divdenle  12768  nn0sqrtelqelz  12777  difsqpwdvds  12910  fldivp1  12920  pcfaclem  12921  4sqlem11  12973  4sqlem12  12974  2expltfac  13011  oddennn  13012  exmidunben  13046  nninfdclemlt  13071  znidomb  14671  psrbaglesuppg  14685  hoverlt1  15372  ivthdichlem  15374  dveflem  15449  reeff1oleme  15495  reeff1o  15496  cosz12  15503  sin0pilem2  15505  cos02pilt1  15574  rplogcl  15602  logdivlti  15604  cxplt  15639  cxple  15640  ltexp2  15664  logbrec  15683  logbgt0b  15689  logbgcd1irr  15690  logbgcd1irraplemexp  15691  logbgcd1irraplemap  15692  mersenne  15720  perfectlem2  15723  zabsle1  15727  lgslem3  15730  lgsdirprm  15762  gausslemma2dlem1a  15786  lgseisen  15802  lgsquadlem2  15806  2sqlem8  15851  clwwlkext2edg  16272  clwwlknonex2lem2  16288  iooref1o  16638  trilpolemgt1  16643  trilpolemlt1  16645  trilpo  16647  redcwlpo  16659  neapmkvlem  16671  neapmkv  16672  taupi  16677  gsumgfsumlem  16683