Theorem 1red 7134

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

Syntax hints:   → wi 4   ∈ wcel 1433  ℝcr 6980  1c1 6982

This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-1re 7070

This theorem is referenced by:  recgt0  7928  ltrec  7961  recp1lt1  7977  peano5nni  8042  peano2nn  8051  nn0p1gt0  8317  nn0ge2m1nn  8348  peano2z  8387  suprzclex  8445  ledivge1le  8803  iccf1o  9026  zltaddlt1le  9028  fznatpl1  9093  elfz1b  9107  fzonn0p1p1  9222  elfzom1p1elfzo  9223  qbtwnzlemstep  9257  qbtwnz  9260  rebtwn2zlemstep  9261  rebtwn2z  9263  qfraclt1  9282  flqaddz  9299  btwnzge0  9302  2tnp1ge0ge0  9303  flhalf  9304  modqid  9351  m1modge3gt1  9373  modqltm1p1mod  9378  addmodlteq  9400  ltexp2a  9528  leexp2a  9529  leexp2r  9530  nnlesq  9578  bernneq3  9595  expnbnd  9596  expnlbnd2  9598  expcanlem  9643  expcan  9644  ibcval5  9690  cvg1nlemcau  9870  resqrexlem1arp  9891  resqrexlemf1  9894  resqrexlemover  9896  resqrexlemdecn  9898  resqrexlemlo  9899  resqrexlemcalc2  9901  resqrexlemnm  9904  resqrexlemga  9909  oddge22np1  10281  ltoddhalfle  10293  nno  10306  nn0oddm1d2  10309  nnoddm1d2  10310  zssinfcl  10344  coprmgcdb  10470  prmind2  10502  dvdsnprmd  10507  znege1  10556  sqrt2irrap  10558