Theorem 1red 8194

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8031  1c1 8033

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

This theorem is referenced by:  recgt0  9030  ltrec  9063  recp1lt1  9079  peano5nni  9146  peano2nn  9155  nn0p1gt0  9431  nn0ge2m1nn  9462  peano2z  9515  suprzclex  9578  ledivge1le  9961  iccf1o  10239  zltaddlt1le  10242  fznatpl1  10311  elfz1b  10325  fzonn0p1p1  10459  elfzom1p1elfzo  10460  zssinfcl  10493  exbtwnzlemstep  10508  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2z  10515  qfraclt1  10541  flqaddz  10558  btwnzge0  10561  2tnp1ge0ge0  10562  flhalf  10563  fldiv4lem1div2uz2  10567  modqid  10612  m1modge3gt1  10634  modqltm1p1mod  10639  addmodlteq  10661  seq3f1olemqsumkj  10774  ltexp2a  10854  leexp2a  10855  leexp2r  10856  nnlesq  10906  bernneq3  10925  expnbnd  10926  expnlbnd2  10928  nn0ltexp2  10972  expcanlem  10978  expcan  10979  bcval5  11026  wrdlenge2n0  11153  cvg1nlemcau  11549  resqrexlem1arp  11570  resqrexlemf1  11573  resqrexlemover  11575  resqrexlemdecn  11577  resqrexlemlo  11578  resqrexlemcalc2  11580  resqrexlemnm  11583  resqrexlemga  11588  reccn2ap  11878  sumsnf  11975  expcnvre  12069  geolim  12077  geolim2  12078  georeclim  12079  geoisumr  12084  geoisum1c  12086  cvgratnnlembern  12089  cvgratnnlemsumlt  12094  cvgratnnlemfm  12095  cvgratnnlemrate  12096  cvgratnn  12097  cvgratz  12098  prodsnf  12158  fprodrecl  12174  fprodreclf  12180  efcllemp  12224  efgt1  12263  eflegeo  12267  sinltxirr  12327  eirraplem  12343  p1modz1  12360  oddge22np1  12447  ltoddhalfle  12459  nno  12472  nn0oddm1d2  12475  nnoddm1d2  12476  bitsfzolem  12520  bitsfzo  12521  bitsmod  12522  bitscmp  12524  bitsinv1lem  12527  uzwodc  12613  coprmgcdb  12665  prmind2  12697  dvdsnprmd  12702  prmdc  12707  isprm5lem  12718  znege1  12755  sqrt2irrap  12757  divdenle  12774  nn0sqrtelqelz  12783  difsqpwdvds  12916  fldivp1  12926  pcfaclem  12927  4sqlem11  12979  4sqlem12  12980  2expltfac  13017  oddennn  13018  exmidunben  13052  nninfdclemlt  13077  znidomb  14678  psrbaglesuppg  14692  hoverlt1  15379  ivthdichlem  15381  dveflem  15456  reeff1oleme  15502  reeff1o  15503  cosz12  15510  sin0pilem2  15512  cos02pilt1  15581  rplogcl  15609  logdivlti  15611  cxplt  15646  cxple  15647  ltexp2  15671  logbrec  15690  logbgt0b  15696  logbgcd1irr  15697  logbgcd1irraplemexp  15698  logbgcd1irraplemap  15699  mersenne  15727  perfectlem2  15730  zabsle1  15734  lgslem3  15737  lgsdirprm  15769  gausslemma2dlem1a  15793  lgseisen  15809  lgsquadlem2  15813  2sqlem8  15858  clwwlkext2edg  16279  clwwlknonex2lem2  16295  iooref1o  16664  trilpolemgt1  16669  trilpolemlt1  16671  trilpo  16673  redcwlpo  16685  neapmkvlem  16697  neapmkv  16698  taupi  16703  gsumgfsumlem  16709