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

Theorem 3ne0 11320
Description: The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Assertion
Ref Expression
3ne0 3 ≠ 0

Proof of Theorem 3ne0
StepHypRef Expression
1 3re 11299 . 2 3 ∈ ℝ
2 3pos 11319 . 2 0 < 3
31, 2gt0ne0ii 10769 1 3 ≠ 0
Colors of variables: wff setvar class
Syntax hints:  wne 2943  0cc0 10141  3c3 11276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7099  ax-resscn 10198  ax-1cn 10199  ax-icn 10200  ax-addcl 10201  ax-addrcl 10202  ax-mulcl 10203  ax-mulrcl 10204  ax-mulcom 10205  ax-addass 10206  ax-mulass 10207  ax-distr 10208  ax-i2m1 10209  ax-1ne0 10210  ax-1rid 10211  ax-rnegex 10212  ax-rrecex 10213  ax-cnre 10214  ax-pre-lttri 10215  ax-pre-lttrn 10216  ax-pre-ltadd 10217  ax-pre-mulgt0 10218
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-po 5171  df-so 5172  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-riota 6756  df-ov 6798  df-oprab 6799  df-mpt2 6800  df-er 7899  df-en 8113  df-dom 8114  df-sdom 8115  df-pnf 10281  df-mnf 10282  df-xr 10283  df-ltxr 10284  df-le 10285  df-sub 10473  df-neg 10474  df-2 11284  df-3 11285
This theorem is referenced by:  8th4div3  11458  halfpm6th  11459  halfthird  11890  f1oun2prg  13870  sqrlem7  14196  caurcvgr  14611  bpoly2  14993  bpoly3  14994  bpoly4  14995  sin01bnd  15120  cos01bnd  15121  cos1bnd  15122  cos2bnd  15123  sin01gt0  15125  cos01gt0  15126  rpnnen2lem3  15150  rpnnen2lem11  15158  tangtx  24477  sincos6thpi  24487  sincos3rdpi  24488  pige3  24489  1cubr  24789  dcubic1lem  24790  dcubic2  24791  dcubic1  24792  dcubic  24793  mcubic  24794  cubic2  24795  cubic  24796  quartlem3  24806  log2cnv  24891  log2tlbnd  24892  ppiub  25149  bclbnd  25225  bposlem6  25234  bposlem9  25237  usgrexmplef  26373  upgr4cycl4dv4e  27364  konigsbergiedgw  27427  konigsberglem1  27431  konigsberglem3  27433  konigsberglem5  27435  ex-lcm  27656  hgt750lem  31068  sinccvglem  31903  pigt3  33734  mblfinlem3  33780  itg2addnclem2  33793  itg2addnclem3  33794  lhe4.4ex1a  39054  stoweidlem11  40742  stoweidlem13  40744  stoweidlem26  40757  stoweidlem34  40765  stoweidlem42  40773  stoweidlem59  40790  stoweidlem62  40793  stoweid  40794  wallispilem4  40799  wallispi2lem1  40802  stirlinglem11  40815  fourierdlem87  40924
  Copyright terms: Public domain W3C validator