Theorem 1red 7781

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

Syntax hints:   -> wi 4   e. wcel 1480   RRcr 7619   1c1 7621

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

This theorem is referenced by:  recgt0  8608  ltrec  8641  recp1lt1  8657  peano5nni  8723  peano2nn  8732  nn0p1gt0  9006  nn0ge2m1nn  9037  peano2z  9090  suprzclex  9149  ledivge1le  9513  iccf1o  9787  zltaddlt1le  9789  fznatpl1  9856  elfz1b  9870  fzonn0p1p1  9990  elfzom1p1elfzo  9991  exbtwnzlemstep  10025  exbtwnz  10028  rebtwn2zlemstep  10030  rebtwn2z  10032  qfraclt1  10053  flqaddz  10070  btwnzge0  10073  2tnp1ge0ge0  10074  flhalf  10075  modqid  10122  m1modge3gt1  10144  modqltm1p1mod  10149  addmodlteq  10171  seq3f1olemqsumkj  10271  ltexp2a  10345  leexp2a  10346  leexp2r  10347  nnlesq  10396  bernneq3  10414  expnbnd  10415  expnlbnd2  10417  expcanlem  10462  expcan  10463  bcval5  10509  cvg1nlemcau  10756  resqrexlem1arp  10777  resqrexlemf1  10780  resqrexlemover  10782  resqrexlemdecn  10784  resqrexlemlo  10785  resqrexlemcalc2  10787  resqrexlemnm  10790  resqrexlemga  10795  reccn2ap  11082  sumsnf  11178  expcnvre  11272  geolim  11280  geolim2  11281  georeclim  11282  geoisumr  11287  geoisum1c  11289  cvgratnnlembern  11292  cvgratnnlemsumlt  11297  cvgratnnlemfm  11298  cvgratnnlemrate  11299  cvgratnn  11300  cvgratz  11301  efcllemp  11364  efgt1  11403  eflegeo  11408  eirraplem  11483  oddge22np1  11578  ltoddhalfle  11590  nno  11603  nn0oddm1d2  11606  nnoddm1d2  11607  zssinfcl  11641  coprmgcdb  11769  prmind2  11801  dvdsnprmd  11806  znege1  11856  sqrt2irrap  11858  divdenle  11875  nn0sqrtelqelz  11884  oddennn  11905  exmidunben  11939  dveflem  12855  cosz12  12861  sin0pilem2  12863  cos02pilt1  12932  trilpolemgt1  13232  trilpolemlt1  13234  trilpo  13236  taupi  13239