Theorem 1red 8305

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℝcr 8142  1c1 8144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1re 8237

This theorem is referenced by:  recgt0  9144  ltrec  9177  recp1lt1  9193  peano5nni  9260  peano2nn  9269  nn0p1gt0  9545  nn0ge2m1nn  9580  peano2z  9633  suprzclex  9697  ledivge1le  10080  lincmble  10359  iccf1o  10360  zltaddlt1le  10363  fznatpl1  10435  elfz1b  10449  fzonn0p1p1  10583  elfzom1p1elfzo  10584  zssinfcl  10617  exbtwnzlemstep  10634  exbtwnz  10637  rebtwn2zlemstep  10639  rebtwn2z  10641  qfraclt1  10667  flqaddz  10684  btwnzge0  10687  2tnp1ge0ge0  10688  flhalf  10689  fldiv4lem1div2uz2  10693  modqid  10738  m1modge3gt1  10760  modqltm1p1mod  10765  addmodlteq  10787  seq3f1olemqsumkj  10900  ltexp2a  10980  leexp2a  10981  leexp2r  10982  nnlesq  11032  resq01  11047  bernneq3  11052  expnbnd  11053  expnlbnd2  11055  nn0ltexp2  11099  expcanlem  11105  expcan  11106  bcval5  11153  ssenneg  11232  wrdlenge2n0  11288  sq01  11608  cvg1nlemcau  11698  resqrexlem1arp  11719  resqrexlemf1  11722  resqrexlemover  11724  resqrexlemdecn  11726  resqrexlemlo  11727  resqrexlemcalc2  11729  resqrexlemnm  11732  resqrexlemga  11737  reccn2ap  12027  sumsnf  12124  expcnvre  12218  geolim  12226  geolim2  12227  georeclim  12228  geoisumr  12233  geoisum1c  12235  cvgratnnlembern  12238  cvgratnnlemsumlt  12243  cvgratnnlemfm  12244  cvgratnnlemrate  12245  cvgratnn  12246  cvgratz  12247  prodsnf  12307  fprodrecl  12323  fprodreclf  12329  efcllemp  12373  efgt1  12412  eflegeo  12416  sinltxirr  12476  eirraplem  12492  p1modz1  12509  oddge22np1  12596  ltoddhalfle  12608  nno  12621  nn0oddm1d2  12624  nnoddm1d2  12625  bitsfzolem  12669  bitsfzo  12670  bitsmod  12671  bitscmp  12673  bitsinv1lem  12676  uzwodc  12762  coprmgcdb  12814  prmind2  12846  dvdsnprmd  12851  prmdc  12856  isprm5lem  12867  znege1  12904  sqrt2irrap  12906  divdenle  12923  nn0sqrtelqelz  12932  difsqpwdvds  13065  fldivp1  13075  pcfaclem  13076  4sqlem11  13128  4sqlem12  13129  2expltfac  13166  ballotfilemsgt1  13202  ballotfilemsel1i  13204  ballotfilemfrcn0  13221  oddennn  13231  exmidunben  13265  nninfdclemlt  13290  gsumshift  14109  znidomb  14936  psrbaglesuppg  14951  hoverlt1  15644  ivthdichlem  15646  dveflem  15721  reeff1oleme  15767  reeff1o  15768  cosz12  15775  sin0pilem2  15777  cos02pilt1  15846  rplogcl  15874  logdivlti  15876  cxplt  15911  cxple  15912  ltexp2  15936  logbrec  15955  logbgt0b  15961  logbgcd1irr  15962  logbgcd1irraplemexp  15963  logbgcd1irraplemap  15964  pellexlem2  15976  mersenne  15995  perfectlem2  15998  zabsle1  16002  lgslem3  16005  lgsdirprm  16037  gausslemma2dlem1a  16061  lgseisen  16077  lgsquadlem2  16081  2sqlem8  16126  clwwlkext2edg  16547  clwwlknonex2lem2  16563  iooref1o  16958  trilpolemgt1  16963  trilpolemlt1  16965  trilpo  16967  redcwlpo  16980  neapmkvlem  16992  neapmkv  16993  taupi  16998