Theorem 1red 8305

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

Syntax hints:   -> wi 4   e. wcel 2205   RRcr 8142   1c1 8144

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

This theorem is referenced by:  recgt0  9141  ltrec  9174  recp1lt1  9190  peano5nni  9257  peano2nn  9266  nn0p1gt0  9542  nn0ge2m1nn  9577  peano2z  9630  suprzclex  9694  ledivge1le  10077  lincmble  10356  iccf1o  10357  zltaddlt1le  10360  fznatpl1  10432  elfz1b  10446  fzonn0p1p1  10580  elfzom1p1elfzo  10581  zssinfcl  10614  exbtwnzlemstep  10631  exbtwnz  10634  rebtwn2zlemstep  10636  rebtwn2z  10638  qfraclt1  10664  flqaddz  10681  btwnzge0  10684  2tnp1ge0ge0  10685  flhalf  10686  fldiv4lem1div2uz2  10690  modqid  10735  m1modge3gt1  10757  modqltm1p1mod  10762  addmodlteq  10784  seq3f1olemqsumkj  10897  ltexp2a  10977  leexp2a  10978  leexp2r  10979  nnlesq  11029  resq01  11044  bernneq3  11049  expnbnd  11050  expnlbnd2  11052  nn0ltexp2  11096  expcanlem  11102  expcan  11103  bcval5  11150  ssenneg  11229  wrdlenge2n0  11285  cvg1nlemcau  11694  resqrexlem1arp  11715  resqrexlemf1  11718  resqrexlemover  11720  resqrexlemdecn  11722  resqrexlemlo  11723  resqrexlemcalc2  11725  resqrexlemnm  11728  resqrexlemga  11733  reccn2ap  12023  sumsnf  12120  expcnvre  12214  geolim  12222  geolim2  12223  georeclim  12224  geoisumr  12229  geoisum1c  12231  cvgratnnlembern  12234  cvgratnnlemsumlt  12239  cvgratnnlemfm  12240  cvgratnnlemrate  12241  cvgratnn  12242  cvgratz  12243  prodsnf  12303  fprodrecl  12319  fprodreclf  12325  efcllemp  12369  efgt1  12408  eflegeo  12412  sinltxirr  12472  eirraplem  12488  p1modz1  12505  oddge22np1  12592  ltoddhalfle  12604  nno  12617  nn0oddm1d2  12620  nnoddm1d2  12621  bitsfzolem  12665  bitsfzo  12666  bitsmod  12667  bitscmp  12669  bitsinv1lem  12672  uzwodc  12758  coprmgcdb  12810  prmind2  12842  dvdsnprmd  12847  prmdc  12852  isprm5lem  12863  znege1  12900  sqrt2irrap  12902  divdenle  12919  nn0sqrtelqelz  12928  difsqpwdvds  13061  fldivp1  13071  pcfaclem  13072  4sqlem11  13124  4sqlem12  13125  2expltfac  13162  ballotfilemsgt1  13198  ballotfilemsel1i  13200  ballotfilemfrcn0  13217  oddennn  13227  exmidunben  13261  nninfdclemlt  13286  gsumshift  14105  znidomb  14932  psrbaglesuppg  14947  hoverlt1  15640  ivthdichlem  15642  dveflem  15717  reeff1oleme  15763  reeff1o  15764  cosz12  15771  sin0pilem2  15773  cos02pilt1  15842  rplogcl  15870  logdivlti  15872  cxplt  15907  cxple  15908  ltexp2  15932  logbrec  15951  logbgt0b  15957  logbgcd1irr  15958  logbgcd1irraplemexp  15959  logbgcd1irraplemap  15960  pellexlem2  15972  mersenne  15991  perfectlem2  15994  zabsle1  15998  lgslem3  16001  lgsdirprm  16033  gausslemma2dlem1a  16057  lgseisen  16073  lgsquadlem2  16077  2sqlem8  16122  clwwlkext2edg  16543  clwwlknonex2lem2  16559  iooref1o  16944  trilpolemgt1  16949  trilpolemlt1  16951  trilpo  16953  redcwlpo  16966  neapmkvlem  16979  neapmkv  16980  taupi  16985