Theorem 2ne0 12378

Description: The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)

Assertion

Ref	Expression
2ne0	⊢ 2 ≠ 0

Proof of Theorem 2ne0

Step	Hyp	Ref	Expression
1		2re 12348	. 2 ⊢ 2 ∈ ℝ
2		2pos 12377	. 2 ⊢ 0 < 2
3	1, 2	gt0ne0ii 11807	1 ⊢ 2 ≠ 0

Syntax hints:   ≠ wne 2933  0cc0 11165  2c2 12329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pow 5373  ax-pr 5437  ax-un 7751  ax-resscn 11222  ax-1cn 11223  ax-icn 11224  ax-addcl 11225  ax-addrcl 11226  ax-mulcl 11227  ax-mulrcl 11228  ax-mulcom 11229  ax-addass 11230  ax-mulass 11231  ax-distr 11232  ax-i2m1 11233  ax-1ne0 11234  ax-1rid 11235  ax-rnegex 11236  ax-rrecex 11237  ax-cnre 11238  ax-pre-lttri 11239  ax-pre-lttrn 11240  ax-pre-ltadd 11241  ax-pre-mulgt0 11242

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3789  df-csb 3905  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-nul 4336  df-if 4537  df-pw 4612  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-br 5157  df-opab 5219  df-mpt 5240  df-id 5584  df-po 5598  df-so 5599  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-res 5698  df-ima 5699  df-iota 6510  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-riota 7386  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8742  df-en 8983  df-dom 8984  df-sdom 8985  df-pnf 11307  df-mnf 11308  df-xr 11309  df-ltxr 11310  df-le 11311  df-sub 11503  df-neg 11504  df-2 12337

