Theorem gt0ne0d 11692

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 11126	. 2 ⊢ (𝜑 → 0 ∈ ℝ)
2		gt0ne0d.1	. 2 ⊢ (𝜑 → 0 < 𝐴)
3	1, 2	gtned 11259	1 ⊢ (𝜑 → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ≠ wne 2929   class class class wbr 5095  0cc0 11017   < clt 11157

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11074  ax-1cn 11075  ax-addrcl 11078  ax-rnegex 11088  ax-cnre 11090  ax-pre-lttri 11091  ax-pre-lttrn 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11159  df-mnf 11160  df-ltxr 11162

This theorem is referenced by:  recextlem2  11759  prodgt0  11979  ltdiv1  11997  ltmuldiv  12006  ltrec  12015  lerec  12016  lediv12a  12026  recp1lt1  12031  ledivp1  12035  supmul1  12102  nnne0  12170  rpnnen1lem5  12885  ltexp2a  14080  leexp2  14085  leexp2a  14086  expnbnd  14146  expmulnbnd  14149  discr1  14153  eqsqrt2d  15283  bpoly4  15973  isabvd  20736  gzrngunit  21379  fvmptnn04ifa  22785  chfacffsupp  22791  chfacfscmul0  22793  chfacfpmmul0  22797  stdbdxmet  24450  evth  24905  itg2monolem3  25700  mvth  25944  dvlip  25945  dvcvx  25972  ftc1lem4  25993  dgradd2  26221  radcnvlem1  26369  pilem2  26409  coseq00topi  26458  tangtx  26461  tanabsge  26462  cos02pilt1  26482  tanord1  26493  logcnlem4  26601  cxplt  26650  atantan  26880  jensenlem2  26945  jensen  26946  lgamgulmlem2  26987  basellem3  27040  basellem4  27041  basellem8  27045  dchrmusumlema  27451  selberg3lem1  27515  abvcxp  27573  ostth2  27595  axsegconlem8  28923  axsegconlem9  28924  axsegconlem10  28925  axpaschlem  28939  axcontlem2  28964  axcontlem4  28966  axcontlem7  28969  iswwlksnx  29839  wspn0  29923  friendshipgt3  30399  his6  31100  eigrei  31835  sgnmul  32844  sgn0bi  32849  sgnmulsgp  32852  cycpmco2lem4  33139  cycpmco2lem5  33140  finexttrb  33750  fldext2rspun  33767  cos9thpiminplylem1  33867  cos9thpiminply  33873  xrge0iifcv  34019  signsvfpn  34670  tgoldbachgtde  34745  tgoldbachgtda  34746  lfuhgr2  35235  knoppndvlem18  36645  knoppndvlem19  36646  knoppndvlem21  36648  ftc1cnnclem  37804  areacirclem1  37821  3lexlogpow2ineq1  42224  3lexlogpow2ineq2  42225  3lexlogpow5ineq5  42226  aks4d1p1p6  42239  aks6d1c4  42290  aks6d1c2  42296  aks6d1c6lem4  42339  sn-nnne0  42630  sn-recgt0d  42647  mulgt0b2d  42648  mulltgt0d  42652  mullt0b2d  42654  3cubeslem2  42842  irrapxlem2  42980  irrapxlem5  42983  pellexlem2  42987  imo72b2  44329  binomcxplemnotnn0  44513  dvdivbd  46083  dvbdfbdioolem1  46088  ioodvbdlimc1lem1  46091  ioodvbdlimc1lem2  46092  ioodvbdlimc2lem  46094  stoweidlem7  46167  stoweidlem36  46196  wallispilem3  46227  wallispilem4  46228  wallispi2lem1  46231  wallispi2lem2  46232  stirlinglem3  46236  stirlinglem6  46239  stirlinglem7  46240  stirlinglem10  46243  stirlinglem11  46244  stirlinglem12  46245  stirlinglem13  46246  stirlinglem14  46247  stirlinglem15  46248  dirkerval2  46254  dirkeritg  46262  dirkercncflem2  46264  fourierdlem6  46273  fourierdlem7  46274  fourierdlem19  46286  fourierdlem26  46293  fourierdlem30  46297  fourierdlem48  46314  fourierdlem49  46315  fourierdlem51  46317  fourierdlem63  46329  fourierdlem64  46330  fourierdlem71  46337  fourierdlem89  46355  fourierdlem90  46356  fourierdlem91  46357  fourierdlem103  46369  fourierdlem104  46370  fourierdlem112  46378  sqwvfoura  46388  fourierswlem  46390  etransclem4  46398  etransclem31  46425  etransclem32  46426  cjnpoly  47051  iccpartgt  47589  upgrimpthslem2  48070  rege1logbrege0  48720  itcovalsuc  48829  ackvalsuc1mpt  48840  eenglngeehlnmlem2  48900  itsclc0yqsol  48926  itscnhlc0xyqsol  48927  itsclc0xyqsolr  48931  itsclinecirc0in  48937  itscnhlinecirc02p  48947  inlinecirc02plem  48948