Theorem 1red 8169

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8006  1c1 8008

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

This theorem is referenced by:  recgt0  9005  ltrec  9038  recp1lt1  9054  peano5nni  9121  peano2nn  9130  nn0p1gt0  9406  nn0ge2m1nn  9437  peano2z  9490  suprzclex  9553  ledivge1le  9930  iccf1o  10208  zltaddlt1le  10211  fznatpl1  10280  elfz1b  10294  fzonn0p1p1  10427  elfzom1p1elfzo  10428  zssinfcl  10460  exbtwnzlemstep  10475  exbtwnz  10478  rebtwn2zlemstep  10480  rebtwn2z  10482  qfraclt1  10508  flqaddz  10525  btwnzge0  10528  2tnp1ge0ge0  10529  flhalf  10530  fldiv4lem1div2uz2  10534  modqid  10579  m1modge3gt1  10601  modqltm1p1mod  10606  addmodlteq  10628  seq3f1olemqsumkj  10741  ltexp2a  10821  leexp2a  10822  leexp2r  10823  nnlesq  10873  bernneq3  10892  expnbnd  10893  expnlbnd2  10895  nn0ltexp2  10939  expcanlem  10945  expcan  10946  bcval5  10993  wrdlenge2n0  11115  cvg1nlemcau  11503  resqrexlem1arp  11524  resqrexlemf1  11527  resqrexlemover  11529  resqrexlemdecn  11531  resqrexlemlo  11532  resqrexlemcalc2  11534  resqrexlemnm  11537  resqrexlemga  11542  reccn2ap  11832  sumsnf  11928  expcnvre  12022  geolim  12030  geolim2  12031  georeclim  12032  geoisumr  12037  geoisum1c  12039  cvgratnnlembern  12042  cvgratnnlemsumlt  12047  cvgratnnlemfm  12048  cvgratnnlemrate  12049  cvgratnn  12050  cvgratz  12051  prodsnf  12111  fprodrecl  12127  fprodreclf  12133  efcllemp  12177  efgt1  12216  eflegeo  12220  sinltxirr  12280  eirraplem  12296  p1modz1  12313  oddge22np1  12400  ltoddhalfle  12412  nno  12425  nn0oddm1d2  12428  nnoddm1d2  12429  bitsfzolem  12473  bitsfzo  12474  bitsmod  12475  bitscmp  12477  bitsinv1lem  12480  uzwodc  12566  coprmgcdb  12618  prmind2  12650  dvdsnprmd  12655  prmdc  12660  isprm5lem  12671  znege1  12708  sqrt2irrap  12710  divdenle  12727  nn0sqrtelqelz  12736  difsqpwdvds  12869  fldivp1  12879  pcfaclem  12880  4sqlem11  12932  4sqlem12  12933  2expltfac  12970  oddennn  12971  exmidunben  13005  nninfdclemlt  13030  znidomb  14630  psrbaglesuppg  14644  hoverlt1  15331  ivthdichlem  15333  dveflem  15408  reeff1oleme  15454  reeff1o  15455  cosz12  15462  sin0pilem2  15464  cos02pilt1  15533  rplogcl  15561  logdivlti  15563  cxplt  15598  cxple  15599  ltexp2  15623  logbrec  15642  logbgt0b  15648  logbgcd1irr  15649  logbgcd1irraplemexp  15650  logbgcd1irraplemap  15651  mersenne  15679  perfectlem2  15682  zabsle1  15686  lgslem3  15689  lgsdirprm  15721  gausslemma2dlem1a  15745  lgseisen  15761  lgsquadlem2  15765  2sqlem8  15810  iooref1o  16432  trilpolemgt1  16437  trilpolemlt1  16439  trilpo  16441  redcwlpo  16453  neapmkvlem  16465  neapmkv  16466  taupi  16471