Theorem 1red 7774

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 7758	. 2 ⊢ 1 ∈ ℝ
2	1	a1i 9	1 ⊢ (𝜑 → 1 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 1480  ℝcr 7612  1c1 7614

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

This theorem is referenced by:  recgt0  8601  ltrec  8634  recp1lt1  8650  peano5nni  8716  peano2nn  8725  nn0p1gt0  8999  nn0ge2m1nn  9030  peano2z  9083  suprzclex  9142  ledivge1le  9506  iccf1o  9780  zltaddlt1le  9782  fznatpl1  9849  elfz1b  9863  fzonn0p1p1  9983  elfzom1p1elfzo  9984  exbtwnzlemstep  10018  exbtwnz  10021  rebtwn2zlemstep  10023  rebtwn2z  10025  qfraclt1  10046  flqaddz  10063  btwnzge0  10066  2tnp1ge0ge0  10067  flhalf  10068  modqid  10115  m1modge3gt1  10137  modqltm1p1mod  10142  addmodlteq  10164  seq3f1olemqsumkj  10264  ltexp2a  10338  leexp2a  10339  leexp2r  10340  nnlesq  10389  bernneq3  10407  expnbnd  10408  expnlbnd2  10410  expcanlem  10455  expcan  10456  bcval5  10502  cvg1nlemcau  10749  resqrexlem1arp  10770  resqrexlemf1  10773  resqrexlemover  10775  resqrexlemdecn  10777  resqrexlemlo  10778  resqrexlemcalc2  10780  resqrexlemnm  10783  resqrexlemga  10788  reccn2ap  11075  sumsnf  11171  expcnvre  11265  geolim  11273  geolim2  11274  georeclim  11275  geoisumr  11280  geoisum1c  11282  cvgratnnlembern  11285  cvgratnnlemsumlt  11290  cvgratnnlemfm  11291  cvgratnnlemrate  11292  cvgratnn  11293  cvgratz  11294  efcllemp  11353  efgt1  11392  eflegeo  11397  eirraplem  11472  oddge22np1  11567  ltoddhalfle  11579  nno  11592  nn0oddm1d2  11595  nnoddm1d2  11596  zssinfcl  11630  coprmgcdb  11758  prmind2  11790  dvdsnprmd  11795  znege1  11845  sqrt2irrap  11847  divdenle  11864  nn0sqrtelqelz  11873  oddennn  11894  exmidunben  11928  dveflem  12844  cosz12  12850  sin0pilem2  12852  cos02pilt1  12921  trilpolemgt1  13221  trilpolemlt1  13223  trilpo  13225  taupi  13228