Theorem gt0ne0d 11684

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

Syntax hints:   → wi 4   ≠ wne 2925   class class class wbr 5092  0cc0 11009   < clt 11149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-addrcl 11070  ax-rnegex 11080  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-ltxr 11154

This theorem is referenced by:  recextlem2  11751  prodgt0  11971  ltdiv1  11989  ltmuldiv  11998  ltrec  12007  lerec  12008  lediv12a  12018  recp1lt1  12023  ledivp1  12027  supmul1  12094  nnne0  12162  rpnnen1lem5  12882  ltexp2a  14073  leexp2  14078  leexp2a  14079  expnbnd  14139  expmulnbnd  14142  discr1  14146  eqsqrt2d  15276  bpoly4  15966  isabvd  20697  gzrngunit  21340  fvmptnn04ifa  22735  chfacffsupp  22741  chfacfscmul0  22743  chfacfpmmul0  22747  stdbdxmet  24401  evth  24856  itg2monolem3  25651  mvth  25895  dvlip  25896  dvcvx  25923  ftc1lem4  25944  dgradd2  26172  radcnvlem1  26320  pilem2  26360  coseq00topi  26409  tangtx  26412  tanabsge  26413  cos02pilt1  26433  tanord1  26444  logcnlem4  26552  cxplt  26601  atantan  26831  jensenlem2  26896  jensen  26897  lgamgulmlem2  26938  basellem3  26991  basellem4  26992  basellem8  26996  dchrmusumlema  27402  selberg3lem1  27466  abvcxp  27524  ostth2  27546  axsegconlem8  28869  axsegconlem9  28870  axsegconlem10  28871  axpaschlem  28885  axcontlem2  28910  axcontlem4  28912  axcontlem7  28915  iswwlksnx  29785  wspn0  29869  friendshipgt3  30342  his6  31043  eigrei  31778  sgnmul  32780  sgn0bi  32785  sgnmulsgp  32788  cycpmco2lem4  33071  cycpmco2lem5  33072  finexttrb  33632  fldext2rspun  33649  cos9thpiminplylem1  33749  cos9thpiminply  33755  xrge0iifcv  33901  signsvfpn  34553  tgoldbachgtde  34628  tgoldbachgtda  34629  lfuhgr2  35092  knoppndvlem18  36503  knoppndvlem19  36504  knoppndvlem21  36506  ftc1cnnclem  37671  areacirclem1  37688  3lexlogpow2ineq1  42031  3lexlogpow2ineq2  42032  3lexlogpow5ineq5  42033  aks4d1p1p6  42046  aks6d1c4  42097  aks6d1c2  42103  aks6d1c6lem4  42146  sn-nnne0  42433  sn-recgt0d  42450  mulgt0b2d  42451  mulltgt0d  42455  mullt0b2d  42457  3cubeslem2  42658  irrapxlem2  42796  irrapxlem5  42799  pellexlem2  42803  imo72b2  44145  binomcxplemnotnn0  44329  dvdivbd  45904  dvbdfbdioolem1  45909  ioodvbdlimc1lem1  45912  ioodvbdlimc1lem2  45913  ioodvbdlimc2lem  45915  stoweidlem7  45988  stoweidlem36  46017  wallispilem3  46048  wallispilem4  46049  wallispi2lem1  46052  wallispi2lem2  46053  stirlinglem3  46057  stirlinglem6  46060  stirlinglem7  46061  stirlinglem10  46064  stirlinglem11  46065  stirlinglem12  46066  stirlinglem13  46067  stirlinglem14  46068  stirlinglem15  46069  dirkerval2  46075  dirkeritg  46083  dirkercncflem2  46085  fourierdlem6  46094  fourierdlem7  46095  fourierdlem19  46107  fourierdlem26  46114  fourierdlem30  46118  fourierdlem48  46135  fourierdlem49  46136  fourierdlem51  46138  fourierdlem63  46150  fourierdlem64  46151  fourierdlem71  46158  fourierdlem89  46176  fourierdlem90  46177  fourierdlem91  46178  fourierdlem103  46190  fourierdlem104  46191  fourierdlem112  46199  sqwvfoura  46209  fourierswlem  46211  etransclem4  46219  etransclem31  46246  etransclem32  46247  cjnpoly  46873  iccpartgt  47411  upgrimpthslem2  47892  rege1logbrege0  48543  itcovalsuc  48652  ackvalsuc1mpt  48663  eenglngeehlnmlem2  48723  itsclc0yqsol  48749  itscnhlc0xyqsol  48750  itsclc0xyqsolr  48754  itsclinecirc0in  48760  itscnhlinecirc02p  48770  inlinecirc02plem  48771