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

Theorem 0red 7028
 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 7027 . 2 0 ∈ ℝ
21a1i 9 1 (𝜑 → 0 ∈ ℝ)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 1393  ℝcr 6888  0cc0 6889 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-1re 6978  ax-addrcl 6981  ax-rnegex 6993 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-cleq 2033  df-clel 2036  df-ral 2311  df-rex 2312 This theorem is referenced by:  gt0ne0  7422  add20  7469  subge0  7470  lesub0  7474  addgt0d  7512  sublt0d  7561  gt0add  7564  apreap  7578  gt0ap0  7616  ap0gt0  7629  prodgt0  7818  prodge0  7820  lt2msq1  7851  lediv12a  7860  ledivp1  7869  squeeze0  7870  nn2ge  7946  0mnnnnn0  8214  elnn0z  8258  rpgecl  8611  ge0p1rp  8614  ledivge1le  8652  iccf1o  8872  elfz1b  8952  elfz0fzfz0  8983  fz0fzelfz0  8984  fzo1fzo0n0  9039  elfzo0z  9040  fzofzim  9044  elfzodifsumelfzo  9057  btwnzge0  9142  expival  9257  expgt1  9293  ltexp2a  9306  leexp2a  9307  expnbnd  9372  expnlbnd2  9374  resqrexlemcalc3  9614  resqrexlemnm  9616  resqrexlemgt0  9618  sqrtgt0  9632  abs00ap  9660  leabs  9672  ltabs  9683  abslt  9684  absle  9685  absgt0ap  9695  climge0  9845
 Copyright terms: Public domain W3C validator