Theorem 1red 8342

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

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

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

This theorem is used by:  recgt0  9183  ltrec  9216  recp1lt1  9232  indfdc  9301  peano5nni  9310  peano2nn  9319  nn0p1gt0  9597  nn0ge2m1nn  9632  peano2z  9685  suprzclex  9749  ledivge1le  10138  lincmble  10417  iccf1o  10418  zltaddlt1le  10421  fznatpl1  10494  elfz1b  10508  fzonn0p1p1  10642  elfzom1p1elfzo  10643  zssinfcl  10676  exbtwnzlemstep  10693  exbtwnz  10696  rebtwn2zlemstep  10698  rebtwn2z  10700  qfraclt1  10728  flqaddz  10746  btwnzge0  10749  2tnp1ge0ge0  10750  flhalf  10751  fldiv4lem1div2uz2  10755  modqid  10800  m1modge3gt1  10822  modqltm1p1mod  10827  addmodlteq  10849  seq3f1olemqsumkj  10962  ltexp2a  11042  leexp2a  11043  leexp2r  11044  nnlesq  11094  resq01  11109  bernneq3  11114  expnbnd  11115  expnlbnd2  11117  nn0ltexp2  11162  expcanlem  11168  expcan  11169  bcval5  11216  ssenneg  11295  wrdlenge2n0  11355  sq01  11675  cvg1nlemcau  11765  resqrexlem1arp  11786  resqrexlemf1  11789  resqrexlemover  11791  resqrexlemdecn  11793  resqrexlemlo  11794  resqrexlemcalc2  11796  resqrexlemnm  11799  resqrexlemga  11804  reccn2ap  12097  sumsnf  12194  expcnvre  12288  geolim  12296  geolim2  12297  georeclim  12298  geoisumr  12303  geoisum1c  12305  cvgratnnlembern  12308  cvgratnnlemsumlt  12313  cvgratnnlemfm  12314  cvgratnnlemrate  12315  cvgratnn  12316  cvgratz  12317  prodsnf  12377  fprodrecl  12393  fprodreclf  12399  efcllemp  12443  efgt1  12482  eflegeo  12486  sinltxirr  12546  eirraplem  12562  p1modz1  12579  oddge22np1  12666  ltoddhalfle  12678  nno  12691  nn0oddm1d2  12694  nnoddm1d2  12695  bitsfzolem  12739  bitsfzo  12740  bitsmod  12741  bitscmp  12743  bitsinv1lem  12746  uzwodc  12832  coprmgcdb  12884  prmind2  12916  dvdsnprmd  12921  prmdc  12926  isprm5lem  12938  znege1  12976  sqrt2irrap  12978  divdenle  12995  nn0sqrtelqelz  13004  difsqpwdvds  13139  fldivp1  13149  pcfaclem  13150  4sqlem11  13202  4sqlem12  13203  2expltfac  13241  ballotfilemsgt1  13305  ballotfilemsel1i  13307  ballotfilemfrcn0  13324  oddennn  13334  exmidunben  13368  nninfdclemlt  13393  gzsumshift  14200  znidomb  15044  psrbaglesuppg  15108  hoverlt1  15802  ivthdichlem  15804  dveflem  15879  reeff1oleme  15925  reeff1o  15926  efap1p  15932  cosz12  15934  sin0pilem2  15936  cos02pilt1  16005  rplogcl  16034  logdivlti  16036  logdivlt  16049  cxplt  16074  cxple  16075  ltexp2  16099  logbrec  16118  logbgt0b  16124  logbgcd1irr  16125  logbgcd1irraplemexp  16126  logbgcd1irraplemap  16127  zprmlogbaplem1  16137  zprmlogbaplem2  16138  log2tlbndlog2  16142  birthdaylem3  16149  pellexlem2  16152  ppiqltx  16203  ppiqub  16215  chtqub  16218  mersenne  16219  perfectlem2  16222  bcmono  16226  bposlem1  16233  bposlem2  16234  zabsle1  16240  lgslem3  16243  lgsdirprm  16275  gausslemma2dlem1a  16299  lgseisen  16315  lgsquadlem2  16319  2sqlem8  16364  clwwlkext2edg  16785  clwwlknonex2lem2  16801  iooref1o  17205  trilpolemgt1  17210  trilpolemlt1  17212  trilpo  17214  redcwlpo  17227  neapmkvlem  17239  neapmkv  17240  taupi  17245