This theorem is referenced by:  2div2e1  12415  4d2e2  12444  0ne2  12481  2cnne0  12484  2rene0  12485  halfre  12488  halfcn  12489  halfpm6th  12495  2muline0  12498  halfcl  12499  rehalfcl  12500  half0  12501  2halves  12502  halfaddsub  12507  subhalfhalf  12508  xp1d2m1eqxm1d2  12528  div4p1lem1div2  12529  zneo  12707  nneo  12708  zeo  12710  zeo2  12711  halfthird  12882  fvf1tp  13820  2tnp1ge0ge0  13860  zesq  14255  discr  14269  prprrab  14504  tpf1ofv2  14528  crre  15140  addcj  15174  absmax  15355  rddif  15366  abs3lemi  15436  iseralt  15710  arisum  15885  arisum2  15886  geo2sum  15898  geo2lim  15900  geoihalfsum  15907  bpoly2  16080  bpoly3  16081  bpoly4  16082  ege2le3  16113  efgt0  16126  tanval2  16156  tanval3  16157  efi4p  16160  efival  16175  sinhval  16177  tanhlt1  16183  cosadd  16188  sinmul  16195  cos01bnd  16209  sin02gt0  16215  sqrt2irrlem  16271  sqrt2irr  16272  mod2eq1n2dvds  16370  evend2  16380  oddp1d2  16381  ltoddhalfle  16384  nn0enne  16400  nn0o  16406  flodddiv4  16436  flodddiv4t2lthalf  16439  bitsp1e  16453  bitsp1o  16454  bitsfzo  16456  bitsmod  16457  bitsinv1lem  16462  bitsuz  16495  3lcm2e6woprm  16637  6lcm4e12  16638  pythagtriplem12  16849  pythagtriplem14  16851  pythagtriplem15  16852  pythagtriplem16  16853  pythagtriplem17  16854  iserodd  16858  prmreclem5  16943  prmreclem6  16944  4sqlem7  16967  4sqlem10  16970  4sqlem19  16986  smndex2dlinvh  18928  ablsimpgfindlem2  20130  zringndrg  21480  metnrmlem3  24891  htpycc  25020  pcoval2  25057  pcocn  25058  pcohtpylem  25060  pcopt  25063  pcopt2  25064  pcoass  25065  pcorevlem  25067  minveclem2  25468  ovolunlem1a  25539  ovolunlem1  25540  uniioombl  25632  dyaddisjlem  25638  mbfi1fseqlem6  25764  dvmptre  26015  dvsincos  26027  lhop1  26061  coscn  26498  sinhalfpilem  26514  cospi  26523  sincosq3sgn  26551  sincosq4sgn  26552  tangtx  26556  sinq12gt0  26558  sincosq1eq  26563  sincos4thpi  26564  tan4thpi  26565  sincos6thpi  26566  sincos3rdpi  26567  pige3ALT  26570  abssinper  26571  sineq0  26574  coseq1  26575  efeq1  26578  eflogeq  26652  cosargd  26658  tanarg  26669  cxpsqrtlem  26752  cxpsqrt  26753  logsqrt  26754  dvcnsqrt  26794  root1eq1  26806  2logb9irrALT  26849  sqrt2cxp2logb9e3  26850  ang180lem2  26861  ang180lem3  26862  ssscongptld  26873  chordthmlem  26883  chordthmlem2  26884  chordthmlem4  26886  heron  26889  quad2  26890  1cubrlem  26892  dcubic2  26895  dcubic1  26896  dcubic  26897  mcubic  26898  cubic2  26899  cubic  26900  dquartlem1  26902  dquartlem2  26903  dquart  26904  quart1lem  26906  quart1  26907  quartlem4  26911  quart  26912  asinsin  26943  cosasin  26955  atancj  26961  efiatan  26963  efiatan2  26968  2efiatan  26969  tanatan  26970  cosatan  26972  atantan  26974  atanbndlem  26976  dvatan  26986  atantayl  26988  atantayl2  26989  atantayl3  26990  leibpilem2  26992  log2cnv  26995  log2tlbnd  26996  birthday  27005  cxp2limlem  27027  lgamgulmlem2  27081  lgamgulmlem3  27082  lgamucov  27089  ftalem2  27125  basellem3  27134  chtub  27264  mersenne  27279  bcmax  27330  bclbnd  27332  bposlem6  27341  bposlem8  27343  bposlem9  27344  lgslem1  27349  lgsqrlem2  27399  gausslemma2dlem1a  27417  gausslemma2dlem3  27420  lgseisenlem1  27427  lgseisenlem2  27428  lgseisenlem3  27429  lgsquadlem1  27432  lgsquadlem2  27433  lgsquad2lem1  27436  lgsquad2lem2  27437  lgsquad3  27439  m1lgs  27440  2lgslem1a1  27441  2lgslem1a2  27442  2lgslem1b  27444  2lgslem1c  27445  2lgslem3a  27448  2lgslem3b  27449  2lgslem3c  27450  2lgslem3d  27451  chebbnd1lem2  27522  chebbnd1lem3  27523  chebbnd1  27524  dchrisum0fno1  27563  logdivsum  27585  mulog2sumlem3  27588  vmalogdivsum2  27590  selberg4lem1  27612  selberg3r  27621  selberg4r  27622  selberg34r  27623  pntpbnd1a  27637  pntibndlem2  27643  pntlemg  27650  axlowdimlem13  28911  usgrexmpldifpr  29217  usgrexmplef  29218  upgrwlkdvdelem  29696  rusgrnumwwlkl1  29925  upgr4cycl4dv4e  30141  konigsberglem1  30208  ex-hash  30409  ipdirilem  30785  minvecolem2  30831  norm3lem  31105  normpar2i  31112  mayete3i  31684  nmcexi  31982  opsqrlem6  32101  quad3d  32683  threehalves  32805  constrelextdg2  33664  2sqr3minply  33665  sqsscirc1  33781  dya2icoseg  34169  dya2iocucvr  34176  omssubadd  34192  oddpwdc  34246  coinfliplem  34370  itgexpif  34510  hgt750lemd  34552  logdivsqrle  34554  umgracycusgr  35049  problem5  35564  quad3  35565  circum  35569  knoppndvlem1  36283  knoppndvlem2  36284  knoppndvlem7  36289  knoppndvlem8  36290  knoppndvlem9  36291  knoppndvlem10  36292  knoppndvlem14  36296  knoppndvlem15  36297  knoppndvlem16  36298  knoppndvlem17  36299  cnndvlem1  36308  irrdifflemf  37099  sin2h  37378  cos2h  37379  tan2h  37380  poimirlem29  37417  mblfinlem1  37425  mblfinlem2  37426  itg2addnclem  37439  areacirclem1  37476  areacirc  37481  isbnd2  37551  dvrelog2b  41832  oddnumth  42092  sumcubes  42094  ef11d  42120  cxpi11d  42124  dffltz  42378  flt4lem5e  42400  sum9cubes  42418  jm2.22  42744  jm2.23  42745  proot1ex  42952  areaquad  42972  sqrtcval  43399  resqrtvalex  43403  isosctrlem1ALT  44701  sineq0ALT  44704  suplesup  45044  sumnnodd  45341  0ellimcdiv  45360  coseq0  45575  sinmulcos  45576  sinaover2ne0  45579  ioodvbdlimc1lem2  45643  ioodvbdlimc2lem  45645  stoweidlem62  45773  wallispilem4  45779  wallispilem5  45780  wallispi  45781  wallispi2  45784  stirlinglem1  45785  stirlinglem7  45791  dirker2re  45803  dirkerdenne0  45804  dirkerre  45806  dirkerper  45807  dirkertrigeqlem2  45810  dirkertrigeqlem3  45811  dirkertrigeq  45812  dirkeritg  45813  dirkercncflem1  45814  dirkercncflem2  45815  fourierdlem43  45861  fourierdlem44  45862  fourierdlem56  45873  fourierdlem57  45874  fourierdlem58  45875  fourierdlem62  45879  fourierdlem66  45883  fourierdlem68  45885  fourierdlem72  45889  fourierdlem76  45893  fourierdlem78  45895  fourierdlem79  45896  fourierdlem80  45897  fourierdlem83  45900  fourierdlem95  45912  fourierdlem103  45920  fourierdlem104  45921  fouriercnp  45937  fourierswlem  45941  sge0ad2en  46142  ovnsubaddlem1  46281  fmtnorec1  47199  fmtnoprmfac2lem1  47228  sfprmdvdsmersenne  47265  proththd  47276  41prothprmlem1  47279  quad1  47282  requad01  47283  requad1  47284  dfodd6  47299  dfeven4  47300  enege  47307  onego  47308  oddflALTV  47325  0evenALTV  47350  nn0onn0exALTV  47361  nn0enn0exALTV  47362  nnennexALTV  47363  6even  47373  8even  47375  0nodd  47648  2nodd  47650  2zrngnmlid  47733  zlmodzxzldeplem4  47987  pw2m1lepw2m1  48004  nn0onn0ex  48012  nn0enn0ex  48013  nnennex  48014  nnpw2even  48018  fldivexpfllog2  48054  nnlog2ge0lt1  48055  nnpw2blen  48069  blen1  48073  blen2  48074  blennnt2  48078  nnolog2flm1  48079  blennn0em1  48080  dig2nn1st  48094  dig2nn0  48100  0dig2nn0o  48102  dig2bits  48103  dignn0flhalflem1  48104  dignn0flhalflem2  48105  dignn0ehalf  48106  nn0sumshdiglemA  48108  nn0sumshdiglemB  48109  itcoval2  48153  itsclc0yqsol  48253  sinhpcosh  48587