Theorem 1red 8194

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

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8031   1c1 8033

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

This theorem is referenced by:  recgt0  9030  ltrec  9063  recp1lt1  9079  peano5nni  9146  peano2nn  9155  nn0p1gt0  9431  nn0ge2m1nn  9462  peano2z  9515  suprzclex  9578  ledivge1le  9961  iccf1o  10239  zltaddlt1le  10242  fznatpl1  10311  elfz1b  10325  fzonn0p1p1  10459  elfzom1p1elfzo  10460  zssinfcl  10493  exbtwnzlemstep  10508  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2z  10515  qfraclt1  10541  flqaddz  10558  btwnzge0  10561  2tnp1ge0ge0  10562  flhalf  10563  fldiv4lem1div2uz2  10567  modqid  10612  m1modge3gt1  10634  modqltm1p1mod  10639  addmodlteq  10661  seq3f1olemqsumkj  10774  ltexp2a  10854  leexp2a  10855  leexp2r  10856  nnlesq  10906  bernneq3  10925  expnbnd  10926  expnlbnd2  10928  nn0ltexp2  10972  expcanlem  10978  expcan  10979  bcval5  11026  wrdlenge2n0  11153  cvg1nlemcau  11562  resqrexlem1arp  11583  resqrexlemf1  11586  resqrexlemover  11588  resqrexlemdecn  11590  resqrexlemlo  11591  resqrexlemcalc2  11593  resqrexlemnm  11596  resqrexlemga  11601  reccn2ap  11891  sumsnf  11988  expcnvre  12082  geolim  12090  geolim2  12091  georeclim  12092  geoisumr  12097  geoisum1c  12099  cvgratnnlembern  12102  cvgratnnlemsumlt  12107  cvgratnnlemfm  12108  cvgratnnlemrate  12109  cvgratnn  12110  cvgratz  12111  prodsnf  12171  fprodrecl  12187  fprodreclf  12193  efcllemp  12237  efgt1  12276  eflegeo  12280  sinltxirr  12340  eirraplem  12356  p1modz1  12373  oddge22np1  12460  ltoddhalfle  12472  nno  12485  nn0oddm1d2  12488  nnoddm1d2  12489  bitsfzolem  12533  bitsfzo  12534  bitsmod  12535  bitscmp  12537  bitsinv1lem  12540  uzwodc  12626  coprmgcdb  12678  prmind2  12710  dvdsnprmd  12715  prmdc  12720  isprm5lem  12731  znege1  12768  sqrt2irrap  12770  divdenle  12787  nn0sqrtelqelz  12796  difsqpwdvds  12929  fldivp1  12939  pcfaclem  12940  4sqlem11  12992  4sqlem12  12993  2expltfac  13030  oddennn  13031  exmidunben  13065  nninfdclemlt  13090  znidomb  14691  psrbaglesuppg  14705  hoverlt1  15392  ivthdichlem  15394  dveflem  15469  reeff1oleme  15515  reeff1o  15516  cosz12  15523  sin0pilem2  15525  cos02pilt1  15594  rplogcl  15622  logdivlti  15624  cxplt  15659  cxple  15660  ltexp2  15684  logbrec  15703  logbgt0b  15709  logbgcd1irr  15710  logbgcd1irraplemexp  15711  logbgcd1irraplemap  15712  mersenne  15740  perfectlem2  15743  zabsle1  15747  lgslem3  15750  lgsdirprm  15782  gausslemma2dlem1a  15806  lgseisen  15822  lgsquadlem2  15826  2sqlem8  15871  clwwlkext2edg  16292  clwwlknonex2lem2  16308  iooref1o  16689  trilpolemgt1  16694  trilpolemlt1  16696  trilpo  16698  redcwlpo  16711  neapmkvlem  16723  neapmkv  16724  taupi  16729  gsumgfsumlem  16735