Theorem 1red 7972

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

Syntax hints:   -> wi 4   e. wcel 2148   RRcr 7810   1c1 7812

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

This theorem is referenced by:  recgt0  8807  ltrec  8840  recp1lt1  8856  peano5nni  8922  peano2nn  8931  nn0p1gt0  9205  nn0ge2m1nn  9236  peano2z  9289  suprzclex  9351  ledivge1le  9726  iccf1o  10004  zltaddlt1le  10007  fznatpl1  10076  elfz1b  10090  fzonn0p1p1  10213  elfzom1p1elfzo  10214  exbtwnzlemstep  10248  exbtwnz  10251  rebtwn2zlemstep  10253  rebtwn2z  10255  qfraclt1  10280  flqaddz  10297  btwnzge0  10300  2tnp1ge0ge0  10301  flhalf  10302  modqid  10349  m1modge3gt1  10371  modqltm1p1mod  10376  addmodlteq  10398  seq3f1olemqsumkj  10498  ltexp2a  10572  leexp2a  10573  leexp2r  10574  nnlesq  10624  bernneq3  10643  expnbnd  10644  expnlbnd2  10646  nn0ltexp2  10689  expcanlem  10695  expcan  10696  bcval5  10743  cvg1nlemcau  10993  resqrexlem1arp  11014  resqrexlemf1  11017  resqrexlemover  11019  resqrexlemdecn  11021  resqrexlemlo  11022  resqrexlemcalc2  11024  resqrexlemnm  11027  resqrexlemga  11032  reccn2ap  11321  sumsnf  11417  expcnvre  11511  geolim  11519  geolim2  11520  georeclim  11521  geoisumr  11526  geoisum1c  11528  cvgratnnlembern  11531  cvgratnnlemsumlt  11536  cvgratnnlemfm  11537  cvgratnnlemrate  11538  cvgratnn  11539  cvgratz  11540  prodsnf  11600  fprodrecl  11616  fprodreclf  11622  efcllemp  11666  efgt1  11705  eflegeo  11709  eirraplem  11784  p1modz1  11801  oddge22np1  11886  ltoddhalfle  11898  nno  11911  nn0oddm1d2  11914  nnoddm1d2  11915  zssinfcl  11949  uzwodc  12038  coprmgcdb  12088  prmind2  12120  dvdsnprmd  12125  prmdc  12130  isprm5lem  12141  znege1  12178  sqrt2irrap  12180  divdenle  12197  nn0sqrtelqelz  12206  difsqpwdvds  12337  fldivp1  12346  pcfaclem  12347  oddennn  12393  exmidunben  12427  nninfdclemlt  12452  dveflem  14190  reeff1oleme  14196  reeff1o  14197  cosz12  14204  sin0pilem2  14206  cos02pilt1  14275  rplogcl  14303  logdivlti  14305  cxplt  14339  cxple  14340  ltexp2  14363  logbrec  14381  logbgt0b  14387  logbgcd1irr  14388  logbgcd1irraplemexp  14389  logbgcd1irraplemap  14390  zabsle1  14403  lgslem3  14406  lgsdirprm  14438  2sqlem8  14473  iooref1o  14785  trilpolemgt1  14790  trilpolemlt1  14792  trilpo  14794  redcwlpo  14806  neapmkvlem  14817  neapmkv  14818  taupi  14823