Theorem 1red 8058

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

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

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

This theorem is referenced by:  recgt0  8894  ltrec  8927  recp1lt1  8943  peano5nni  9010  peano2nn  9019  nn0p1gt0  9295  nn0ge2m1nn  9326  peano2z  9379  suprzclex  9441  ledivge1le  9818  iccf1o  10096  zltaddlt1le  10099  fznatpl1  10168  elfz1b  10182  fzonn0p1p1  10306  elfzom1p1elfzo  10307  zssinfcl  10339  exbtwnzlemstep  10354  exbtwnz  10357  rebtwn2zlemstep  10359  rebtwn2z  10361  qfraclt1  10387  flqaddz  10404  btwnzge0  10407  2tnp1ge0ge0  10408  flhalf  10409  fldiv4lem1div2uz2  10413  modqid  10458  m1modge3gt1  10480  modqltm1p1mod  10485  addmodlteq  10507  seq3f1olemqsumkj  10620  ltexp2a  10700  leexp2a  10701  leexp2r  10702  nnlesq  10752  bernneq3  10771  expnbnd  10772  expnlbnd2  10774  nn0ltexp2  10818  expcanlem  10824  expcan  10825  bcval5  10872  wrdlenge2n0  10987  cvg1nlemcau  11166  resqrexlem1arp  11187  resqrexlemf1  11190  resqrexlemover  11192  resqrexlemdecn  11194  resqrexlemlo  11195  resqrexlemcalc2  11197  resqrexlemnm  11200  resqrexlemga  11205  reccn2ap  11495  sumsnf  11591  expcnvre  11685  geolim  11693  geolim2  11694  georeclim  11695  geoisumr  11700  geoisum1c  11702  cvgratnnlembern  11705  cvgratnnlemsumlt  11710  cvgratnnlemfm  11711  cvgratnnlemrate  11712  cvgratnn  11713  cvgratz  11714  prodsnf  11774  fprodrecl  11790  fprodreclf  11796  efcllemp  11840  efgt1  11879  eflegeo  11883  sinltxirr  11943  eirraplem  11959  p1modz1  11976  oddge22np1  12063  ltoddhalfle  12075  nno  12088  nn0oddm1d2  12091  nnoddm1d2  12092  bitsfzolem  12136  bitsfzo  12137  bitsmod  12138  bitscmp  12140  bitsinv1lem  12143  uzwodc  12229  coprmgcdb  12281  prmind2  12313  dvdsnprmd  12318  prmdc  12323  isprm5lem  12334  znege1  12371  sqrt2irrap  12373  divdenle  12390  nn0sqrtelqelz  12399  difsqpwdvds  12532  fldivp1  12542  pcfaclem  12543  4sqlem11  12595  4sqlem12  12596  2expltfac  12633  oddennn  12634  exmidunben  12668  nninfdclemlt  12693  znidomb  14290  psrbaglesuppg  14302  hoverlt1  14969  ivthdichlem  14971  dveflem  15046  reeff1oleme  15092  reeff1o  15093  cosz12  15100  sin0pilem2  15102  cos02pilt1  15171  rplogcl  15199  logdivlti  15201  cxplt  15236  cxple  15237  ltexp2  15261  logbrec  15280  logbgt0b  15286  logbgcd1irr  15287  logbgcd1irraplemexp  15288  logbgcd1irraplemap  15289  mersenne  15317  perfectlem2  15320  zabsle1  15324  lgslem3  15327  lgsdirprm  15359  gausslemma2dlem1a  15383  lgseisen  15399  lgsquadlem2  15403  2sqlem8  15448  iooref1o  15765  trilpolemgt1  15770  trilpolemlt1  15772  trilpo  15774  redcwlpo  15786  neapmkvlem  15798  neapmkv  15799  taupi  15804