MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  4ne0 Structured version   Visualization version   GIF version

Theorem 4ne0 11731
Description: The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
Assertion
Ref Expression
4ne0 4 ≠ 0

Proof of Theorem 4ne0
StepHypRef Expression
1 4re 11707 . 2 4 ∈ ℝ
2 4pos 11730 . 2 0 < 4
31, 2gt0ne0ii 11161 1 4 ≠ 0
Colors of variables: wff setvar class
Syntax hints:  wne 3013  0cc0 10522  4c4 11680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7444  ax-resscn 10579  ax-1cn 10580  ax-icn 10581  ax-addcl 10582  ax-addrcl 10583  ax-mulcl 10584  ax-mulrcl 10585  ax-mulcom 10586  ax-addass 10587  ax-mulass 10588  ax-distr 10589  ax-i2m1 10590  ax-1ne0 10591  ax-1rid 10592  ax-rnegex 10593  ax-rrecex 10594  ax-cnre 10595  ax-pre-lttri 10596  ax-pre-lttrn 10597  ax-pre-ltadd 10598  ax-pre-mulgt0 10599
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-nel 3118  df-ral 3137  df-rex 3138  df-reu 3139  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-br 5048  df-opab 5110  df-mpt 5128  df-id 5441  df-po 5455  df-so 5456  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7096  df-ov 7141  df-oprab 7142  df-mpo 7143  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10662  df-mnf 10663  df-xr 10664  df-ltxr 10665  df-le 10666  df-sub 10857  df-neg 10858  df-2 11686  df-3 11687  df-4 11688
This theorem is referenced by:  8th4div3  11843  div4p1lem1div2  11878  fldiv4p1lem1div2  13198  fldiv4lem1div2uz2  13199  fldiv4lem1div2  13200  discr  13595  sqoddm1div8  13598  4bc2eq6  13683  bpoly3  15401  bpoly4  15402  flodddiv4  15751  flodddiv4lt  15753  flodddiv4t2lthalf  15754  6lcm4e12  15947  cphipval2  23834  4cphipval2  23835  minveclem3  24022  uniioombl  24182  sincos4thpi  25095  sincos6thpi  25097  heron  25413  quad2  25414  dcubic  25421  mcubic  25422  cubic  25424  dquartlem1  25426  dquartlem2  25427  dquart  25428  quart1cl  25429  quart1lem  25430  quart1  25431  quartlem4  25435  quart  25436  log2tlbnd  25520  bclbnd  25853  bposlem7  25863  bposlem8  25864  bposlem9  25865  gausslemma2dlem0d  25932  gausslemma2dlem3  25941  gausslemma2dlem4  25942  gausslemma2dlem5  25944  m1lgs  25961  2lgslem1a2  25963  2lgslem1  25967  2lgslem2  25968  2lgslem3a  25969  2lgslem3b  25970  2lgslem3c  25971  2lgslem3d  25972  pntibndlem2  26164  4ipval2  28480  ipidsq  28482  dipcl  28484  dipcj  28486  dip0r  28489  dipcn  28492  ip1ilem  28598  ipasslem10  28611  polid2i  28929  lnopeq0i  29779  lnophmlem2  29789  quad3  32931  limclner  42135  stoweid  42547  wallispi2lem1  42555  stirlinglem3  42560  stirlinglem12  42569  stirlinglem13  42570  fouriersw  42715
  Copyright terms: Public domain W3C validator