Theorem 1red 8100

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

Syntax hints:   → wi 4   ∈ wcel 2177  ℝcr 7937  1c1 7939

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

This theorem is referenced by:  recgt0  8936  ltrec  8969  recp1lt1  8985  peano5nni  9052  peano2nn  9061  nn0p1gt0  9337  nn0ge2m1nn  9368  peano2z  9421  suprzclex  9484  ledivge1le  9861  iccf1o  10139  zltaddlt1le  10142  fznatpl1  10211  elfz1b  10225  fzonn0p1p1  10355  elfzom1p1elfzo  10356  zssinfcl  10388  exbtwnzlemstep  10403  exbtwnz  10406  rebtwn2zlemstep  10408  rebtwn2z  10410  qfraclt1  10436  flqaddz  10453  btwnzge0  10456  2tnp1ge0ge0  10457  flhalf  10458  fldiv4lem1div2uz2  10462  modqid  10507  m1modge3gt1  10529  modqltm1p1mod  10534  addmodlteq  10556  seq3f1olemqsumkj  10669  ltexp2a  10749  leexp2a  10750  leexp2r  10751  nnlesq  10801  bernneq3  10820  expnbnd  10821  expnlbnd2  10823  nn0ltexp2  10867  expcanlem  10873  expcan  10874  bcval5  10921  wrdlenge2n0  11042  cvg1nlemcau  11345  resqrexlem1arp  11366  resqrexlemf1  11369  resqrexlemover  11371  resqrexlemdecn  11373  resqrexlemlo  11374  resqrexlemcalc2  11376  resqrexlemnm  11379  resqrexlemga  11384  reccn2ap  11674  sumsnf  11770  expcnvre  11864  geolim  11872  geolim2  11873  georeclim  11874  geoisumr  11879  geoisum1c  11881  cvgratnnlembern  11884  cvgratnnlemsumlt  11889  cvgratnnlemfm  11890  cvgratnnlemrate  11891  cvgratnn  11892  cvgratz  11893  prodsnf  11953  fprodrecl  11969  fprodreclf  11975  efcllemp  12019  efgt1  12058  eflegeo  12062  sinltxirr  12122  eirraplem  12138  p1modz1  12155  oddge22np1  12242  ltoddhalfle  12254  nno  12267  nn0oddm1d2  12270  nnoddm1d2  12271  bitsfzolem  12315  bitsfzo  12316  bitsmod  12317  bitscmp  12319  bitsinv1lem  12322  uzwodc  12408  coprmgcdb  12460  prmind2  12492  dvdsnprmd  12497  prmdc  12502  isprm5lem  12513  znege1  12550  sqrt2irrap  12552  divdenle  12569  nn0sqrtelqelz  12578  difsqpwdvds  12711  fldivp1  12721  pcfaclem  12722  4sqlem11  12774  4sqlem12  12775  2expltfac  12812  oddennn  12813  exmidunben  12847  nninfdclemlt  12872  znidomb  14470  psrbaglesuppg  14484  hoverlt1  15171  ivthdichlem  15173  dveflem  15248  reeff1oleme  15294  reeff1o  15295  cosz12  15302  sin0pilem2  15304  cos02pilt1  15373  rplogcl  15401  logdivlti  15403  cxplt  15438  cxple  15439  ltexp2  15463  logbrec  15482  logbgt0b  15488  logbgcd1irr  15489  logbgcd1irraplemexp  15490  logbgcd1irraplemap  15491  mersenne  15519  perfectlem2  15522  zabsle1  15526  lgslem3  15529  lgsdirprm  15561  gausslemma2dlem1a  15585  lgseisen  15601  lgsquadlem2  15605  2sqlem8  15650  iooref1o  16088  trilpolemgt1  16093  trilpolemlt1  16095  trilpo  16097  redcwlpo  16109  neapmkvlem  16121  neapmkv  16122  taupi  16127