Theorem 1red 8237

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8074  1c1 8076

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

This theorem is referenced by:  recgt0  9073  ltrec  9106  recp1lt1  9122  peano5nni  9189  peano2nn  9198  nn0p1gt0  9474  nn0ge2m1nn  9505  peano2z  9558  suprzclex  9621  ledivge1le  10004  iccf1o  10282  zltaddlt1le  10285  fznatpl1  10354  elfz1b  10368  fzonn0p1p1  10502  elfzom1p1elfzo  10503  zssinfcl  10536  exbtwnzlemstep  10551  exbtwnz  10554  rebtwn2zlemstep  10556  rebtwn2z  10558  qfraclt1  10584  flqaddz  10601  btwnzge0  10604  2tnp1ge0ge0  10605  flhalf  10606  fldiv4lem1div2uz2  10610  modqid  10655  m1modge3gt1  10677  modqltm1p1mod  10682  addmodlteq  10704  seq3f1olemqsumkj  10817  ltexp2a  10897  leexp2a  10898  leexp2r  10899  nnlesq  10949  bernneq3  10968  expnbnd  10969  expnlbnd2  10971  nn0ltexp2  11015  expcanlem  11021  expcan  11022  bcval5  11069  wrdlenge2n0  11196  cvg1nlemcau  11605  resqrexlem1arp  11626  resqrexlemf1  11629  resqrexlemover  11631  resqrexlemdecn  11633  resqrexlemlo  11634  resqrexlemcalc2  11636  resqrexlemnm  11639  resqrexlemga  11644  reccn2ap  11934  sumsnf  12031  expcnvre  12125  geolim  12133  geolim2  12134  georeclim  12135  geoisumr  12140  geoisum1c  12142  cvgratnnlembern  12145  cvgratnnlemsumlt  12150  cvgratnnlemfm  12151  cvgratnnlemrate  12152  cvgratnn  12153  cvgratz  12154  prodsnf  12214  fprodrecl  12230  fprodreclf  12236  efcllemp  12280  efgt1  12319  eflegeo  12323  sinltxirr  12383  eirraplem  12399  p1modz1  12416  oddge22np1  12503  ltoddhalfle  12515  nno  12528  nn0oddm1d2  12531  nnoddm1d2  12532  bitsfzolem  12576  bitsfzo  12577  bitsmod  12578  bitscmp  12580  bitsinv1lem  12583  uzwodc  12669  coprmgcdb  12721  prmind2  12753  dvdsnprmd  12758  prmdc  12763  isprm5lem  12774  znege1  12811  sqrt2irrap  12813  divdenle  12830  nn0sqrtelqelz  12839  difsqpwdvds  12972  fldivp1  12982  pcfaclem  12983  4sqlem11  13035  4sqlem12  13036  2expltfac  13073  oddennn  13074  exmidunben  13108  nninfdclemlt  13133  znidomb  14734  psrbaglesuppg  14748  hoverlt1  15440  ivthdichlem  15442  dveflem  15517  reeff1oleme  15563  reeff1o  15564  cosz12  15571  sin0pilem2  15573  cos02pilt1  15642  rplogcl  15670  logdivlti  15672  cxplt  15707  cxple  15708  ltexp2  15732  logbrec  15751  logbgt0b  15757  logbgcd1irr  15758  logbgcd1irraplemexp  15759  logbgcd1irraplemap  15760  pellexlem2  15772  mersenne  15791  perfectlem2  15794  zabsle1  15798  lgslem3  15801  lgsdirprm  15833  gausslemma2dlem1a  15857  lgseisen  15873  lgsquadlem2  15877  2sqlem8  15922  clwwlkext2edg  16343  clwwlknonex2lem2  16359  iooref1o  16746  trilpolemgt1  16751  trilpolemlt1  16753  trilpo  16755  redcwlpo  16768  neapmkvlem  16780  neapmkv  16781  taupi  16786  gsumgfsumlem  16792