Theorem 1red 7805

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

Syntax hints:   → wi 4   ∈ wcel 1481  ℝcr 7643  1c1 7645

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

This theorem is referenced by:  recgt0  8632  ltrec  8665  recp1lt1  8681  peano5nni  8747  peano2nn  8756  nn0p1gt0  9030  nn0ge2m1nn  9061  peano2z  9114  suprzclex  9173  ledivge1le  9543  iccf1o  9817  zltaddlt1le  9820  fznatpl1  9887  elfz1b  9901  fzonn0p1p1  10021  elfzom1p1elfzo  10022  exbtwnzlemstep  10056  exbtwnz  10059  rebtwn2zlemstep  10061  rebtwn2z  10063  qfraclt1  10084  flqaddz  10101  btwnzge0  10104  2tnp1ge0ge0  10105  flhalf  10106  modqid  10153  m1modge3gt1  10175  modqltm1p1mod  10180  addmodlteq  10202  seq3f1olemqsumkj  10302  ltexp2a  10376  leexp2a  10377  leexp2r  10378  nnlesq  10427  bernneq3  10445  expnbnd  10446  expnlbnd2  10448  expcanlem  10493  expcan  10494  bcval5  10541  cvg1nlemcau  10788  resqrexlem1arp  10809  resqrexlemf1  10812  resqrexlemover  10814  resqrexlemdecn  10816  resqrexlemlo  10817  resqrexlemcalc2  10819  resqrexlemnm  10822  resqrexlemga  10827  reccn2ap  11114  sumsnf  11210  expcnvre  11304  geolim  11312  geolim2  11313  georeclim  11314  geoisumr  11319  geoisum1c  11321  cvgratnnlembern  11324  cvgratnnlemsumlt  11329  cvgratnnlemfm  11330  cvgratnnlemrate  11331  cvgratnn  11332  cvgratz  11333  efcllemp  11401  efgt1  11440  eflegeo  11444  eirraplem  11519  oddge22np1  11614  ltoddhalfle  11626  nno  11639  nn0oddm1d2  11642  nnoddm1d2  11643  zssinfcl  11677  coprmgcdb  11805  prmind2  11837  dvdsnprmd  11842  znege1  11892  sqrt2irrap  11894  divdenle  11911  nn0sqrtelqelz  11920  oddennn  11941  exmidunben  11975  dveflem  12895  reeff1oleme  12901  reeff1o  12902  cosz12  12909  sin0pilem2  12911  cos02pilt1  12980  rplogcl  13008  logdivlti  13010  cxplt  13044  cxple  13045  logbrec  13085  logbgt0b  13091  logbgcd1irr  13092  logbgcd1irraplemexp  13093  logbgcd1irraplemap  13094  trilpolemgt1  13407  trilpolemlt1  13409  trilpo  13411  redcwlpo  13422  neapmkvlem  13424  neapmkv  13425  iooref1o  13426  taupi  13430