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  10747  btwnzge0  10750  2tnp1ge0ge0  10751  flhalf  10752  fldiv4lem1div2uz2  10756  modqid  10801  m1modge3gt1  10823  modqltm1p1mod  10828  addmodlteq  10850  seq3f1olemqsumkj  10963  ltexp2a  11043  leexp2a  11044  leexp2r  11045  nnlesq  11095  resq01  11110  bernneq3  11115  expnbnd  11116  expnlbnd2  11118  nn0ltexp2  11163  expcanlem  11169  expcan  11170  bcval5  11217  ssenneg  11296  wrdlenge2n0  11356  sq01  11676  cvg1nlemcau  11766  resqrexlem1arp  11787  resqrexlemf1  11790  resqrexlemover  11792  resqrexlemdecn  11794  resqrexlemlo  11795  resqrexlemcalc2  11797  resqrexlemnm  11800  resqrexlemga  11805  reccn2ap  12098  sumsnf  12195  expcnvre  12289  geolim  12297  geolim2  12298  georeclim  12299  geoisumr  12304  geoisum1c  12306  cvgratnnlembern  12309  cvgratnnlemsumlt  12314  cvgratnnlemfm  12315  cvgratnnlemrate  12316  cvgratnn  12317  cvgratz  12318  prodsnf  12378  fprodrecl  12394  fprodreclf  12400  efcllemp  12444  efgt1  12483  eflegeo  12487  sinltxirr  12547  eirraplem  12563  p1modz1  12580  oddge22np1  12667  ltoddhalfle  12679  nno  12692  nn0oddm1d2  12695  nnoddm1d2  12696  bitsfzolem  12740  bitsfzo  12741  bitsmod  12742  bitscmp  12744  bitsinv1lem  12747  uzwodc  12833  coprmgcdb  12885  prmind2  12917  dvdsnprmd  12922  prmdc  12927  isprm5lem  12939  znege1  12977  sqrt2irrap  12979  divdenle  12996  nn0sqrtelqelz  13005  difsqpwdvds  13140  fldivp1  13150  pcfaclem  13151  4sqlem11  13203  4sqlem12  13204  2expltfac  13242  ballotfilemsgt1  13306  ballotfilemsel1i  13308  ballotfilemfrcn0  13325  oddennn  13335  exmidunben  13369  nninfdclemlt  13394  gzsumshift  14233  znidomb  15077  psrbaglesuppg  15141  hoverlt1  15841  ivthdichlem  15843  dveflem  15918  reeff1oleme  15964  reeff1o  15965  efap1p  15971  cosz12  15973  sin0pilem2  15975  cos02pilt1  16045  rplogcl  16075  logdivlti  16077  logdivlt  16090  cxplt  16117  cxple  16118  ltexp2  16143  logbrec  16162  logbgt0b  16168  logbgcd1irr  16169  logbgcd1irraplemexp  16170  logbgcd1irraplemap  16171  zprmlogbaplem1  16181  zprmlogbaplem2  16182  log2tlbndlog2  16186  birthdaylem3  16193  pellexlem2  16196  ppiqltx  16247  ppiqub  16259  chtqub  16262  mersenne  16263  perfectlem2  16266  bcmono  16270  bposlem1  16277  bposlem2  16278  zabsle1  16289  lgslem3  16292  lgsdirprm  16324  gausslemma2dlem1a  16348  lgseisen  16364  lgsquadlem2  16368  2sqlem8  16413  clwwlkext2edg  16834  clwwlknonex2lem2  16850  iooref1o  17254  trilpolemgt1  17260  trilpolemlt1  17262  trilpo  17264  redcwlpo  17277  neapmkvlem  17289  neapmkv  17290  taupi  17295