Theorem 1red 8348

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

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

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

This theorem is used by:  recgt0  9189  ltrec  9222  recp1lt1  9238  indfdc  9308  peano5nni  9317  peano2nn  9326  nn0p1gt0  9604  nn0ge2m1nn  9639  peano2z  9692  suprzclex  9756  ledivge1le  10145  lincmble  10424  iccf1o  10425  zltaddlt1le  10428  fznatpl1  10501  elfz1b  10515  fzonn0p1p1  10649  elfzom1p1elfzo  10650  zssinfcl  10683  exbtwnzlemstep  10700  exbtwnz  10703  rebtwn2zlemstep  10705  rebtwn2z  10707  qfraclt1  10735  flqaddz  10754  btwnzge0  10757  2tnp1ge0ge0  10758  flhalf  10759  fldiv4lem1div2uz2  10763  modqid  10808  m1modge3gt1  10830  modqltm1p1mod  10835  addmodlteq  10857  seq3f1olemqsumkj  10970  ltexp2a  11050  leexp2a  11051  leexp2r  11052  nnlesq  11102  resq01  11117  bernneq3  11122  expnbnd  11123  expnlbnd2  11125  nn0ltexp2  11170  expcanlem  11176  expcan  11177  bcval5  11224  ssenneg  11303  wrdlenge2n0  11363  sq01  11683  cvg1nlemcau  11773  resqrexlem1arp  11794  resqrexlemf1  11797  resqrexlemover  11799  resqrexlemdecn  11801  resqrexlemlo  11802  resqrexlemcalc2  11804  resqrexlemnm  11807  resqrexlemga  11812  reccn2ap  12105  sumsnf  12202  expcnvre  12296  geolim  12304  geolim2  12305  georeclim  12306  geoisumr  12311  geoisum1c  12313  cvgratnnlembern  12316  cvgratnnlemsumlt  12321  cvgratnnlemfm  12322  cvgratnnlemrate  12323  cvgratnn  12324  cvgratz  12325  prodsnf  12385  fprodrecl  12401  fprodreclf  12407  efcllemp  12451  efgt1  12490  eflegeo  12494  sinltxirr  12554  eirraplem  12570  p1modz1  12587  oddge22np1  12674  ltoddhalfle  12686  nno  12699  nn0oddm1d2  12702  nnoddm1d2  12703  bitsfzolem  12747  bitsfzo  12748  bitsmod  12749  bitscmp  12751  bitsinv1lem  12754  uzwodc  12840  coprmgcdb  12892  prmind2  12924  dvdsnprmd  12929  prmdc  12934  isprm5lem  12946  znege1  12984  sqrt2irrap  12986  divdenle  13003  nn0sqrtelqelz  13012  difsqpwdvds  13147  fldivp1  13157  pcfaclem  13158  4sqlem11  13210  4sqlem12  13211  2expltfac  13249  ballotfilemsgt1  13313  ballotfilemsel1i  13315  ballotfilemfrcn0  13332  oddennn  13342  exmidunben  13376  nninfdclemlt  13401  gzsumshift  14240  znidomb  15103  psrbaglesuppg  15172  hoverlt1  15887  ivthdichlem  15889  dveflem  15964  reeff1oleme  16010  reeff1o  16011  efap1p  16017  cosz12  16019  sin0pilem2  16021  cos02pilt1  16091  rplogcl  16121  logdivlti  16123  logdivlt  16136  cxplt  16163  cxple  16164  ltexp2  16189  logbrec  16208  logbgt0b  16214  logbgcd1irr  16215  logbgcd1irraplemexp  16216  logbgcd1irraplemap  16217  zprmlogbaplem1  16227  zprmlogbaplem2  16228  log2tlbndlog2  16232  birthdaylem3  16239  pellexlem2  16242  ppiqltx  16293  ppiqub  16305  chtqub  16308  mersenne  16309  perfectlem2  16312  bcmono  16316  bposlem1  16323  bposlem2  16324  zabsle1  16335  lgslem3  16338  lgsdirprm  16370  gausslemma2dlem1a  16394  lgseisen  16410  lgsquadlem2  16414  2sqlem8  16459  clwwlkext2edg  16880  clwwlknonex2lem2  16896  iooref1o  17301  trilpolemgt1  17307  trilpolemlt1  17309  trilpo  17311  redcwlpo  17324  neapmkvlem  17336  neapmkv  17337  taupi  17342