Theorem 0red 7933

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 7932	. 2 ⊢ 0 ∈ ℝ
2	1	a1i 9	1 ⊢ (𝜑 → 0 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2146  ℝcr 7785  0cc0 7786

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 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-17 1524  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-1re 7880  ax-addrcl 7883  ax-rnegex 7895

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-cleq 2168  df-clel 2171  df-ral 2458  df-rex 2459

This theorem is referenced by:  gt0ne0  8358  add20  8405  subge0  8406  lesub0  8410  addgt0d  8452  sublt0d  8501  gt0add  8504  apreap  8518  gt0ap0  8557  ap0gt0  8571  lt0ap0  8579  prodgt0  8782  prodge0  8784  lt2msq1  8815  lediv12a  8824  ledivp1  8833  squeeze0  8834  mulle0r  8874  nn2ge  8925  0mnnnnn0  9181  elnn0z  9239  nn0negleid  9294  rpgecl  9653  ge0p1rp  9656  ledivge1le  9697  mul2lt0rlt0  9730  mul2lt0rgt0  9731  mul2lt0np  9734  iccf1o  9975  elfz1b  10060  elfz0fzfz0  10096  fz0fzelfz0  10097  fzo1fzo0n0  10153  elfzo0z  10154  fzofzim  10158  elfzodifsumelfzo  10171  btwnzge0  10270  modqid  10319  mulqaddmodid  10334  mulp1mod1  10335  modqltm1p1mod  10346  addmodlteq  10368  expgt1  10528  ltexp2a  10542  leexp2a  10543  expnbnd  10613  expnlbnd2  10615  nn0ltexp2  10658  expcanlem  10663  expcan  10664  resqrexlemcalc3  10993  resqrexlemnm  10995  resqrexlemgt0  10997  sqrtgt0  11011  abs00ap  11039  leabs  11051  ltabs  11064  abslt  11065  absle  11066  absgt0ap  11076  rpmaxcl  11200  rpmincl  11214  mul0inf  11217  reccn2ap  11289  climge0  11301  fsumrecl  11377  isumlessdc  11472  divcnv  11473  expcnvre  11479  absltap  11485  geolim2  11488  georeclim  11489  geoisumr  11494  cvgratnnlemnexp  11500  cvgratnnlemmn  11501  cvgratnnlemabsle  11503  mertenslem2  11512  cos12dec  11743  p1modz1  11769  dvdslelemd  11816  oddge22np1  11853  divalglemnn  11890  divalglemeuneg  11895  lcmgcdlem  12044  dvdsnprmd  12092  isprm5lem  12108  sqrt2irraplemnn  12146  sqrt2irrap  12147  qnumgt0  12165  qexpz  12317  4sqlem6  12348  znnen  12366  ennnfoneleminc  12379  exmidunben  12394  mulcncflem  13661  cosz12  13772  cos02pilt1  13843  ioocosf1o  13846  rplogcl  13871  cxplt  13907  cxple  13908  ltexp2  13931  lgsdilem  13999  refeq  14337  trilpolemeq1  14349  trilpolemlt1  14350