Theorem 0red 8180

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8031  0cc0 8032

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1re 8126  ax-addrcl 8129  ax-rnegex 8141

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

This theorem is referenced by:  gt0ne0  8607  add20  8654  subge0  8655  lesub0  8659  addgt0d  8701  sublt0d  8750  gt0add  8753  apreap  8767  gt0ap0  8806  ap0gt0  8820  lt0ap0  8828  prodgt0  9032  prodge0  9034  lt2msq1  9065  lediv12a  9074  ledivp1  9083  squeeze0  9084  mulle0r  9124  nn2ge  9176  0mnnnnn0  9434  elnn0z  9492  nn0negleid  9548  rpgecl  9917  ge0p1rp  9920  ledivge1le  9961  mul2lt0rlt0  9994  mul2lt0rgt0  9995  mul2lt0np  9998  iccf1o  10239  elfz1b  10325  elfz0fzfz0  10361  fz0fzelfz0  10362  fzo1fzo0n0  10423  elfzo0z  10424  fzofzim  10428  elfzodifsumelfzo  10447  btwnzge0  10561  modqid  10612  mulqaddmodid  10627  mulp1mod1  10628  modqltm1p1mod  10639  addmodlteq  10661  expgt1  10840  ltexp2a  10854  leexp2a  10855  expnbnd  10926  expnlbnd2  10928  zzlesq  10971  nn0ltexp2  10972  expcanlem  10978  expcan  10979  iswrdiz  11124  ccat2s1fvwd  11228  swrdswrdlem  11289  swrdswrd  11290  resqrexlemcalc3  11581  resqrexlemnm  11583  resqrexlemgt0  11585  sqrtgt0  11599  abs00ap  11627  leabs  11639  ltabs  11652  abslt  11653  absle  11654  absgt0ap  11664  rpmaxcl  11788  nn0maxcl  11790  rpmincl  11803  mul0inf  11806  reccn2ap  11878  climge0  11890  fsumrecl  11967  isumlessdc  12062  divcnv  12063  expcnvre  12069  absltap  12075  geolim2  12078  georeclim  12079  geoisumr  12084  cvgratnnlemnexp  12090  cvgratnnlemmn  12091  cvgratnnlemabsle  12093  mertenslem2  12102  cos12dec  12334  p1modz1  12360  dvdslelemd  12409  oddge22np1  12447  divalglemnn  12484  divalglemeuneg  12489  bitsfzolem  12520  bitsinv1lem  12527  lcmgcdlem  12654  dvdsnprmd  12702  isprm5lem  12718  sqrt2irraplemnn  12756  sqrt2irrap  12757  qnumgt0  12775  qexpz  12930  4sqlem6  12961  znnen  13024  ennnfoneleminc  13037  exmidunben  13052  mulcncflem  15337  hovercncf  15376  hovera  15377  hoverb  15378  hoverlt1  15379  hovergt0  15380  ivthdichlem  15381  dich0  15382  cosz12  15510  cos02pilt1  15581  ioocosf1o  15584  rplogcl  15609  cxplt  15646  cxple  15647  ltexp2  15671  mersenne  15727  lgsdilem  15762  gausslemma2dlem1a  15793  lgseisen  15809  lgsquadlem1  15812  lgsquadlem2  15813  refeq  16658  trilpolemeq1  16670  trilpolemlt1  16671  ltlenmkv  16700