Theorem 1red 8177

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8014  1c1 8016

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

This theorem is referenced by:  recgt0  9013  ltrec  9046  recp1lt1  9062  peano5nni  9129  peano2nn  9138  nn0p1gt0  9414  nn0ge2m1nn  9445  peano2z  9498  suprzclex  9561  ledivge1le  9939  iccf1o  10217  zltaddlt1le  10220  fznatpl1  10289  elfz1b  10303  fzonn0p1p1  10436  elfzom1p1elfzo  10437  zssinfcl  10469  exbtwnzlemstep  10484  exbtwnz  10487  rebtwn2zlemstep  10489  rebtwn2z  10491  qfraclt1  10517  flqaddz  10534  btwnzge0  10537  2tnp1ge0ge0  10538  flhalf  10539  fldiv4lem1div2uz2  10543  modqid  10588  m1modge3gt1  10610  modqltm1p1mod  10615  addmodlteq  10637  seq3f1olemqsumkj  10750  ltexp2a  10830  leexp2a  10831  leexp2r  10832  nnlesq  10882  bernneq3  10901  expnbnd  10902  expnlbnd2  10904  nn0ltexp2  10948  expcanlem  10954  expcan  10955  bcval5  11002  wrdlenge2n0  11125  cvg1nlemcau  11516  resqrexlem1arp  11537  resqrexlemf1  11540  resqrexlemover  11542  resqrexlemdecn  11544  resqrexlemlo  11545  resqrexlemcalc2  11547  resqrexlemnm  11550  resqrexlemga  11555  reccn2ap  11845  sumsnf  11941  expcnvre  12035  geolim  12043  geolim2  12044  georeclim  12045  geoisumr  12050  geoisum1c  12052  cvgratnnlembern  12055  cvgratnnlemsumlt  12060  cvgratnnlemfm  12061  cvgratnnlemrate  12062  cvgratnn  12063  cvgratz  12064  prodsnf  12124  fprodrecl  12140  fprodreclf  12146  efcllemp  12190  efgt1  12229  eflegeo  12233  sinltxirr  12293  eirraplem  12309  p1modz1  12326  oddge22np1  12413  ltoddhalfle  12425  nno  12438  nn0oddm1d2  12441  nnoddm1d2  12442  bitsfzolem  12486  bitsfzo  12487  bitsmod  12488  bitscmp  12490  bitsinv1lem  12493  uzwodc  12579  coprmgcdb  12631  prmind2  12663  dvdsnprmd  12668  prmdc  12673  isprm5lem  12684  znege1  12721  sqrt2irrap  12723  divdenle  12740  nn0sqrtelqelz  12749  difsqpwdvds  12882  fldivp1  12892  pcfaclem  12893  4sqlem11  12945  4sqlem12  12946  2expltfac  12983  oddennn  12984  exmidunben  13018  nninfdclemlt  13043  znidomb  14643  psrbaglesuppg  14657  hoverlt1  15344  ivthdichlem  15346  dveflem  15421  reeff1oleme  15467  reeff1o  15468  cosz12  15475  sin0pilem2  15477  cos02pilt1  15546  rplogcl  15574  logdivlti  15576  cxplt  15611  cxple  15612  ltexp2  15636  logbrec  15655  logbgt0b  15661  logbgcd1irr  15662  logbgcd1irraplemexp  15663  logbgcd1irraplemap  15664  mersenne  15692  perfectlem2  15695  zabsle1  15699  lgslem3  15702  lgsdirprm  15734  gausslemma2dlem1a  15758  lgseisen  15774  lgsquadlem2  15778  2sqlem8  15823  clwwlkext2edg  16190  iooref1o  16516  trilpolemgt1  16521  trilpolemlt1  16523  trilpo  16525  redcwlpo  16537  neapmkvlem  16549  neapmkv  16550  taupi  16555