Theorem 0red 8240

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 8239	. 2 |- 0 e. RR
2	1	a1i 9	1 |- ( ph -> 0 e. RR )

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8091   0cc0 8092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-1re 8186  ax-addrcl 8189  ax-rnegex 8201

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-cleq 2224  df-clel 2227  df-ral 2516  df-rex 2517

This theorem is referenced by:  gt0ne0  8666  add20  8713  subge0  8714  lesub0  8718  addgt0d  8760  sublt0d  8809  gt0add  8812  apreap  8826  gt0ap0  8865  ap0gt0  8879  lt0ap0  8887  prodgt0  9091  prodge0  9093  lt2msq1  9124  lediv12a  9133  ledivp1  9142  squeeze0  9143  mulle0r  9183  nn2ge  9235  0mnnnnn0  9493  elnn0z  9553  nn0negleid  9609  rpgecl  9978  ge0p1rp  9981  ledivge1le  10022  mul2lt0rlt0  10055  mul2lt0rgt0  10056  mul2lt0np  10059  iccf1o  10301  elfz1b  10387  elfz0fzfz0  10423  fz0fzelfz0  10424  fzo1fzo0n0  10485  elfzo0z  10486  fzofzim  10490  elfzodifsumelfzo  10509  btwnzge0  10623  modqid  10674  mulqaddmodid  10689  mulp1mod1  10690  modqltm1p1mod  10701  addmodlteq  10723  expgt1  10902  ltexp2a  10916  leexp2a  10917  expnbnd  10988  expnlbnd2  10990  zzlesq  11033  nn0ltexp2  11034  expcanlem  11040  expcan  11041  iswrdiz  11186  ccat2s1fvwd  11290  swrdswrdlem  11351  swrdswrd  11352  resqrexlemcalc3  11656  resqrexlemnm  11658  resqrexlemgt0  11660  sqrtgt0  11674  abs00ap  11702  leabs  11714  ltabs  11727  abslt  11728  absle  11729  absgt0ap  11739  rpmaxcl  11863  nn0maxcl  11865  rpmincl  11878  mul0inf  11881  reccn2ap  11953  climge0  11965  fsumrecl  12042  isumlessdc  12137  divcnv  12138  expcnvre  12144  absltap  12150  geolim2  12153  georeclim  12154  geoisumr  12159  cvgratnnlemnexp  12165  cvgratnnlemmn  12166  cvgratnnlemabsle  12168  mertenslem2  12177  cos12dec  12409  p1modz1  12435  dvdslelemd  12484  oddge22np1  12522  divalglemnn  12559  divalglemeuneg  12564  bitsfzolem  12595  bitsinv1lem  12602  lcmgcdlem  12729  dvdsnprmd  12777  isprm5lem  12793  sqrt2irraplemnn  12831  sqrt2irrap  12832  qnumgt0  12850  qexpz  13005  4sqlem6  13036  znnen  13099  ennnfoneleminc  13112  exmidunben  13127  mulcncflem  15418  hovercncf  15457  hovera  15458  hoverb  15459  hoverlt1  15460  hovergt0  15461  ivthdichlem  15462  dich0  15463  cosz12  15591  cos02pilt1  15662  ioocosf1o  15665  rplogcl  15690  cxplt  15727  cxple  15728  ltexp2  15752  mersenne  15811  lgsdilem  15846  gausslemma2dlem1a  15877  lgseisen  15893  lgsquadlem1  15896  lgsquadlem2  15897  refeq  16756  trilpolemeq1  16772  trilpolemlt1  16773  ltlenmkv  16803