Theorem 0red 7957

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℝcr 7809  0cc0 7810

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1re 7904  ax-addrcl 7907  ax-rnegex 7919

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-cleq 2170  df-clel 2173  df-ral 2460  df-rex 2461

This theorem is referenced by:  gt0ne0  8383  add20  8430  subge0  8431  lesub0  8435  addgt0d  8477  sublt0d  8526  gt0add  8529  apreap  8543  gt0ap0  8582  ap0gt0  8596  lt0ap0  8604  prodgt0  8808  prodge0  8810  lt2msq1  8841  lediv12a  8850  ledivp1  8859  squeeze0  8860  mulle0r  8900  nn2ge  8951  0mnnnnn0  9207  elnn0z  9265  nn0negleid  9320  rpgecl  9681  ge0p1rp  9684  ledivge1le  9725  mul2lt0rlt0  9758  mul2lt0rgt0  9759  mul2lt0np  9762  iccf1o  10003  elfz1b  10089  elfz0fzfz0  10125  fz0fzelfz0  10126  fzo1fzo0n0  10182  elfzo0z  10183  fzofzim  10187  elfzodifsumelfzo  10200  btwnzge0  10299  modqid  10348  mulqaddmodid  10363  mulp1mod1  10364  modqltm1p1mod  10375  addmodlteq  10397  expgt1  10557  ltexp2a  10571  leexp2a  10572  expnbnd  10643  expnlbnd2  10645  nn0ltexp2  10688  expcanlem  10694  expcan  10695  resqrexlemcalc3  11024  resqrexlemnm  11026  resqrexlemgt0  11028  sqrtgt0  11042  abs00ap  11070  leabs  11082  ltabs  11095  abslt  11096  absle  11097  absgt0ap  11107  rpmaxcl  11231  rpmincl  11245  mul0inf  11248  reccn2ap  11320  climge0  11332  fsumrecl  11408  isumlessdc  11503  divcnv  11504  expcnvre  11510  absltap  11516  geolim2  11519  georeclim  11520  geoisumr  11525  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  cvgratnnlemabsle  11534  mertenslem2  11543  cos12dec  11774  p1modz1  11800  dvdslelemd  11848  oddge22np1  11885  divalglemnn  11922  divalglemeuneg  11927  lcmgcdlem  12076  dvdsnprmd  12124  isprm5lem  12140  sqrt2irraplemnn  12178  sqrt2irrap  12179  qnumgt0  12197  qexpz  12349  4sqlem6  12380  znnen  12398  ennnfoneleminc  12411  exmidunben  12426  mulcncflem  14060  cosz12  14171  cos02pilt1  14242  ioocosf1o  14245  rplogcl  14270  cxplt  14306  cxple  14307  ltexp2  14330  lgsdilem  14398  refeq  14746  trilpolemeq1  14758  trilpolemlt1  14759  ltlenmkv  14787