Theorem 0red 7410

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

Step	Hyp	Ref	Expression
1		0re 7409	. 2 ⊢ 0 ∈ ℝ
2	1	a1i 9	1 ⊢ (𝜑 → 0 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 1436  ℝcr 7270  0cc0 7271

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 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-1re 7360  ax-addrcl 7363  ax-rnegex 7375

This theorem depends on definitions:  df-bi 115  df-nf 1393  df-cleq 2078  df-clel 2081  df-ral 2360  df-rex 2361

This theorem is referenced by:  gt0ne0  7826  add20  7873  subge0  7874  lesub0  7878  addgt0d  7916  sublt0d  7965  gt0add  7968  apreap  7982  gt0ap0  8020  ap0gt0  8033  prodgt0  8225  prodge0  8227  lt2msq1  8258  lediv12a  8267  ledivp1  8276  squeeze0  8277  mulle0r  8317  nn2ge  8366  0mnnnnn0  8615  elnn0z  8673  rpgecl  9071  ge0p1rp  9074  ledivge1le  9112  iccf1o  9330  elfz1b  9411  elfz0fzfz0  9442  fz0fzelfz0  9443  fzo1fzo0n0  9497  elfzo0z  9498  fzofzim  9502  elfzodifsumelfzo  9515  btwnzge0  9610  modqid  9659  mulqaddmodid  9674  mulp1mod1  9675  modqltm1p1mod  9686  addmodlteq  9708  expival  9808  expgt1  9844  ltexp2a  9858  leexp2a  9859  expnbnd  9926  expnlbnd2  9928  expcanlem  9973  expcan  9974  resqrexlemcalc3  10290  resqrexlemnm  10292  resqrexlemgt0  10294  sqrtgt0  10308  abs00ap  10336  leabs  10348  ltabs  10361  abslt  10362  absle  10363  absgt0ap  10373  climge0  10551  dvdslelemd  10638  oddge22np1  10675  divalglemnn  10712  divalglemeuneg  10717  lcmgcdlem  10853  dvdsnprmd  10901  sqrt2irraplemnn  10951  sqrt2irrap  10952  qnumgt0  10970  znnen  11005