Theorem 1red 7876

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

Syntax hints:   → wi 4   ∈ wcel 2128  ℝcr 7714  1c1 7716

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

This theorem is referenced by:  recgt0  8704  ltrec  8737  recp1lt1  8753  peano5nni  8819  peano2nn  8828  nn0p1gt0  9102  nn0ge2m1nn  9133  peano2z  9186  suprzclex  9245  ledivge1le  9615  iccf1o  9890  zltaddlt1le  9893  fznatpl1  9960  elfz1b  9974  fzonn0p1p1  10094  elfzom1p1elfzo  10095  exbtwnzlemstep  10129  exbtwnz  10132  rebtwn2zlemstep  10134  rebtwn2z  10136  qfraclt1  10161  flqaddz  10178  btwnzge0  10181  2tnp1ge0ge0  10182  flhalf  10183  modqid  10230  m1modge3gt1  10252  modqltm1p1mod  10257  addmodlteq  10279  seq3f1olemqsumkj  10379  ltexp2a  10453  leexp2a  10454  leexp2r  10455  nnlesq  10504  bernneq3  10522  expnbnd  10523  expnlbnd2  10525  expcanlem  10571  expcan  10572  bcval5  10619  cvg1nlemcau  10866  resqrexlem1arp  10887  resqrexlemf1  10890  resqrexlemover  10892  resqrexlemdecn  10894  resqrexlemlo  10895  resqrexlemcalc2  10897  resqrexlemnm  10900  resqrexlemga  10905  reccn2ap  11192  sumsnf  11288  expcnvre  11382  geolim  11390  geolim2  11391  georeclim  11392  geoisumr  11397  geoisum1c  11399  cvgratnnlembern  11402  cvgratnnlemsumlt  11407  cvgratnnlemfm  11408  cvgratnnlemrate  11409  cvgratnn  11410  cvgratz  11411  prodsnf  11471  fprodrecl  11487  fprodreclf  11493  efcllemp  11537  efgt1  11576  eflegeo  11580  eirraplem  11655  p1modz1  11672  oddge22np1  11753  ltoddhalfle  11765  nno  11778  nn0oddm1d2  11781  nnoddm1d2  11782  zssinfcl  11816  coprmgcdb  11945  prmind2  11977  dvdsnprmd  11982  znege1  12032  sqrt2irrap  12034  divdenle  12051  nn0sqrtelqelz  12060  oddennn  12093  exmidunben  12127  dveflem  13047  reeff1oleme  13053  reeff1o  13054  cosz12  13061  sin0pilem2  13063  cos02pilt1  13132  rplogcl  13160  logdivlti  13162  cxplt  13196  cxple  13197  logbrec  13237  logbgt0b  13243  logbgcd1irr  13244  logbgcd1irraplemexp  13245  logbgcd1irraplemap  13246  iooref1o  13568  trilpolemgt1  13573  trilpolemlt1  13575  trilpo  13577  redcwlpo  13589  neapmkvlem  13600  neapmkv  13601  taupi  13604