Theorem 1red 7971

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℝcr 7809  1c1 7811

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

This theorem is referenced by:  recgt0  8806  ltrec  8839  recp1lt1  8855  peano5nni  8921  peano2nn  8930  nn0p1gt0  9204  nn0ge2m1nn  9235  peano2z  9288  suprzclex  9350  ledivge1le  9725  iccf1o  10003  zltaddlt1le  10006  fznatpl1  10075  elfz1b  10089  fzonn0p1p1  10212  elfzom1p1elfzo  10213  exbtwnzlemstep  10247  exbtwnz  10250  rebtwn2zlemstep  10252  rebtwn2z  10254  qfraclt1  10279  flqaddz  10296  btwnzge0  10299  2tnp1ge0ge0  10300  flhalf  10301  modqid  10348  m1modge3gt1  10370  modqltm1p1mod  10375  addmodlteq  10397  seq3f1olemqsumkj  10497  ltexp2a  10571  leexp2a  10572  leexp2r  10573  nnlesq  10623  bernneq3  10642  expnbnd  10643  expnlbnd2  10645  nn0ltexp2  10688  expcanlem  10694  expcan  10695  bcval5  10742  cvg1nlemcau  10992  resqrexlem1arp  11013  resqrexlemf1  11016  resqrexlemover  11018  resqrexlemdecn  11020  resqrexlemlo  11021  resqrexlemcalc2  11023  resqrexlemnm  11026  resqrexlemga  11031  reccn2ap  11320  sumsnf  11416  expcnvre  11510  geolim  11518  geolim2  11519  georeclim  11520  geoisumr  11525  geoisum1c  11527  cvgratnnlembern  11530  cvgratnnlemsumlt  11535  cvgratnnlemfm  11536  cvgratnnlemrate  11537  cvgratnn  11538  cvgratz  11539  prodsnf  11599  fprodrecl  11615  fprodreclf  11621  efcllemp  11665  efgt1  11704  eflegeo  11708  eirraplem  11783  p1modz1  11800  oddge22np1  11885  ltoddhalfle  11897  nno  11910  nn0oddm1d2  11913  nnoddm1d2  11914  zssinfcl  11948  uzwodc  12037  coprmgcdb  12087  prmind2  12119  dvdsnprmd  12124  prmdc  12129  isprm5lem  12140  znege1  12177  sqrt2irrap  12179  divdenle  12196  nn0sqrtelqelz  12205  difsqpwdvds  12336  fldivp1  12345  pcfaclem  12346  oddennn  12392  exmidunben  12426  nninfdclemlt  12451  dveflem  14157  reeff1oleme  14163  reeff1o  14164  cosz12  14171  sin0pilem2  14173  cos02pilt1  14242  rplogcl  14270  logdivlti  14272  cxplt  14306  cxple  14307  ltexp2  14330  logbrec  14348  logbgt0b  14354  logbgcd1irr  14355  logbgcd1irraplemexp  14356  logbgcd1irraplemap  14357  zabsle1  14370  lgslem3  14373  lgsdirprm  14405  2sqlem8  14440  iooref1o  14752  trilpolemgt1  14757  trilpolemlt1  14759  trilpo  14761  redcwlpo  14773  neapmkvlem  14784  neapmkv  14785  taupi  14790