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

Theorem 0red 7774
Description:  0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
0red  |-  ( ph  ->  0  e.  RR )

Proof of Theorem 0red
StepHypRef Expression
1 0re 7773 . 2  |-  0  e.  RR
21a1i 9 1  |-  ( ph  ->  0  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1480   RRcr 7626   0cc0 7627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-1re 7721  ax-addrcl 7724  ax-rnegex 7736
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-cleq 2132  df-clel 2135  df-ral 2421  df-rex 2422
This theorem is referenced by:  gt0ne0  8196  add20  8243  subge0  8244  lesub0  8248  addgt0d  8290  sublt0d  8339  gt0add  8342  apreap  8356  gt0ap0  8395  ap0gt0  8409  lt0ap0  8417  prodgt0  8617  prodge0  8619  lt2msq1  8650  lediv12a  8659  ledivp1  8668  squeeze0  8669  mulle0r  8709  nn2ge  8760  0mnnnnn0  9016  elnn0z  9074  rpgecl  9477  ge0p1rp  9480  ledivge1le  9520  mul2lt0rlt0  9553  mul2lt0rgt0  9554  mul2lt0np  9557  iccf1o  9794  elfz1b  9877  elfz0fzfz0  9910  fz0fzelfz0  9911  fzo1fzo0n0  9967  elfzo0z  9968  fzofzim  9972  elfzodifsumelfzo  9985  btwnzge0  10080  modqid  10129  mulqaddmodid  10144  mulp1mod1  10145  modqltm1p1mod  10156  addmodlteq  10178  expgt1  10338  ltexp2a  10352  leexp2a  10353  expnbnd  10422  expnlbnd2  10424  expcanlem  10469  expcan  10470  resqrexlemcalc3  10795  resqrexlemnm  10797  resqrexlemgt0  10799  sqrtgt0  10813  abs00ap  10841  leabs  10853  ltabs  10866  abslt  10867  absle  10868  absgt0ap  10878  rpmaxcl  11002  rpmincl  11016  mul0inf  11019  reccn2ap  11089  climge0  11101  fsumrecl  11177  isumlessdc  11272  divcnv  11273  expcnvre  11279  absltap  11285  geolim2  11288  georeclim  11289  geoisumr  11294  cvgratnnlemnexp  11300  cvgratnnlemmn  11301  cvgratnnlemabsle  11303  mertenslem2  11312  cos12dec  11480  dvdslelemd  11547  oddge22np1  11584  divalglemnn  11621  divalglemeuneg  11626  lcmgcdlem  11764  dvdsnprmd  11812  sqrt2irraplemnn  11863  sqrt2irrap  11864  qnumgt0  11882  znnen  11917  ennnfoneleminc  11930  exmidunben  11945  mulcncflem  12768  cosz12  12877  cos02pilt1  12948  ioocosf1o  12951  rplogcl  12971  refeq  13276  trilpolemeq1  13286  trilpolemlt1  13287
  Copyright terms: Public domain W3C validator