Theorem 1red 8149

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 7986  1c1 7988

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

This theorem is referenced by:  recgt0  8985  ltrec  9018  recp1lt1  9034  peano5nni  9101  peano2nn  9110  nn0p1gt0  9386  nn0ge2m1nn  9417  peano2z  9470  suprzclex  9533  ledivge1le  9910  iccf1o  10188  zltaddlt1le  10191  fznatpl1  10260  elfz1b  10274  fzonn0p1p1  10406  elfzom1p1elfzo  10407  zssinfcl  10439  exbtwnzlemstep  10454  exbtwnz  10457  rebtwn2zlemstep  10459  rebtwn2z  10461  qfraclt1  10487  flqaddz  10504  btwnzge0  10507  2tnp1ge0ge0  10508  flhalf  10509  fldiv4lem1div2uz2  10513  modqid  10558  m1modge3gt1  10580  modqltm1p1mod  10585  addmodlteq  10607  seq3f1olemqsumkj  10720  ltexp2a  10800  leexp2a  10801  leexp2r  10802  nnlesq  10852  bernneq3  10871  expnbnd  10872  expnlbnd2  10874  nn0ltexp2  10918  expcanlem  10924  expcan  10925  bcval5  10972  wrdlenge2n0  11093  cvg1nlemcau  11481  resqrexlem1arp  11502  resqrexlemf1  11505  resqrexlemover  11507  resqrexlemdecn  11509  resqrexlemlo  11510  resqrexlemcalc2  11512  resqrexlemnm  11515  resqrexlemga  11520  reccn2ap  11810  sumsnf  11906  expcnvre  12000  geolim  12008  geolim2  12009  georeclim  12010  geoisumr  12015  geoisum1c  12017  cvgratnnlembern  12020  cvgratnnlemsumlt  12025  cvgratnnlemfm  12026  cvgratnnlemrate  12027  cvgratnn  12028  cvgratz  12029  prodsnf  12089  fprodrecl  12105  fprodreclf  12111  efcllemp  12155  efgt1  12194  eflegeo  12198  sinltxirr  12258  eirraplem  12274  p1modz1  12291  oddge22np1  12378  ltoddhalfle  12390  nno  12403  nn0oddm1d2  12406  nnoddm1d2  12407  bitsfzolem  12451  bitsfzo  12452  bitsmod  12453  bitscmp  12455  bitsinv1lem  12458  uzwodc  12544  coprmgcdb  12596  prmind2  12628  dvdsnprmd  12633  prmdc  12638  isprm5lem  12649  znege1  12686  sqrt2irrap  12688  divdenle  12705  nn0sqrtelqelz  12714  difsqpwdvds  12847  fldivp1  12857  pcfaclem  12858  4sqlem11  12910  4sqlem12  12911  2expltfac  12948  oddennn  12949  exmidunben  12983  nninfdclemlt  13008  znidomb  14607  psrbaglesuppg  14621  hoverlt1  15308  ivthdichlem  15310  dveflem  15385  reeff1oleme  15431  reeff1o  15432  cosz12  15439  sin0pilem2  15441  cos02pilt1  15510  rplogcl  15538  logdivlti  15540  cxplt  15575  cxple  15576  ltexp2  15600  logbrec  15619  logbgt0b  15625  logbgcd1irr  15626  logbgcd1irraplemexp  15627  logbgcd1irraplemap  15628  mersenne  15656  perfectlem2  15659  zabsle1  15663  lgslem3  15666  lgsdirprm  15698  gausslemma2dlem1a  15722  lgseisen  15738  lgsquadlem2  15742  2sqlem8  15787  iooref1o  16333  trilpolemgt1  16338  trilpolemlt1  16340  trilpo  16342  redcwlpo  16354  neapmkvlem  16366  neapmkv  16367  taupi  16372