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

Theorem 0red 7085
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 7084 . 2 0 ∈ ℝ
21a1i 9 1 (𝜑 → 0 ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1409  cr 6945  0cc0 6946
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-1re 7035  ax-addrcl 7038  ax-rnegex 7050
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-cleq 2049  df-clel 2052  df-ral 2328  df-rex 2329
This theorem is referenced by:  gt0ne0  7495  add20  7542  subge0  7543  lesub0  7547  addgt0d  7585  sublt0d  7634  gt0add  7637  apreap  7651  gt0ap0  7689  ap0gt0  7702  prodgt0  7892  prodge0  7894  lt2msq1  7925  lediv12a  7934  ledivp1  7943  squeeze0  7944  mulle0r  7984  nn2ge  8021  0mnnnnn0  8270  elnn0z  8314  rpgecl  8708  ge0p1rp  8711  ledivge1le  8749  iccf1o  8972  elfz1b  9053  elfz0fzfz0  9084  fz0fzelfz0  9085  fzo1fzo0n0  9140  elfzo0z  9141  fzofzim  9145  elfzodifsumelfzo  9158  btwnzge0  9249  modqid  9298  mulqaddmodid  9313  mulp1mod1  9314  modqltm1p1mod  9325  addmodlteq  9347  expival  9421  expgt1  9457  ltexp2a  9471  leexp2a  9472  expnbnd  9539  expnlbnd2  9541  resqrexlemcalc3  9842  resqrexlemnm  9844  resqrexlemgt0  9846  sqrtgt0  9860  abs00ap  9888  leabs  9900  ltabs  9913  abslt  9914  absle  9915  absgt0ap  9925  climge0  10075  dvdslelemd  10154  oddge22np1  10192
  Copyright terms: Public domain W3C validator