Theorem 1red 8187

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8024  1c1 8026

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

This theorem is referenced by:  recgt0  9023  ltrec  9056  recp1lt1  9072  peano5nni  9139  peano2nn  9148  nn0p1gt0  9424  nn0ge2m1nn  9455  peano2z  9508  suprzclex  9571  ledivge1le  9954  iccf1o  10232  zltaddlt1le  10235  fznatpl1  10304  elfz1b  10318  fzonn0p1p1  10451  elfzom1p1elfzo  10452  zssinfcl  10485  exbtwnzlemstep  10500  exbtwnz  10503  rebtwn2zlemstep  10505  rebtwn2z  10507  qfraclt1  10533  flqaddz  10550  btwnzge0  10553  2tnp1ge0ge0  10554  flhalf  10555  fldiv4lem1div2uz2  10559  modqid  10604  m1modge3gt1  10626  modqltm1p1mod  10631  addmodlteq  10653  seq3f1olemqsumkj  10766  ltexp2a  10846  leexp2a  10847  leexp2r  10848  nnlesq  10898  bernneq3  10917  expnbnd  10918  expnlbnd2  10920  nn0ltexp2  10964  expcanlem  10970  expcan  10971  bcval5  11018  wrdlenge2n0  11142  cvg1nlemcau  11538  resqrexlem1arp  11559  resqrexlemf1  11562  resqrexlemover  11564  resqrexlemdecn  11566  resqrexlemlo  11567  resqrexlemcalc2  11569  resqrexlemnm  11572  resqrexlemga  11577  reccn2ap  11867  sumsnf  11963  expcnvre  12057  geolim  12065  geolim2  12066  georeclim  12067  geoisumr  12072  geoisum1c  12074  cvgratnnlembern  12077  cvgratnnlemsumlt  12082  cvgratnnlemfm  12083  cvgratnnlemrate  12084  cvgratnn  12085  cvgratz  12086  prodsnf  12146  fprodrecl  12162  fprodreclf  12168  efcllemp  12212  efgt1  12251  eflegeo  12255  sinltxirr  12315  eirraplem  12331  p1modz1  12348  oddge22np1  12435  ltoddhalfle  12447  nno  12460  nn0oddm1d2  12463  nnoddm1d2  12464  bitsfzolem  12508  bitsfzo  12509  bitsmod  12510  bitscmp  12512  bitsinv1lem  12515  uzwodc  12601  coprmgcdb  12653  prmind2  12685  dvdsnprmd  12690  prmdc  12695  isprm5lem  12706  znege1  12743  sqrt2irrap  12745  divdenle  12762  nn0sqrtelqelz  12771  difsqpwdvds  12904  fldivp1  12914  pcfaclem  12915  4sqlem11  12967  4sqlem12  12968  2expltfac  13005  oddennn  13006  exmidunben  13040  nninfdclemlt  13065  znidomb  14665  psrbaglesuppg  14679  hoverlt1  15366  ivthdichlem  15368  dveflem  15443  reeff1oleme  15489  reeff1o  15490  cosz12  15497  sin0pilem2  15499  cos02pilt1  15568  rplogcl  15596  logdivlti  15598  cxplt  15633  cxple  15634  ltexp2  15658  logbrec  15677  logbgt0b  15683  logbgcd1irr  15684  logbgcd1irraplemexp  15685  logbgcd1irraplemap  15686  mersenne  15714  perfectlem2  15717  zabsle1  15721  lgslem3  15724  lgsdirprm  15756  gausslemma2dlem1a  15780  lgseisen  15796  lgsquadlem2  15800  2sqlem8  15845  clwwlkext2edg  16231  clwwlknonex2lem2  16247  iooref1o  16588  trilpolemgt1  16593  trilpolemlt1  16595  trilpo  16597  redcwlpo  16609  neapmkvlem  16621  neapmkv  16622  taupi  16627  gsumgfsumlem  16633