Theorem 1red 8335

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

Syntax hints:   → wi 4   ∈ wcel 2209  ℝcr 8172  1c1 8174

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

This theorem is referenced by:  recgt0  9174  ltrec  9207  recp1lt1  9223  peano5nni  9290  peano2nn  9299  nn0p1gt0  9575  nn0ge2m1nn  9610  peano2z  9663  suprzclex  9727  ledivge1le  10110  lincmble  10389  iccf1o  10390  zltaddlt1le  10393  fznatpl1  10466  elfz1b  10480  fzonn0p1p1  10614  elfzom1p1elfzo  10615  zssinfcl  10648  exbtwnzlemstep  10665  exbtwnz  10668  rebtwn2zlemstep  10670  rebtwn2z  10672  qfraclt1  10698  flqaddz  10715  btwnzge0  10718  2tnp1ge0ge0  10719  flhalf  10720  fldiv4lem1div2uz2  10724  modqid  10769  m1modge3gt1  10791  modqltm1p1mod  10796  addmodlteq  10818  seq3f1olemqsumkj  10931  ltexp2a  11011  leexp2a  11012  leexp2r  11013  nnlesq  11063  resq01  11078  bernneq3  11083  expnbnd  11084  expnlbnd2  11086  nn0ltexp2  11130  expcanlem  11136  expcan  11137  bcval5  11184  ssenneg  11263  wrdlenge2n0  11323  sq01  11643  cvg1nlemcau  11733  resqrexlem1arp  11754  resqrexlemf1  11757  resqrexlemover  11759  resqrexlemdecn  11761  resqrexlemlo  11762  resqrexlemcalc2  11764  resqrexlemnm  11767  resqrexlemga  11772  reccn2ap  12062  sumsnf  12159  expcnvre  12253  geolim  12261  geolim2  12262  georeclim  12263  geoisumr  12268  geoisum1c  12270  cvgratnnlembern  12273  cvgratnnlemsumlt  12278  cvgratnnlemfm  12279  cvgratnnlemrate  12280  cvgratnn  12281  cvgratz  12282  prodsnf  12342  fprodrecl  12358  fprodreclf  12364  efcllemp  12408  efgt1  12447  eflegeo  12451  sinltxirr  12511  eirraplem  12527  p1modz1  12544  oddge22np1  12631  ltoddhalfle  12643  nno  12656  nn0oddm1d2  12659  nnoddm1d2  12660  bitsfzolem  12704  bitsfzo  12705  bitsmod  12706  bitscmp  12708  bitsinv1lem  12711  uzwodc  12797  coprmgcdb  12849  prmind2  12881  dvdsnprmd  12886  prmdc  12891  isprm5lem  12902  znege1  12939  sqrt2irrap  12941  divdenle  12958  nn0sqrtelqelz  12967  difsqpwdvds  13100  fldivp1  13110  pcfaclem  13111  4sqlem11  13163  4sqlem12  13164  2expltfac  13201  ballotfilemsgt1  13237  ballotfilemsel1i  13239  ballotfilemfrcn0  13256  oddennn  13266  exmidunben  13300  nninfdclemlt  13325  gzsumshift  14132  znidomb  14976  psrbaglesuppg  15040  hoverlt1  15733  ivthdichlem  15735  dveflem  15810  reeff1oleme  15856  reeff1o  15857  cosz12  15864  sin0pilem2  15866  cos02pilt1  15935  rplogcl  15963  logdivlti  15965  cxplt  16001  cxple  16002  ltexp2  16026  logbrec  16045  logbgt0b  16051  logbgcd1irr  16052  logbgcd1irraplemexp  16053  logbgcd1irraplemap  16054  log2tlbndlog2  16065  birthdaylem3  16072  pellexlem2  16075  mersenne  16094  perfectlem2  16097  zabsle1  16101  lgslem3  16104  lgsdirprm  16136  gausslemma2dlem1a  16160  lgseisen  16176  lgsquadlem2  16180  2sqlem8  16225  clwwlkext2edg  16646  clwwlknonex2lem2  16662  iooref1o  17057  trilpolemgt1  17062  trilpolemlt1  17064  trilpo  17066  redcwlpo  17079  neapmkvlem  17091  neapmkv  17092  taupi  17097