Theorem 1red 8341

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℝcr 8178  1c1 8180

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-1re 8273

This theorem is used by:  recgt0  9181  ltrec  9214  recp1lt1  9230  indfdc  9299  peano5nni  9308  peano2nn  9317  nn0p1gt0  9594  nn0ge2m1nn  9629  peano2z  9682  suprzclex  9746  ledivge1le  10129  lincmble  10408  iccf1o  10409  zltaddlt1le  10412  fznatpl1  10485  elfz1b  10499  fzonn0p1p1  10633  elfzom1p1elfzo  10634  zssinfcl  10667  exbtwnzlemstep  10684  exbtwnz  10687  rebtwn2zlemstep  10689  rebtwn2z  10691  qfraclt1  10717  flqaddz  10734  btwnzge0  10737  2tnp1ge0ge0  10738  flhalf  10739  fldiv4lem1div2uz2  10743  modqid  10788  m1modge3gt1  10810  modqltm1p1mod  10815  addmodlteq  10837  seq3f1olemqsumkj  10950  ltexp2a  11030  leexp2a  11031  leexp2r  11032  nnlesq  11082  resq01  11097  bernneq3  11102  expnbnd  11103  expnlbnd2  11105  nn0ltexp2  11149  expcanlem  11155  expcan  11156  bcval5  11203  ssenneg  11282  wrdlenge2n0  11342  sq01  11662  cvg1nlemcau  11752  resqrexlem1arp  11773  resqrexlemf1  11776  resqrexlemover  11778  resqrexlemdecn  11780  resqrexlemlo  11781  resqrexlemcalc2  11783  resqrexlemnm  11786  resqrexlemga  11791  reccn2ap  12081  sumsnf  12178  expcnvre  12272  geolim  12280  geolim2  12281  georeclim  12282  geoisumr  12287  geoisum1c  12289  cvgratnnlembern  12292  cvgratnnlemsumlt  12297  cvgratnnlemfm  12298  cvgratnnlemrate  12299  cvgratnn  12300  cvgratz  12301  prodsnf  12361  fprodrecl  12377  fprodreclf  12383  efcllemp  12427  efgt1  12466  eflegeo  12470  sinltxirr  12530  eirraplem  12546  p1modz1  12563  oddge22np1  12650  ltoddhalfle  12662  nno  12675  nn0oddm1d2  12678  nnoddm1d2  12679  bitsfzolem  12723  bitsfzo  12724  bitsmod  12725  bitscmp  12727  bitsinv1lem  12730  uzwodc  12816  coprmgcdb  12868  prmind2  12900  dvdsnprmd  12905  prmdc  12910  isprm5lem  12921  znege1  12958  sqrt2irrap  12960  divdenle  12977  nn0sqrtelqelz  12986  difsqpwdvds  13119  fldivp1  13129  pcfaclem  13130  4sqlem11  13182  4sqlem12  13183  2expltfac  13220  ballotfilemsgt1  13256  ballotfilemsel1i  13258  ballotfilemfrcn0  13275  oddennn  13285  exmidunben  13319  nninfdclemlt  13344  gzsumshift  14151  znidomb  14995  psrbaglesuppg  15059  hoverlt1  15752  ivthdichlem  15754  dveflem  15829  reeff1oleme  15875  reeff1o  15876  efap1p  15882  cosz12  15884  sin0pilem2  15886  cos02pilt1  15955  rplogcl  15984  logdivlti  15986  logdivlt  15999  cxplt  16024  cxple  16025  ltexp2  16049  logbrec  16068  logbgt0b  16074  logbgcd1irr  16075  logbgcd1irraplemexp  16076  logbgcd1irraplemap  16077  log2tlbndlog2  16088  birthdaylem3  16095  pellexlem2  16098  mersenne  16117  perfectlem2  16120  bcmono  16124  zabsle1  16130  lgslem3  16133  lgsdirprm  16165  gausslemma2dlem1a  16189  lgseisen  16205  lgsquadlem2  16209  2sqlem8  16254  clwwlkext2edg  16675  clwwlknonex2lem2  16691  iooref1o  17095  trilpolemgt1  17100  trilpolemlt1  17102  trilpo  17104  redcwlpo  17117  neapmkvlem  17129  neapmkv  17130  taupi  17135