Theorem 1red 7974

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℝcr 7812  1c1 7814

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

This theorem is referenced by:  recgt0  8809  ltrec  8842  recp1lt1  8858  peano5nni  8924  peano2nn  8933  nn0p1gt0  9207  nn0ge2m1nn  9238  peano2z  9291  suprzclex  9353  ledivge1le  9728  iccf1o  10006  zltaddlt1le  10009  fznatpl1  10078  elfz1b  10092  fzonn0p1p1  10215  elfzom1p1elfzo  10216  exbtwnzlemstep  10250  exbtwnz  10253  rebtwn2zlemstep  10255  rebtwn2z  10257  qfraclt1  10282  flqaddz  10299  btwnzge0  10302  2tnp1ge0ge0  10303  flhalf  10304  modqid  10351  m1modge3gt1  10373  modqltm1p1mod  10378  addmodlteq  10400  seq3f1olemqsumkj  10500  ltexp2a  10574  leexp2a  10575  leexp2r  10576  nnlesq  10626  bernneq3  10645  expnbnd  10646  expnlbnd2  10648  nn0ltexp2  10691  expcanlem  10697  expcan  10698  bcval5  10745  cvg1nlemcau  10995  resqrexlem1arp  11016  resqrexlemf1  11019  resqrexlemover  11021  resqrexlemdecn  11023  resqrexlemlo  11024  resqrexlemcalc2  11026  resqrexlemnm  11029  resqrexlemga  11034  reccn2ap  11323  sumsnf  11419  expcnvre  11513  geolim  11521  geolim2  11522  georeclim  11523  geoisumr  11528  geoisum1c  11530  cvgratnnlembern  11533  cvgratnnlemsumlt  11538  cvgratnnlemfm  11539  cvgratnnlemrate  11540  cvgratnn  11541  cvgratz  11542  prodsnf  11602  fprodrecl  11618  fprodreclf  11624  efcllemp  11668  efgt1  11707  eflegeo  11711  eirraplem  11786  p1modz1  11803  oddge22np1  11888  ltoddhalfle  11900  nno  11913  nn0oddm1d2  11916  nnoddm1d2  11917  zssinfcl  11951  uzwodc  12040  coprmgcdb  12090  prmind2  12122  dvdsnprmd  12127  prmdc  12132  isprm5lem  12143  znege1  12180  sqrt2irrap  12182  divdenle  12199  nn0sqrtelqelz  12208  difsqpwdvds  12339  fldivp1  12348  pcfaclem  12349  oddennn  12395  exmidunben  12429  nninfdclemlt  12454  dveflem  14272  reeff1oleme  14278  reeff1o  14279  cosz12  14286  sin0pilem2  14288  cos02pilt1  14357  rplogcl  14385  logdivlti  14387  cxplt  14421  cxple  14422  ltexp2  14445  logbrec  14463  logbgt0b  14469  logbgcd1irr  14470  logbgcd1irraplemexp  14471  logbgcd1irraplemap  14472  zabsle1  14485  lgslem3  14488  lgsdirprm  14520  2sqlem8  14555  iooref1o  14867  trilpolemgt1  14872  trilpolemlt1  14874  trilpo  14876  redcwlpo  14888  neapmkvlem  14900  neapmkv  14901  taupi  14906