Theorem 1red 8305

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℝcr 8142  1c1 8144

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

This theorem is referenced by:  recgt0  9141  ltrec  9174  recp1lt1  9190  peano5nni  9257  peano2nn  9266  nn0p1gt0  9542  nn0ge2m1nn  9577  peano2z  9630  suprzclex  9694  ledivge1le  10077  lincmble  10356  iccf1o  10357  zltaddlt1le  10360  fznatpl1  10432  elfz1b  10446  fzonn0p1p1  10580  elfzom1p1elfzo  10581  zssinfcl  10614  exbtwnzlemstep  10631  exbtwnz  10634  rebtwn2zlemstep  10636  rebtwn2z  10638  qfraclt1  10664  flqaddz  10681  btwnzge0  10684  2tnp1ge0ge0  10685  flhalf  10686  fldiv4lem1div2uz2  10690  modqid  10735  m1modge3gt1  10757  modqltm1p1mod  10762  addmodlteq  10784  seq3f1olemqsumkj  10897  ltexp2a  10977  leexp2a  10978  leexp2r  10979  nnlesq  11029  resq01  11044  bernneq3  11049  expnbnd  11050  expnlbnd2  11052  nn0ltexp2  11096  expcanlem  11102  expcan  11103  bcval5  11150  ssenneg  11229  wrdlenge2n0  11285  cvg1nlemcau  11694  resqrexlem1arp  11715  resqrexlemf1  11718  resqrexlemover  11720  resqrexlemdecn  11722  resqrexlemlo  11723  resqrexlemcalc2  11725  resqrexlemnm  11728  resqrexlemga  11733  reccn2ap  12023  sumsnf  12120  expcnvre  12214  geolim  12222  geolim2  12223  georeclim  12224  geoisumr  12229  geoisum1c  12231  cvgratnnlembern  12234  cvgratnnlemsumlt  12239  cvgratnnlemfm  12240  cvgratnnlemrate  12241  cvgratnn  12242  cvgratz  12243  prodsnf  12303  fprodrecl  12319  fprodreclf  12325  efcllemp  12369  efgt1  12408  eflegeo  12412  sinltxirr  12472  eirraplem  12488  p1modz1  12505  oddge22np1  12592  ltoddhalfle  12604  nno  12617  nn0oddm1d2  12620  nnoddm1d2  12621  bitsfzolem  12665  bitsfzo  12666  bitsmod  12667  bitscmp  12669  bitsinv1lem  12672  uzwodc  12758  coprmgcdb  12810  prmind2  12842  dvdsnprmd  12847  prmdc  12852  isprm5lem  12863  znege1  12900  sqrt2irrap  12902  divdenle  12919  nn0sqrtelqelz  12928  difsqpwdvds  13061  fldivp1  13071  pcfaclem  13072  4sqlem11  13124  4sqlem12  13125  2expltfac  13162  ballotfilemsgt1  13198  ballotfilemsel1i  13200  ballotfilemfrcn0  13217  oddennn  13227  exmidunben  13261  nninfdclemlt  13286  znidomb  14918  psrbaglesuppg  14933  hoverlt1  15626  ivthdichlem  15628  dveflem  15703  reeff1oleme  15749  reeff1o  15750  cosz12  15757  sin0pilem2  15759  cos02pilt1  15828  rplogcl  15856  logdivlti  15858  cxplt  15893  cxple  15894  ltexp2  15918  logbrec  15937  logbgt0b  15943  logbgcd1irr  15944  logbgcd1irraplemexp  15945  logbgcd1irraplemap  15946  pellexlem2  15958  mersenne  15977  perfectlem2  15980  zabsle1  15984  lgslem3  15987  lgsdirprm  16019  gausslemma2dlem1a  16043  lgseisen  16059  lgsquadlem2  16063  2sqlem8  16108  clwwlkext2edg  16529  clwwlknonex2lem2  16545  iooref1o  16930  trilpolemgt1  16935  trilpolemlt1  16937  trilpo  16939  redcwlpo  16952  neapmkvlem  16965  neapmkv  16966  taupi  16971  gsumgfsumlem  16977