Theorem gt0ne0d 11873

Description: Positive implies nonzero. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
gt0ne0d.1	⊢ (𝜑 → 0 < 𝐴)

Assertion

Ref	Expression
gt0ne0d	⊢ (𝜑 → 𝐴 ≠ 0)

Proof of Theorem gt0ne0d

Step	Hyp	Ref	Expression
1		0red 11304	. 2 ⊢ (𝜑 → 0 ∈ ℝ)
2		gt0ne0d.1	. 2 ⊢ (𝜑 → 0 < 𝐴)
3	1, 2	gtned 11438	1 ⊢ (𝜑 → 𝐴 ≠ 0)

This proof depends on syntax axioms:   → wi 4   ≠ wne 2956   class class class wbr 5103  0cc0 11193   < clt 11336

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-1cn 11251  ax-addrcl 11254  ax-rnegex 11264  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-ltxr 11341

This theorem is used by:  recextlem2  11940  prodgt0  12157  ltdiv1  12174  ltmuldiv  12183  ltrec  12192  lerec  12193  lediv12a  12203  recp1lt1  12208  ledivp1  12212  supmul1  12279  nnne0  12365  rpnnen1lem5  13102  ltexp2a  14302  leexp2  14307  leexp2a  14308  expnbnd  14369  expmulnbnd  14372  discr1  14376  sgn0bi  15249  sgnmul  15253  eqsqrt2d  15529  bpoly4  16218  isabvd  21062  gzrngunit  21732  fvmptnn04ifa  23161  chfacffsupp  23167  chfacfscmul0  23169  chfacfpmmul0  23173  stdbdxmet  24827  evth  25273  itg2monolem3  26066  mvth  26305  dvlip  26306  dvcvx  26333  ftc1lem4  26352  dgradd2  26580  radcnvlem1  26733  pilem2  26772  coseq00topi  26824  tangtx  26827  tanabsge  26828  cos02pilt1  26847  tanord1  26858  logcnlem4  26966  cxplt  27015  atantan  27244  jensenlem2  27308  jensen  27309  lgamgulmlem2  27350  basellem3  27403  basellem4  27404  basellem8  27408  dchrmusumlema  27813  selberg3lem1  27877  abvcxp  27935  ostth2  27957  axsegconlem8  29495  axsegconlem9  29496  axsegconlem10  29497  axpaschlem  29511  axcontlem2  29536  axcontlem4  29538  axcontlem7  29541  lfuhgr2  29720  iswwlksnx  30422  wspn0  30506  friendshipgt3  30992  his6  31694  eigrei  32429  sgnmulsgp  33416  cycpmco2lem4  33683  cycpmco2lem5  33684  finexttrb  34290  fldext2rspun  34307  cos9thpiminplylem1  34407  cos9thpiminply  34413  xrge0iifcv  34559  signsvfpn  35207  tgoldbachgtde  35282  tgoldbachgtda  35283  knoppndvlem18  37375  knoppndvlem19  37376  knoppndvlem21  37378  ftc1cnnclem  38589  areacirclem1  38606  3lexlogpow2ineq1  43088  3lexlogpow2ineq2  43089  3lexlogpow5ineq5  43090  aks4d1p1p6  43103  aks6d1c4  43154  aks6d1c2  43160  aks6d1c6lem4  43203  sn-nnne0  43504  sn-recgt0d  43521  mulgt0b2d  43522  mulltgt0d  43526  mullt0b2d  43528  3cubeslem2  43675  irrapxlem2  43809  irrapxlem5  43812  pellexlem2  43816  imo72b2  45157  binomcxplemnotnn0  45325  dvdivbd  46902  dvbdfbdioolem1  46907  ioodvbdlimc1lem1  46910  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  stoweidlem7  46986  stoweidlem36  47015  wallispilem3  47046  wallispilem4  47047  wallispi2lem1  47050  wallispi2lem2  47051  stirlinglem3  47055  stirlinglem6  47058  stirlinglem7  47059  stirlinglem10  47062  stirlinglem11  47063  stirlinglem12  47064  stirlinglem13  47065  stirlinglem14  47066  stirlinglem15  47067  dirkerval2  47073  dirkeritg  47081  dirkercncflem2  47083  fourierdlem6  47092  fourierdlem7  47093  fourierdlem19  47105  fourierdlem26  47112  fourierdlem30  47116  fourierdlem48  47133  fourierdlem49  47134  fourierdlem51  47136  fourierdlem63  47148  fourierdlem64  47149  fourierdlem71  47156  fourierdlem89  47174  fourierdlem90  47175  fourierdlem91  47176  fourierdlem103  47188  fourierdlem104  47189  fourierdlem112  47197  sqwvfoura  47207  fourierswlem  47209  etransclem4  47217  etransclem31  47244  etransclem32  47245  cjnpoly  47908  iccpartgt  48478  upgrimpthslem2  48975  rege1logbrege0  49639  itcovalsuc  49748  ackvalsuc1mpt  49759  eenglngeehlnmlem2  49819  itsclc0yqsol  49845  itscnhlc0xyqsol  49846  itsclc0xyqsolr  49850  itsclinecirc0in  49856  itscnhlinecirc02p  49866  inlinecirc02plem  49867