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

Theorem 0red 7252
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 7251 . 2  |-  0  e.  RR
21a1i 9 1  |-  ( ph  ->  0  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434   RRcr 7112   0cc0 7113
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-1re 7202  ax-addrcl 7205  ax-rnegex 7217
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-cleq 2076  df-clel 2079  df-ral 2358  df-rex 2359
This theorem is referenced by:  gt0ne0  7668  add20  7715  subge0  7716  lesub0  7720  addgt0d  7758  sublt0d  7807  gt0add  7810  apreap  7824  gt0ap0  7862  ap0gt0  7875  prodgt0  8067  prodge0  8069  lt2msq1  8100  lediv12a  8109  ledivp1  8118  squeeze0  8119  mulle0r  8159  nn2ge  8208  0mnnnnn0  8457  elnn0z  8515  rpgecl  8913  ge0p1rp  8916  ledivge1le  8954  iccf1o  9172  elfz1b  9253  elfz0fzfz0  9284  fz0fzelfz0  9285  fzo1fzo0n0  9339  elfzo0z  9340  fzofzim  9344  elfzodifsumelfzo  9357  btwnzge0  9452  modqid  9501  mulqaddmodid  9516  mulp1mod1  9517  modqltm1p1mod  9528  addmodlteq  9550  expival  9645  expgt1  9681  ltexp2a  9695  leexp2a  9696  expnbnd  9763  expnlbnd2  9765  expcanlem  9810  expcan  9811  resqrexlemcalc3  10121  resqrexlemnm  10123  resqrexlemgt0  10125  sqrtgt0  10139  abs00ap  10167  leabs  10179  ltabs  10192  abslt  10193  absle  10194  absgt0ap  10204  climge0  10382  dvdslelemd  10469  oddge22np1  10506  divalglemnn  10543  divalglemeuneg  10548  lcmgcdlem  10684  dvdsnprmd  10732  sqrt2irraplemnn  10782  sqrt2irrap  10783  qnumgt0  10801  znnen  10836
  Copyright terms: Public domain W3C validator