Theorem 0red 7921

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℝcr 7773  0cc0 7774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-1re 7868  ax-addrcl 7871  ax-rnegex 7883

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-cleq 2163  df-clel 2166  df-ral 2453  df-rex 2454

This theorem is referenced by:  gt0ne0  8346  add20  8393  subge0  8394  lesub0  8398  addgt0d  8440  sublt0d  8489  gt0add  8492  apreap  8506  gt0ap0  8545  ap0gt0  8559  lt0ap0  8567  prodgt0  8768  prodge0  8770  lt2msq1  8801  lediv12a  8810  ledivp1  8819  squeeze0  8820  mulle0r  8860  nn2ge  8911  0mnnnnn0  9167  elnn0z  9225  nn0negleid  9280  rpgecl  9639  ge0p1rp  9642  ledivge1le  9683  mul2lt0rlt0  9716  mul2lt0rgt0  9717  mul2lt0np  9720  iccf1o  9961  elfz1b  10046  elfz0fzfz0  10082  fz0fzelfz0  10083  fzo1fzo0n0  10139  elfzo0z  10140  fzofzim  10144  elfzodifsumelfzo  10157  btwnzge0  10256  modqid  10305  mulqaddmodid  10320  mulp1mod1  10321  modqltm1p1mod  10332  addmodlteq  10354  expgt1  10514  ltexp2a  10528  leexp2a  10529  expnbnd  10599  expnlbnd2  10601  nn0ltexp2  10644  expcanlem  10649  expcan  10650  resqrexlemcalc3  10980  resqrexlemnm  10982  resqrexlemgt0  10984  sqrtgt0  10998  abs00ap  11026  leabs  11038  ltabs  11051  abslt  11052  absle  11053  absgt0ap  11063  rpmaxcl  11187  rpmincl  11201  mul0inf  11204  reccn2ap  11276  climge0  11288  fsumrecl  11364  isumlessdc  11459  divcnv  11460  expcnvre  11466  absltap  11472  geolim2  11475  georeclim  11476  geoisumr  11481  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  cvgratnnlemabsle  11490  mertenslem2  11499  cos12dec  11730  p1modz1  11756  dvdslelemd  11803  oddge22np1  11840  divalglemnn  11877  divalglemeuneg  11882  lcmgcdlem  12031  dvdsnprmd  12079  isprm5lem  12095  sqrt2irraplemnn  12133  sqrt2irrap  12134  qnumgt0  12152  qexpz  12304  4sqlem6  12335  znnen  12353  ennnfoneleminc  12366  exmidunben  12381  mulcncflem  13384  cosz12  13495  cos02pilt1  13566  ioocosf1o  13569  rplogcl  13594  cxplt  13630  cxple  13631  ltexp2  13654  lgsdilem  13722  refeq  14060  trilpolemeq1  14072  trilpolemlt1  14073