Theorem 1red 8036

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

Syntax hints:   -> wi 4   e. wcel 2164   RRcr 7873   1c1 7875

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

This theorem is referenced by:  recgt0  8871  ltrec  8904  recp1lt1  8920  peano5nni  8987  peano2nn  8996  nn0p1gt0  9272  nn0ge2m1nn  9303  peano2z  9356  suprzclex  9418  ledivge1le  9795  iccf1o  10073  zltaddlt1le  10076  fznatpl1  10145  elfz1b  10159  fzonn0p1p1  10283  elfzom1p1elfzo  10284  exbtwnzlemstep  10319  exbtwnz  10322  rebtwn2zlemstep  10324  rebtwn2z  10326  qfraclt1  10352  flqaddz  10369  btwnzge0  10372  2tnp1ge0ge0  10373  flhalf  10374  fldiv4lem1div2uz2  10378  modqid  10423  m1modge3gt1  10445  modqltm1p1mod  10450  addmodlteq  10472  seq3f1olemqsumkj  10585  ltexp2a  10665  leexp2a  10666  leexp2r  10667  nnlesq  10717  bernneq3  10736  expnbnd  10737  expnlbnd2  10739  nn0ltexp2  10783  expcanlem  10789  expcan  10790  bcval5  10837  wrdlenge2n0  10952  cvg1nlemcau  11131  resqrexlem1arp  11152  resqrexlemf1  11155  resqrexlemover  11157  resqrexlemdecn  11159  resqrexlemlo  11160  resqrexlemcalc2  11162  resqrexlemnm  11165  resqrexlemga  11170  reccn2ap  11459  sumsnf  11555  expcnvre  11649  geolim  11657  geolim2  11658  georeclim  11659  geoisumr  11664  geoisum1c  11666  cvgratnnlembern  11669  cvgratnnlemsumlt  11674  cvgratnnlemfm  11675  cvgratnnlemrate  11676  cvgratnn  11677  cvgratz  11678  prodsnf  11738  fprodrecl  11754  fprodreclf  11760  efcllemp  11804  efgt1  11843  eflegeo  11847  sinltxirr  11907  eirraplem  11923  p1modz1  11940  oddge22np1  12025  ltoddhalfle  12037  nno  12050  nn0oddm1d2  12053  nnoddm1d2  12054  zssinfcl  12088  uzwodc  12177  coprmgcdb  12229  prmind2  12261  dvdsnprmd  12266  prmdc  12271  isprm5lem  12282  znege1  12319  sqrt2irrap  12321  divdenle  12338  nn0sqrtelqelz  12347  difsqpwdvds  12479  fldivp1  12489  pcfaclem  12490  4sqlem11  12542  4sqlem12  12543  oddennn  12552  exmidunben  12586  nninfdclemlt  12611  znidomb  14157  psrbaglesuppg  14169  hoverlt1  14828  ivthdichlem  14830  dveflem  14905  reeff1oleme  14948  reeff1o  14949  cosz12  14956  sin0pilem2  14958  cos02pilt1  15027  rplogcl  15055  logdivlti  15057  cxplt  15091  cxple  15092  ltexp2  15115  logbrec  15133  logbgt0b  15139  logbgcd1irr  15140  logbgcd1irraplemexp  15141  logbgcd1irraplemap  15142  zabsle1  15156  lgslem3  15159  lgsdirprm  15191  gausslemma2dlem1a  15215  lgseisen  15231  lgsquadlem2  15235  2sqlem8  15280  iooref1o  15594  trilpolemgt1  15599  trilpolemlt1  15601  trilpo  15603  redcwlpo  15615  neapmkvlem  15627  neapmkv  15628  taupi  15633