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  9637  peano2z  9690  suprzclex  9755  ledivge1le  10144  lincmble  10423  iccf1o  10424  zltaddlt1le  10427  fznatpl1  10500  elfz1b  10514  fzonn0p1p1  10648  elfzom1p1elfzo  10649  zssinfcl  10682  exbtwnzlemstep  10699  exbtwnz  10702  rebtwn2zlemstep  10704  rebtwn2z  10706  qfraclt1  10734  flqaddz  10753  btwnzge0  10756  2tnp1ge0ge0  10757  flhalf  10758  fldiv4lem1div2uz2  10762  modqid  10807  m1modge3gt1  10829  modqltm1p1mod  10834  addmodlteq  10856  seq3f1olemqsumkj  10969  ltexp2a  11049  leexp2a  11050  leexp2r  11051  nnlesq  11101  resq01  11116  bernneq3  11121  expnbnd  11122  expnlbnd2  11124  nn0ltexp2  11169  expcanlem  11175  expcan  11176  bcval5  11223  ssenneg  11302  wrdlenge2n0  11362  sq01  11682  cvg1nlemcau  11772  resqrexlem1arp  11793  resqrexlemf1  11796  resqrexlemover  11798  resqrexlemdecn  11800  resqrexlemlo  11801  resqrexlemcalc2  11803  resqrexlemnm  11806  resqrexlemga  11811  reccn2ap  12104  sumsnf  12201  expcnvre  12295  geolim  12303  geolim2  12304  georeclim  12305  geoisumr  12310  geoisum1c  12312  cvgratnnlembern  12315  cvgratnnlemsumlt  12320  cvgratnnlemfm  12321  cvgratnnlemrate  12322  cvgratnn  12323  cvgratz  12324  prodsnf  12384  fprodrecl  12400  fprodreclf  12406  efcllemp  12450  efgt1  12489  eflegeo  12493  sinltxirr  12553  eirraplem  12569  p1modz1  12586  oddge22np1  12673  ltoddhalfle  12685  nno  12698  nn0oddm1d2  12701  nnoddm1d2  12702  bitsfzolem  12746  bitsfzo  12747  bitsmod  12748  bitscmp  12750  bitsinv1lem  12753  uzwodc  12839  coprmgcdb  12891  prmind2  12923  dvdsnprmd  12928  prmdc  12933  isprm5lem  12945  znege1  12983  sqrt2irrap  12985  divdenle  13002  nn0sqrtelqelz  13011  difsqpwdvds  13146  fldivp1  13156  pcfaclem  13157  4sqlem11  13209  4sqlem12  13210  2expltfac  13248  ballotfilemsgt1  13312  ballotfilemsel1i  13314  ballotfilemfrcn0  13331  oddennn  13341  exmidunben  13375  nninfdclemlt  13400  gzsumshift  14239  znidomb  15102  psrbaglesuppg  15171  hoverlt1  15908  ivthdichlem  15910  dveflem  15985  reeff1oleme  16031  reeff1o  16032  efap1p  16038  cosz12  16040  sin0pilem2  16042  cos02pilt1  16112  rplogcl  16142  logdivlti  16144  logdivlt  16157  cxplt  16184  cxple  16185  ltexp2  16210  logbrec  16229  logbgt0b  16235  logbgcd1irr  16236  logbgcd1irraplemexp  16237  logbgcd1irraplemap  16238  zprmlogbaplem1  16248  zprmlogbaplem2  16249  log2tlbndlog2  16253  birthdaylem3  16260  pellexlem2  16263  ppiqltx  16314  ppiqub  16326  chtqub  16329  mersenne  16330  perfectlem2  16333  bcmono  16337  bposlem1  16344  bposlem2  16345  zabsle1  16356  lgslem3  16359  lgsdirprm  16391  gausslemma2dlem1a  16415  lgseisen  16431  lgsquadlem2  16435  2sqlem8  16480  clwwlkext2edg  16901  clwwlknonex2lem2  16917  iooref1o  17322  trilpolemgt1  17328  trilpolemlt1  17330  trilpo  17332  redcwlpo  17345  neapmkvlem  17357  neapmkv  17358  taupi  17363