Theorem 1red 8041

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℝcr 7878  1c1 7880

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

This theorem is referenced by:  recgt0  8877  ltrec  8910  recp1lt1  8926  peano5nni  8993  peano2nn  9002  nn0p1gt0  9278  nn0ge2m1nn  9309  peano2z  9362  suprzclex  9424  ledivge1le  9801  iccf1o  10079  zltaddlt1le  10082  fznatpl1  10151  elfz1b  10165  fzonn0p1p1  10289  elfzom1p1elfzo  10290  zssinfcl  10322  exbtwnzlemstep  10337  exbtwnz  10340  rebtwn2zlemstep  10342  rebtwn2z  10344  qfraclt1  10370  flqaddz  10387  btwnzge0  10390  2tnp1ge0ge0  10391  flhalf  10392  fldiv4lem1div2uz2  10396  modqid  10441  m1modge3gt1  10463  modqltm1p1mod  10468  addmodlteq  10490  seq3f1olemqsumkj  10603  ltexp2a  10683  leexp2a  10684  leexp2r  10685  nnlesq  10735  bernneq3  10754  expnbnd  10755  expnlbnd2  10757  nn0ltexp2  10801  expcanlem  10807  expcan  10808  bcval5  10855  wrdlenge2n0  10970  cvg1nlemcau  11149  resqrexlem1arp  11170  resqrexlemf1  11173  resqrexlemover  11175  resqrexlemdecn  11177  resqrexlemlo  11178  resqrexlemcalc2  11180  resqrexlemnm  11183  resqrexlemga  11188  reccn2ap  11478  sumsnf  11574  expcnvre  11668  geolim  11676  geolim2  11677  georeclim  11678  geoisumr  11683  geoisum1c  11685  cvgratnnlembern  11688  cvgratnnlemsumlt  11693  cvgratnnlemfm  11694  cvgratnnlemrate  11695  cvgratnn  11696  cvgratz  11697  prodsnf  11757  fprodrecl  11773  fprodreclf  11779  efcllemp  11823  efgt1  11862  eflegeo  11866  sinltxirr  11926  eirraplem  11942  p1modz1  11959  oddge22np1  12046  ltoddhalfle  12058  nno  12071  nn0oddm1d2  12074  nnoddm1d2  12075  bitsfzolem  12118  bitsfzo  12119  uzwodc  12204  coprmgcdb  12256  prmind2  12288  dvdsnprmd  12293  prmdc  12298  isprm5lem  12309  znege1  12346  sqrt2irrap  12348  divdenle  12365  nn0sqrtelqelz  12374  difsqpwdvds  12507  fldivp1  12517  pcfaclem  12518  4sqlem11  12570  4sqlem12  12571  2expltfac  12608  oddennn  12609  exmidunben  12643  nninfdclemlt  12668  znidomb  14214  psrbaglesuppg  14226  hoverlt1  14885  ivthdichlem  14887  dveflem  14962  reeff1oleme  15008  reeff1o  15009  cosz12  15016  sin0pilem2  15018  cos02pilt1  15087  rplogcl  15115  logdivlti  15117  cxplt  15152  cxple  15153  ltexp2  15177  logbrec  15196  logbgt0b  15202  logbgcd1irr  15203  logbgcd1irraplemexp  15204  logbgcd1irraplemap  15205  mersenne  15233  perfectlem2  15236  zabsle1  15240  lgslem3  15243  lgsdirprm  15275  gausslemma2dlem1a  15299  lgseisen  15315  lgsquadlem2  15319  2sqlem8  15364  iooref1o  15678  trilpolemgt1  15683  trilpolemlt1  15685  trilpo  15687  redcwlpo  15699  neapmkvlem  15711  neapmkv  15712  taupi  15717