Theorem 1red 8086

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

Syntax hints:   -> wi 4   e. wcel 2175   RRcr 7923   1c1 7925

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

This theorem is referenced by:  recgt0  8922  ltrec  8955  recp1lt1  8971  peano5nni  9038  peano2nn  9047  nn0p1gt0  9323  nn0ge2m1nn  9354  peano2z  9407  suprzclex  9470  ledivge1le  9847  iccf1o  10125  zltaddlt1le  10128  fznatpl1  10197  elfz1b  10211  fzonn0p1p1  10340  elfzom1p1elfzo  10341  zssinfcl  10373  exbtwnzlemstep  10388  exbtwnz  10391  rebtwn2zlemstep  10393  rebtwn2z  10395  qfraclt1  10421  flqaddz  10438  btwnzge0  10441  2tnp1ge0ge0  10442  flhalf  10443  fldiv4lem1div2uz2  10447  modqid  10492  m1modge3gt1  10514  modqltm1p1mod  10519  addmodlteq  10541  seq3f1olemqsumkj  10654  ltexp2a  10734  leexp2a  10735  leexp2r  10736  nnlesq  10786  bernneq3  10805  expnbnd  10806  expnlbnd2  10808  nn0ltexp2  10852  expcanlem  10858  expcan  10859  bcval5  10906  wrdlenge2n0  11027  cvg1nlemcau  11266  resqrexlem1arp  11287  resqrexlemf1  11290  resqrexlemover  11292  resqrexlemdecn  11294  resqrexlemlo  11295  resqrexlemcalc2  11297  resqrexlemnm  11300  resqrexlemga  11305  reccn2ap  11595  sumsnf  11691  expcnvre  11785  geolim  11793  geolim2  11794  georeclim  11795  geoisumr  11800  geoisum1c  11802  cvgratnnlembern  11805  cvgratnnlemsumlt  11810  cvgratnnlemfm  11811  cvgratnnlemrate  11812  cvgratnn  11813  cvgratz  11814  prodsnf  11874  fprodrecl  11890  fprodreclf  11896  efcllemp  11940  efgt1  11979  eflegeo  11983  sinltxirr  12043  eirraplem  12059  p1modz1  12076  oddge22np1  12163  ltoddhalfle  12175  nno  12188  nn0oddm1d2  12191  nnoddm1d2  12192  bitsfzolem  12236  bitsfzo  12237  bitsmod  12238  bitscmp  12240  bitsinv1lem  12243  uzwodc  12329  coprmgcdb  12381  prmind2  12413  dvdsnprmd  12418  prmdc  12423  isprm5lem  12434  znege1  12471  sqrt2irrap  12473  divdenle  12490  nn0sqrtelqelz  12499  difsqpwdvds  12632  fldivp1  12642  pcfaclem  12643  4sqlem11  12695  4sqlem12  12696  2expltfac  12733  oddennn  12734  exmidunben  12768  nninfdclemlt  12793  znidomb  14391  psrbaglesuppg  14405  hoverlt1  15092  ivthdichlem  15094  dveflem  15169  reeff1oleme  15215  reeff1o  15216  cosz12  15223  sin0pilem2  15225  cos02pilt1  15294  rplogcl  15322  logdivlti  15324  cxplt  15359  cxple  15360  ltexp2  15384  logbrec  15403  logbgt0b  15409  logbgcd1irr  15410  logbgcd1irraplemexp  15411  logbgcd1irraplemap  15412  mersenne  15440  perfectlem2  15443  zabsle1  15447  lgslem3  15450  lgsdirprm  15482  gausslemma2dlem1a  15506  lgseisen  15522  lgsquadlem2  15526  2sqlem8  15571  iooref1o  15935  trilpolemgt1  15940  trilpolemlt1  15942  trilpo  15944  redcwlpo  15956  neapmkvlem  15968  neapmkv  15969  taupi  15974