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

Theorem 0red 7731
Description: 0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
0red (𝜑 → 0 ∈ ℝ)

Proof of Theorem 0red
StepHypRef Expression
1 0re 7730 . 2 0 ∈ ℝ
21a1i 9 1 (𝜑 → 0 ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1463  cr 7583  0cc0 7584
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-1re 7678  ax-addrcl 7681  ax-rnegex 7693
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-cleq 2108  df-clel 2111  df-ral 2396  df-rex 2397
This theorem is referenced by:  gt0ne0  8153  add20  8200  subge0  8201  lesub0  8205  addgt0d  8246  sublt0d  8295  gt0add  8298  apreap  8312  gt0ap0  8351  ap0gt0  8364  prodgt0  8567  prodge0  8569  lt2msq1  8600  lediv12a  8609  ledivp1  8618  squeeze0  8619  mulle0r  8659  nn2ge  8710  0mnnnnn0  8960  elnn0z  9018  rpgecl  9418  ge0p1rp  9421  ledivge1le  9459  iccf1o  9727  elfz1b  9810  elfz0fzfz0  9843  fz0fzelfz0  9844  fzo1fzo0n0  9900  elfzo0z  9901  fzofzim  9905  elfzodifsumelfzo  9918  btwnzge0  10013  modqid  10062  mulqaddmodid  10077  mulp1mod1  10078  modqltm1p1mod  10089  addmodlteq  10111  expgt1  10271  ltexp2a  10285  leexp2a  10286  expnbnd  10355  expnlbnd2  10357  expcanlem  10402  expcan  10403  resqrexlemcalc3  10728  resqrexlemnm  10730  resqrexlemgt0  10732  sqrtgt0  10746  abs00ap  10774  leabs  10786  ltabs  10799  abslt  10800  absle  10801  absgt0ap  10811  rpmaxcl  10935  rpmincl  10949  mul0inf  10952  reccn2ap  11022  climge0  11034  fsumrecl  11110  isumlessdc  11205  divcnv  11206  expcnvre  11212  absltap  11218  geolim2  11221  georeclim  11222  geoisumr  11227  cvgratnnlemnexp  11233  cvgratnnlemmn  11234  cvgratnnlemabsle  11236  mertenslem2  11245  dvdslelemd  11437  oddge22np1  11474  divalglemnn  11511  divalglemeuneg  11516  lcmgcdlem  11654  dvdsnprmd  11702  sqrt2irraplemnn  11752  sqrt2irrap  11753  qnumgt0  11771  znnen  11806  ennnfoneleminc  11819  exmidunben  11834  mulcncflem  12654  refeq  13025  trilpolemeq1  13035  trilpolemlt1  13036
  Copyright terms: Public domain W3C validator