Theorem 1red 8307

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

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

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

This theorem is referenced by:  recgt0  9146  ltrec  9179  recp1lt1  9195  peano5nni  9262  peano2nn  9271  nn0p1gt0  9547  nn0ge2m1nn  9582  peano2z  9635  suprzclex  9699  ledivge1le  10082  lincmble  10361  iccf1o  10362  zltaddlt1le  10365  fznatpl1  10437  elfz1b  10451  fzonn0p1p1  10585  elfzom1p1elfzo  10586  zssinfcl  10619  exbtwnzlemstep  10636  exbtwnz  10639  rebtwn2zlemstep  10641  rebtwn2z  10643  qfraclt1  10669  flqaddz  10686  btwnzge0  10689  2tnp1ge0ge0  10690  flhalf  10691  fldiv4lem1div2uz2  10695  modqid  10740  m1modge3gt1  10762  modqltm1p1mod  10767  addmodlteq  10789  seq3f1olemqsumkj  10902  ltexp2a  10982  leexp2a  10983  leexp2r  10984  nnlesq  11034  resq01  11049  bernneq3  11054  expnbnd  11055  expnlbnd2  11057  nn0ltexp2  11101  expcanlem  11107  expcan  11108  bcval5  11155  ssenneg  11234  wrdlenge2n0  11290  sq01  11610  cvg1nlemcau  11700  resqrexlem1arp  11721  resqrexlemf1  11724  resqrexlemover  11726  resqrexlemdecn  11728  resqrexlemlo  11729  resqrexlemcalc2  11731  resqrexlemnm  11734  resqrexlemga  11739  reccn2ap  12029  sumsnf  12126  expcnvre  12220  geolim  12228  geolim2  12229  georeclim  12230  geoisumr  12235  geoisum1c  12237  cvgratnnlembern  12240  cvgratnnlemsumlt  12245  cvgratnnlemfm  12246  cvgratnnlemrate  12247  cvgratnn  12248  cvgratz  12249  prodsnf  12309  fprodrecl  12325  fprodreclf  12331  efcllemp  12375  efgt1  12414  eflegeo  12418  sinltxirr  12478  eirraplem  12494  p1modz1  12511  oddge22np1  12598  ltoddhalfle  12610  nno  12623  nn0oddm1d2  12626  nnoddm1d2  12627  bitsfzolem  12671  bitsfzo  12672  bitsmod  12673  bitscmp  12675  bitsinv1lem  12678  uzwodc  12764  coprmgcdb  12816  prmind2  12848  dvdsnprmd  12853  prmdc  12858  isprm5lem  12869  znege1  12906  sqrt2irrap  12908  divdenle  12925  nn0sqrtelqelz  12934  difsqpwdvds  13067  fldivp1  13077  pcfaclem  13078  4sqlem11  13130  4sqlem12  13131  2expltfac  13168  ballotfilemsgt1  13204  ballotfilemsel1i  13206  ballotfilemfrcn0  13223  oddennn  13233  exmidunben  13267  nninfdclemlt  13292  gsumshift  14111  znidomb  14938  psrbaglesuppg  14953  hoverlt1  15646  ivthdichlem  15648  dveflem  15723  reeff1oleme  15769  reeff1o  15770  cosz12  15777  sin0pilem2  15779  cos02pilt1  15848  rplogcl  15876  logdivlti  15878  cxplt  15913  cxple  15914  ltexp2  15938  logbrec  15957  logbgt0b  15963  logbgcd1irr  15964  logbgcd1irraplemexp  15965  logbgcd1irraplemap  15966  pellexlem2  15978  mersenne  15997  perfectlem2  16000  zabsle1  16004  lgslem3  16007  lgsdirprm  16039  gausslemma2dlem1a  16063  lgseisen  16079  lgsquadlem2  16083  2sqlem8  16128  clwwlkext2edg  16549  clwwlknonex2lem2  16565  iooref1o  16960  trilpolemgt1  16965  trilpolemlt1  16967  trilpo  16969  redcwlpo  16982  neapmkvlem  16994  neapmkv  16995  taupi  17000