Theorem 0red 7120

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

Step	Hyp	Ref	Expression
1		0re 7119	. 2 |- 0 e. RR
2	1	a1i 9	1 |- ( ph -> 0 e. RR )

Syntax hints:   -> wi 4   e. wcel 1433   RRcr 6980   0cc0 6981

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-1re 7070  ax-addrcl 7073  ax-rnegex 7085

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-cleq 2074  df-clel 2077  df-ral 2353  df-rex 2354

This theorem is referenced by:  gt0ne0  7531  add20  7578  subge0  7579  lesub0  7583  addgt0d  7621  sublt0d  7670  gt0add  7673  apreap  7687  gt0ap0  7725  ap0gt0  7738  prodgt0  7930  prodge0  7932  lt2msq1  7963  lediv12a  7972  ledivp1  7981  squeeze0  7982  mulle0r  8022  nn2ge  8071  0mnnnnn0  8320  elnn0z  8364  rpgecl  8762  ge0p1rp  8765  ledivge1le  8803  iccf1o  9026  elfz1b  9107  elfz0fzfz0  9137  fz0fzelfz0  9138  fzo1fzo0n0  9192  elfzo0z  9193  fzofzim  9197  elfzodifsumelfzo  9210  btwnzge0  9302  modqid  9351  mulqaddmodid  9366  mulp1mod1  9367  modqltm1p1mod  9378  addmodlteq  9400  expival  9478  expgt1  9514  ltexp2a  9528  leexp2a  9529  expnbnd  9596  expnlbnd2  9598  expcanlem  9643  expcan  9644  resqrexlemcalc3  9902  resqrexlemnm  9904  resqrexlemgt0  9906  sqrtgt0  9920  abs00ap  9948  leabs  9960  ltabs  9973  abslt  9974  absle  9975  absgt0ap  9985  climge0  10163  dvdslelemd  10243  oddge22np1  10281  divalglemnn  10318  divalglemeuneg  10323  lcmgcdlem  10459  dvdsnprmd  10507  sqrt2irraplemnn  10557  sqrt2irrap  10558