Theorem 1red 7557

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

Syntax hints:   -> wi 4   e. wcel 1439   RRcr 7403   1c1 7405

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

This theorem is referenced by:  recgt0  8365  ltrec  8398  recp1lt1  8414  peano5nni  8479  peano2nn  8488  nn0p1gt0  8756  nn0ge2m1nn  8787  peano2z  8840  suprzclex  8898  ledivge1le  9257  iccf1o  9475  zltaddlt1le  9477  fznatpl1  9544  elfz1b  9558  fzonn0p1p1  9678  elfzom1p1elfzo  9679  exbtwnzlemstep  9713  exbtwnz  9716  rebtwn2zlemstep  9718  rebtwn2z  9720  qfraclt1  9741  flqaddz  9758  btwnzge0  9761  2tnp1ge0ge0  9762  flhalf  9763  modqid  9810  m1modge3gt1  9832  modqltm1p1mod  9837  addmodlteq  9859  seq3f1olemqsumkj  9981  ltexp2a  10061  leexp2a  10062  leexp2r  10063  nnlesq  10112  bernneq3  10130  expnbnd  10131  expnlbnd2  10133  expcanlem  10178  expcan  10179  ibcval5  10225  cvg1nlemcau  10471  resqrexlem1arp  10492  resqrexlemf1  10495  resqrexlemover  10497  resqrexlemdecn  10499  resqrexlemlo  10500  resqrexlemcalc2  10502  resqrexlemnm  10505  resqrexlemga  10510  sumsnf  10857  expcnvre  10951  geolim  10959  geolim2  10960  georeclim  10961  geoisumr  10966  geoisum1c  10968  cvgratnnlembern  10971  cvgratnnlemsumlt  10976  cvgratnnlemfm  10977  cvgratnnlemrate  10978  cvgratnn  10979  cvgratz  10980  efcllemp  11002  efgt1  11041  eflegeo  11046  eirraplem  11118  oddge22np1  11213  ltoddhalfle  11225  nno  11238  nn0oddm1d2  11241  nnoddm1d2  11242  zssinfcl  11276  coprmgcdb  11402  prmind2  11434  dvdsnprmd  11439  znege1  11488  sqrt2irrap  11490  divdenle  11507  nn0sqrtelqelz  11516  oddennn  11537