Theorem 1red 7564

Description: 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
1red	⊢ (𝜑 → 1 ∈ ℝ)

Proof of Theorem 1red

Step	Hyp	Ref	Expression
1		1re 7548	. 2 ⊢ 1 ∈ ℝ
2	1	a1i 9	1 ⊢ (𝜑 → 1 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 1439  ℝcr 7410  1c1 7412

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

This theorem is referenced by:  recgt0  8372  ltrec  8405  recp1lt1  8421  peano5nni  8486  peano2nn  8495  nn0p1gt0  8763  nn0ge2m1nn  8794  peano2z  8847  suprzclex  8905  ledivge1le  9264  iccf1o  9482  zltaddlt1le  9484  fznatpl1  9551  elfz1b  9565  fzonn0p1p1  9685  elfzom1p1elfzo  9686  exbtwnzlemstep  9720  exbtwnz  9723  rebtwn2zlemstep  9725  rebtwn2z  9727  qfraclt1  9748  flqaddz  9765  btwnzge0  9768  2tnp1ge0ge0  9769  flhalf  9770  modqid  9817  m1modge3gt1  9839  modqltm1p1mod  9844  addmodlteq  9866  seq3f1olemqsumkj  9988  ltexp2a  10068  leexp2a  10069  leexp2r  10070  nnlesq  10119  bernneq3  10137  expnbnd  10138  expnlbnd2  10140  expcanlem  10185  expcan  10186  ibcval5  10232  cvg1nlemcau  10478  resqrexlem1arp  10499  resqrexlemf1  10502  resqrexlemover  10504  resqrexlemdecn  10506  resqrexlemlo  10507  resqrexlemcalc2  10509  resqrexlemnm  10512  resqrexlemga  10517  sumsnf  10864  expcnvre  10958  geolim  10966  geolim2  10967  georeclim  10968  geoisumr  10973  geoisum1c  10975  cvgratnnlembern  10978  cvgratnnlemsumlt  10983  cvgratnnlemfm  10984  cvgratnnlemrate  10985  cvgratnn  10986  cvgratz  10987  efcllemp  11009  efgt1  11048  eflegeo  11053  eirraplem  11125  oddge22np1  11220  ltoddhalfle  11232  nno  11245  nn0oddm1d2  11248  nnoddm1d2  11249  zssinfcl  11283  coprmgcdb  11409  prmind2  11441  dvdsnprmd  11446  znege1  11495  sqrt2irrap  11497  divdenle  11514  nn0sqrtelqelz  11523  oddennn  11544