Theorem 0red 8274

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℝcr 8125  0cc0 8126

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 2214  ax-1re 8220  ax-addrcl 8223  ax-rnegex 8235

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-cleq 2225  df-clel 2228  df-ral 2525  df-rex 2526

This theorem is referenced by:  gt0ne0  8700  add20  8747  subge0  8748  lesub0  8752  addgt0d  8794  sublt0d  8843  gt0add  8846  apreap  8860  gt0ap0  8899  ap0gt0  8913  lt0ap0  8921  prodgt0  9125  prodge0  9127  lt2msq1  9158  lediv12a  9167  ledivp1  9176  squeeze0  9177  mulle0r  9217  nn2ge  9269  0mnnnnn0  9527  elnn0z  9589  nn0negleid  9645  rpgecl  10014  ge0p1rp  10017  ledivge1le  10058  mul2lt0rlt0  10091  mul2lt0rgt0  10092  mul2lt0np  10095  iccf1o  10337  elfz1b  10423  elfz0fzfz0  10459  fz0fzelfz0  10460  fzo1fzo0n0  10521  elfzo0z  10522  fzofzim  10526  elfzodifsumelfzo  10545  btwnzge0  10659  modqid  10710  mulqaddmodid  10725  mulp1mod1  10726  modqltm1p1mod  10737  addmodlteq  10759  expgt1  10938  ltexp2a  10952  leexp2a  10953  expnbnd  11024  expnlbnd2  11026  zzlesq  11069  nn0ltexp2  11070  expcanlem  11076  expcan  11077  ssenneg  11200  sshashneg  11201  iswrdiz  11227  ccat2s1fvwd  11331  swrdswrdlem  11392  swrdswrd  11393  resqrexlemcalc3  11697  resqrexlemnm  11699  resqrexlemgt0  11701  sqrtgt0  11715  abs00ap  11743  leabs  11755  ltabs  11768  abslt  11769  absle  11770  absgt0ap  11780  rpmaxcl  11904  nn0maxcl  11906  rpmincl  11919  mul0inf  11922  reccn2ap  11994  climge0  12006  fsumrecl  12083  isumlessdc  12178  divcnv  12179  expcnvre  12185  absltap  12191  geolim2  12194  georeclim  12195  geoisumr  12200  cvgratnnlemnexp  12206  cvgratnnlemmn  12207  cvgratnnlemabsle  12209  mertenslem2  12218  cos12dec  12450  p1modz1  12476  dvdslelemd  12525  oddge22np1  12563  divalglemnn  12600  divalglemeuneg  12605  bitsfzolem  12636  bitsinv1lem  12643  lcmgcdlem  12770  dvdsnprmd  12818  isprm5lem  12834  sqrt2irraplemnn  12872  sqrt2irrap  12873  qnumgt0  12891  qexpz  13046  4sqlem6  13077  znnen  13141  ennnfoneleminc  13154  exmidunben  13169  mulcncflem  15464  hovercncf  15503  hovera  15504  hoverb  15505  hoverlt1  15506  hovergt0  15507  ivthdichlem  15508  dich0  15509  cosz12  15637  cos02pilt1  15708  ioocosf1o  15711  rplogcl  15736  cxplt  15773  cxple  15774  ltexp2  15798  mersenne  15857  lgsdilem  15892  gausslemma2dlem1a  15923  lgseisen  15939  lgsquadlem1  15942  lgsquadlem2  15943  refeq  16800  trilpolemeq1  16816  trilpolemlt1  16817  ltlenmkv  16847