Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  1red GIF version

Theorem 1red 7099
 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
StepHypRef Expression
1 1re 7083 . 2 1 ∈ ℝ
21a1i 9 1 (𝜑 → 1 ∈ ℝ)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 1409  ℝcr 6945  1c1 6947 This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-1re 7035 This theorem is referenced by:  recgt0  7890  ltrec  7923  recp1lt1  7939  peano5nni  7992  peano2nn  8001  nn0p1gt0  8267  nn0ge2m1nn  8298  peano2z  8337  ledivge1le  8749  iccf1o  8972  zltaddlt1le  8974  fznatpl1  9039  elfz1b  9053  fzonn0p1p1  9170  elfzom1p1elfzo  9171  qbtwnzlemstep  9204  qbtwnz  9207  rebtwn2zlemstep  9208  rebtwn2z  9210  qfraclt1  9229  flqaddz  9246  btwnzge0  9249  2tnp1ge0ge0  9250  flhalf  9251  modqid  9298  m1modge3gt1  9320  modqltm1p1mod  9325  addmodlteq  9347  ltexp2a  9471  leexp2a  9472  leexp2r  9473  nnlesq  9521  bernneq3  9538  expnbnd  9539  expnlbnd2  9541  ibcval5  9630  cvg1nlemcau  9810  resqrexlem1arp  9831  resqrexlemf1  9834  resqrexlemover  9836  resqrexlemdecn  9838  resqrexlemlo  9839  resqrexlemcalc2  9841  resqrexlemnm  9844  resqrexlemga  9849  oddge22np1  10192  ltoddhalfle  10204  nno  10217  nn0oddm1d2  10220  nnoddm1d2  10221
 Copyright terms: Public domain W3C validator