Theorem 1red 8060

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℝcr 7897  1c1 7899

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

This theorem is referenced by:  recgt0  8896  ltrec  8929  recp1lt1  8945  peano5nni  9012  peano2nn  9021  nn0p1gt0  9297  nn0ge2m1nn  9328  peano2z  9381  suprzclex  9443  ledivge1le  9820  iccf1o  10098  zltaddlt1le  10101  fznatpl1  10170  elfz1b  10184  fzonn0p1p1  10308  elfzom1p1elfzo  10309  zssinfcl  10341  exbtwnzlemstep  10356  exbtwnz  10359  rebtwn2zlemstep  10361  rebtwn2z  10363  qfraclt1  10389  flqaddz  10406  btwnzge0  10409  2tnp1ge0ge0  10410  flhalf  10411  fldiv4lem1div2uz2  10415  modqid  10460  m1modge3gt1  10482  modqltm1p1mod  10487  addmodlteq  10509  seq3f1olemqsumkj  10622  ltexp2a  10702  leexp2a  10703  leexp2r  10704  nnlesq  10754  bernneq3  10773  expnbnd  10774  expnlbnd2  10776  nn0ltexp2  10820  expcanlem  10826  expcan  10827  bcval5  10874  wrdlenge2n0  10989  cvg1nlemcau  11168  resqrexlem1arp  11189  resqrexlemf1  11192  resqrexlemover  11194  resqrexlemdecn  11196  resqrexlemlo  11197  resqrexlemcalc2  11199  resqrexlemnm  11202  resqrexlemga  11207  reccn2ap  11497  sumsnf  11593  expcnvre  11687  geolim  11695  geolim2  11696  georeclim  11697  geoisumr  11702  geoisum1c  11704  cvgratnnlembern  11707  cvgratnnlemsumlt  11712  cvgratnnlemfm  11713  cvgratnnlemrate  11714  cvgratnn  11715  cvgratz  11716  prodsnf  11776  fprodrecl  11792  fprodreclf  11798  efcllemp  11842  efgt1  11881  eflegeo  11885  sinltxirr  11945  eirraplem  11961  p1modz1  11978  oddge22np1  12065  ltoddhalfle  12077  nno  12090  nn0oddm1d2  12093  nnoddm1d2  12094  bitsfzolem  12138  bitsfzo  12139  bitsmod  12140  bitscmp  12142  bitsinv1lem  12145  uzwodc  12231  coprmgcdb  12283  prmind2  12315  dvdsnprmd  12320  prmdc  12325  isprm5lem  12336  znege1  12373  sqrt2irrap  12375  divdenle  12392  nn0sqrtelqelz  12401  difsqpwdvds  12534  fldivp1  12544  pcfaclem  12545  4sqlem11  12597  4sqlem12  12598  2expltfac  12635  oddennn  12636  exmidunben  12670  nninfdclemlt  12695  znidomb  14292  psrbaglesuppg  14306  hoverlt1  14993  ivthdichlem  14995  dveflem  15070  reeff1oleme  15116  reeff1o  15117  cosz12  15124  sin0pilem2  15126  cos02pilt1  15195  rplogcl  15223  logdivlti  15225  cxplt  15260  cxple  15261  ltexp2  15285  logbrec  15304  logbgt0b  15310  logbgcd1irr  15311  logbgcd1irraplemexp  15312  logbgcd1irraplemap  15313  mersenne  15341  perfectlem2  15344  zabsle1  15348  lgslem3  15351  lgsdirprm  15383  gausslemma2dlem1a  15407  lgseisen  15423  lgsquadlem2  15427  2sqlem8  15472  iooref1o  15791  trilpolemgt1  15796  trilpolemlt1  15798  trilpo  15800  redcwlpo  15812  neapmkvlem  15824  neapmkv  15825  taupi  15830