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

Theorem 1red 7774
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 7758 . 2  |-  1  e.  RR
21a1i 9 1  |-  ( ph  ->  1  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1480   RRcr 7612   1c1 7614
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1re 7707
This theorem is referenced by:  recgt0  8601  ltrec  8634  recp1lt1  8650  peano5nni  8716  peano2nn  8725  nn0p1gt0  8999  nn0ge2m1nn  9030  peano2z  9083  suprzclex  9142  ledivge1le  9506  iccf1o  9780  zltaddlt1le  9782  fznatpl1  9849  elfz1b  9863  fzonn0p1p1  9983  elfzom1p1elfzo  9984  exbtwnzlemstep  10018  exbtwnz  10021  rebtwn2zlemstep  10023  rebtwn2z  10025  qfraclt1  10046  flqaddz  10063  btwnzge0  10066  2tnp1ge0ge0  10067  flhalf  10068  modqid  10115  m1modge3gt1  10137  modqltm1p1mod  10142  addmodlteq  10164  seq3f1olemqsumkj  10264  ltexp2a  10338  leexp2a  10339  leexp2r  10340  nnlesq  10389  bernneq3  10407  expnbnd  10408  expnlbnd2  10410  expcanlem  10455  expcan  10456  bcval5  10502  cvg1nlemcau  10749  resqrexlem1arp  10770  resqrexlemf1  10773  resqrexlemover  10775  resqrexlemdecn  10777  resqrexlemlo  10778  resqrexlemcalc2  10780  resqrexlemnm  10783  resqrexlemga  10788  reccn2ap  11075  sumsnf  11171  expcnvre  11265  geolim  11273  geolim2  11274  georeclim  11275  geoisumr  11280  geoisum1c  11282  cvgratnnlembern  11285  cvgratnnlemsumlt  11290  cvgratnnlemfm  11291  cvgratnnlemrate  11292  cvgratnn  11293  cvgratz  11294  efcllemp  11349  efgt1  11388  eflegeo  11393  eirraplem  11468  oddge22np1  11563  ltoddhalfle  11575  nno  11588  nn0oddm1d2  11591  nnoddm1d2  11592  zssinfcl  11626  coprmgcdb  11754  prmind2  11786  dvdsnprmd  11791  znege1  11841  sqrt2irrap  11843  divdenle  11860  nn0sqrtelqelz  11869  oddennn  11890  exmidunben  11924  dveflem  12840  cosz12  12846  sin0pilem2  12848  cos02pilt1  12917  trilpolemgt1  13217  trilpolemlt1  13219  trilpo  13221  taupi  13224
  Copyright terms: Public domain W3C validator