Theorem 4ne0 12161

Description: The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)

Assertion

Ref	Expression
4ne0	⊢ 4 ≠ 0

Proof of Theorem 4ne0

Step	Hyp	Ref	Expression
1		4re 12137	. 2 ⊢ 4 ∈ ℝ
2		4pos 12160	. 2 ⊢ 0 < 4
3	1, 2	gt0ne0ii 11591	1 ⊢ 4 ≠ 0

Syntax hints:   ≠ wne 2941  0cc0 10951  4c4 12110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630  ax-resscn 11008  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-mulcom 11015  ax-addass 11016  ax-mulass 11017  ax-distr 11018  ax-i2m1 11019  ax-1ne0 11020  ax-1rid 11021  ax-rnegex 11022  ax-rrecex 11023  ax-cnre 11024  ax-pre-lttri 11025  ax-pre-lttrn 11026  ax-pre-ltadd 11027  ax-pre-mulgt0 11028

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-opab 5150  df-mpt 5171  df-id 5507  df-po 5521  df-so 5522  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-riota 7274  df-ov 7320  df-oprab 7321  df-mpo 7322  df-er 8548  df-en 8784  df-dom 8785  df-sdom 8786  df-pnf 11091  df-mnf 11092  df-xr 11093  df-ltxr 11094  df-le 11095  df-sub 11287  df-neg 11288  df-2 12116  df-3 12117  df-4 12118

This theorem is referenced by:  8th4div3  12273  div4p1lem1div2  12308  fldiv4p1lem1div2  13635  fldiv4lem1div2uz2  13636  fldiv4lem1div2  13637  discr  14035  sqoddm1div8  14038  4bc2eq6  14123  bpoly3  15847  bpoly4  15848  flodddiv4  16201  flodddiv4lt  16203  flodddiv4t2lthalf  16204  6lcm4e12  16398  cphipval2  24488  4cphipval2  24489  minveclem3  24676  uniioombl  24836  sincos4thpi  25753  sincos6thpi  25755  heron  26071  quad2  26072  dcubic  26079  mcubic  26080  cubic  26082  dquartlem1  26084  dquartlem2  26085  dquart  26086  quart1cl  26087  quart1lem  26088  quart1  26089  quartlem4  26093  quart  26094  log2tlbnd  26178  bclbnd  26511  bposlem7  26521  bposlem8  26522  bposlem9  26523  gausslemma2dlem0d  26590  gausslemma2dlem3  26599  gausslemma2dlem4  26600  gausslemma2dlem5  26602  m1lgs  26619  2lgslem1a2  26621  2lgslem1  26625  2lgslem2  26626  2lgslem3a  26627  2lgslem3b  26628  2lgslem3c  26629  2lgslem3d  26630  pntibndlem2  26822  4ipval2  29206  ipidsq  29208  dipcl  29210  dipcj  29212  dip0r  29215  dipcn  29218  ip1ilem  29324  ipasslem10  29337  polid2i  29655  lnopeq0i  30505  lnophmlem2  30515  quad3  33767  flt4lem5e  40709  limclner  43442  stoweid  43854  wallispi2lem1  43862  stirlinglem3  43867  stirlinglem12  43876  stirlinglem13  43877  fouriersw  44022