Theorem 1red 8288

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℝcr 8125  1c1 8127

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

This theorem is referenced by:  recgt0  9123  ltrec  9156  recp1lt1  9172  peano5nni  9239  peano2nn  9248  nn0p1gt0  9524  nn0ge2m1nn  9559  peano2z  9612  suprzclex  9675  ledivge1le  10058  lincmble  10336  iccf1o  10337  zltaddlt1le  10340  fznatpl1  10409  elfz1b  10423  fzonn0p1p1  10557  elfzom1p1elfzo  10558  zssinfcl  10591  exbtwnzlemstep  10606  exbtwnz  10609  rebtwn2zlemstep  10611  rebtwn2z  10613  qfraclt1  10639  flqaddz  10656  btwnzge0  10659  2tnp1ge0ge0  10660  flhalf  10661  fldiv4lem1div2uz2  10665  modqid  10710  m1modge3gt1  10732  modqltm1p1mod  10737  addmodlteq  10759  seq3f1olemqsumkj  10872  ltexp2a  10952  leexp2a  10953  leexp2r  10954  nnlesq  11004  bernneq3  11023  expnbnd  11024  expnlbnd2  11026  nn0ltexp2  11070  expcanlem  11076  expcan  11077  bcval5  11124  ssenneg  11200  wrdlenge2n0  11256  cvg1nlemcau  11665  resqrexlem1arp  11686  resqrexlemf1  11689  resqrexlemover  11691  resqrexlemdecn  11693  resqrexlemlo  11694  resqrexlemcalc2  11696  resqrexlemnm  11699  resqrexlemga  11704  reccn2ap  11994  sumsnf  12091  expcnvre  12185  geolim  12193  geolim2  12194  georeclim  12195  geoisumr  12200  geoisum1c  12202  cvgratnnlembern  12205  cvgratnnlemsumlt  12210  cvgratnnlemfm  12211  cvgratnnlemrate  12212  cvgratnn  12213  cvgratz  12214  prodsnf  12274  fprodrecl  12290  fprodreclf  12296  efcllemp  12340  efgt1  12379  eflegeo  12383  sinltxirr  12443  eirraplem  12459  p1modz1  12476  oddge22np1  12563  ltoddhalfle  12575  nno  12588  nn0oddm1d2  12591  nnoddm1d2  12592  bitsfzolem  12636  bitsfzo  12637  bitsmod  12638  bitscmp  12640  bitsinv1lem  12643  uzwodc  12729  coprmgcdb  12781  prmind2  12813  dvdsnprmd  12818  prmdc  12823  isprm5lem  12834  znege1  12871  sqrt2irrap  12873  divdenle  12890  nn0sqrtelqelz  12899  difsqpwdvds  13032  fldivp1  13042  pcfaclem  13043  4sqlem11  13095  4sqlem12  13096  2expltfac  13133  oddennn  13135  exmidunben  13169  nninfdclemlt  13194  znidomb  14798  psrbaglesuppg  14813  hoverlt1  15506  ivthdichlem  15508  dveflem  15583  reeff1oleme  15629  reeff1o  15630  cosz12  15637  sin0pilem2  15639  cos02pilt1  15708  rplogcl  15736  logdivlti  15738  cxplt  15773  cxple  15774  ltexp2  15798  logbrec  15817  logbgt0b  15823  logbgcd1irr  15824  logbgcd1irraplemexp  15825  logbgcd1irraplemap  15826  pellexlem2  15838  mersenne  15857  perfectlem2  15860  zabsle1  15864  lgslem3  15867  lgsdirprm  15899  gausslemma2dlem1a  15923  lgseisen  15939  lgsquadlem2  15943  2sqlem8  15988  clwwlkext2edg  16409  clwwlknonex2lem2  16425  iooref1o  16810  trilpolemgt1  16815  trilpolemlt1  16817  trilpo  16819  redcwlpo  16832  neapmkvlem  16844  neapmkv  16845  taupi  16850  gsumgfsumlem  16856