Theorem 1red 7042

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

Syntax hints:   -> wi 4   e. wcel 1393   RRcr 6888   1c1 6890

This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-1re 6978

This theorem is referenced by:  recgt0  7816  ltrec  7849  recp1lt1  7865  peano5nni  7917  peano2nn  7926  nn0p1gt0  8211  nn0ge2m1nn  8242  peano2z  8281  ledivge1le  8652  iccf1o  8872  fznatpl1  8938  elfz1b  8952  fzonn0p1p1  9069  elfzom1p1elfzo  9070  qbtwnzlemstep  9103  qbtwnz  9106  rebtwn2zlemstep  9107  rebtwn2z  9109  qfraclt1  9122  flqaddz  9139  btwnzge0  9142  2tnp1ge0ge0  9143  flhalf  9144  ltexp2a  9306  leexp2a  9307  leexp2r  9308  nnlesq  9356  bernneq3  9371  expnbnd  9372  expnlbnd2  9374  cvg1nlemcau  9583  resqrexlem1arp  9603  resqrexlemf1  9606  resqrexlemover  9608  resqrexlemdecn  9610  resqrexlemlo  9611  resqrexlemcalc2  9613  resqrexlemnm  9616  resqrexlemga  9621