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

Theorem 1red 7100
Description: 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
1red  |-  ( ph  ->  1  e.  RR )

Proof of Theorem 1red
StepHypRef Expression
1 1re 7084 . 2  |-  1  e.  RR
21a1i 9 1  |-  ( ph  ->  1  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1409   RRcr 6946   1c1 6948
This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-1re 7036
This theorem is referenced by:  recgt0  7891  ltrec  7924  recp1lt1  7940  peano5nni  7993  peano2nn  8002  nn0p1gt0  8268  nn0ge2m1nn  8299  peano2z  8338  ledivge1le  8750  iccf1o  8973  zltaddlt1le  8975  fznatpl1  9040  elfz1b  9054  fzonn0p1p1  9171  elfzom1p1elfzo  9172  qbtwnzlemstep  9205  qbtwnz  9208  rebtwn2zlemstep  9209  rebtwn2z  9211  qfraclt1  9230  flqaddz  9247  btwnzge0  9250  2tnp1ge0ge0  9251  flhalf  9252  modqid  9299  m1modge3gt1  9321  modqltm1p1mod  9326  addmodlteq  9348  ltexp2a  9472  leexp2a  9473  leexp2r  9474  nnlesq  9522  bernneq3  9539  expnbnd  9540  expnlbnd2  9542  ibcval5  9631  cvg1nlemcau  9811  resqrexlem1arp  9832  resqrexlemf1  9835  resqrexlemover  9837  resqrexlemdecn  9839  resqrexlemlo  9840  resqrexlemcalc2  9842  resqrexlemnm  9845  resqrexlemga  9850  oddge22np1  10193  ltoddhalfle  10205  nno  10218  nn0oddm1d2  10221  nnoddm1d2  10222
  Copyright terms: Public domain W3C validator