Theorem gt0ne0d 11742

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

Syntax hints:   → wi 4   ≠ wne 2925   class class class wbr 5107  0cc0 11068   < clt 11208

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-addrcl 11129  ax-rnegex 11139  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143

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 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-ltxr 11213

This theorem is referenced by:  recextlem2  11809  prodgt0  12029  ltdiv1  12047  ltmuldiv  12056  ltrec  12065  lerec  12066  lediv12a  12076  recp1lt1  12081  ledivp1  12085  supmul1  12152  nnne0  12220  rpnnen1lem5  12940  ltexp2a  14131  leexp2  14136  leexp2a  14137  expnbnd  14197  expmulnbnd  14200  discr1  14204  eqsqrt2d  15335  bpoly4  16025  isabvd  20721  gzrngunit  21350  fvmptnn04ifa  22737  chfacffsupp  22743  chfacfscmul0  22745  chfacfpmmul0  22749  stdbdxmet  24403  evth  24858  itg2monolem3  25653  mvth  25897  dvlip  25898  dvcvx  25925  ftc1lem4  25946  dgradd2  26174  radcnvlem1  26322  pilem2  26362  coseq00topi  26411  tangtx  26414  tanabsge  26415  cos02pilt1  26435  tanord1  26446  logcnlem4  26554  cxplt  26603  atantan  26833  jensenlem2  26898  jensen  26899  lgamgulmlem2  26940  basellem3  26993  basellem4  26994  basellem8  26998  dchrmusumlema  27404  selberg3lem1  27468  abvcxp  27526  ostth2  27548  axsegconlem8  28851  axsegconlem9  28852  axsegconlem10  28853  axpaschlem  28867  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  iswwlksnx  29770  wspn0  29854  friendshipgt3  30327  his6  31028  eigrei  31763  sgnmul  32760  sgn0bi  32765  sgnmulsgp  32768  cycpmco2lem4  33086  cycpmco2lem5  33087  finexttrb  33660  fldext2rspun  33677  cos9thpiminplylem1  33772  cos9thpiminply  33778  xrge0iifcv  33924  signsvfpn  34576  tgoldbachgtde  34651  tgoldbachgtda  34652  lfuhgr2  35106  knoppndvlem18  36517  knoppndvlem19  36518  knoppndvlem21  36520  ftc1cnnclem  37685  areacirclem1  37702  3lexlogpow2ineq1  42046  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1p1p6  42061  aks6d1c4  42112  aks6d1c2  42118  aks6d1c6lem4  42161  sn-nnne0  42448  sn-recgt0d  42465  mulgt0b2d  42466  mulltgt0d  42470  mullt0b2d  42472  3cubeslem2  42673  irrapxlem2  42811  irrapxlem5  42814  pellexlem2  42818  imo72b2  44161  binomcxplemnotnn0  44345  dvdivbd  45921  dvbdfbdioolem1  45926  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  stoweidlem7  46005  stoweidlem36  46034  wallispilem3  46065  wallispilem4  46066  wallispi2lem1  46069  wallispi2lem2  46070  stirlinglem3  46074  stirlinglem6  46077  stirlinglem7  46078  stirlinglem10  46081  stirlinglem11  46082  stirlinglem12  46083  stirlinglem13  46084  stirlinglem14  46085  stirlinglem15  46086  dirkerval2  46092  dirkeritg  46100  dirkercncflem2  46102  fourierdlem6  46111  fourierdlem7  46112  fourierdlem19  46124  fourierdlem26  46131  fourierdlem30  46135  fourierdlem48  46152  fourierdlem49  46153  fourierdlem51  46155  fourierdlem63  46167  fourierdlem64  46168  fourierdlem71  46175  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  sqwvfoura  46226  fourierswlem  46228  etransclem4  46236  etransclem31  46263  etransclem32  46264  cjnpoly  46890  iccpartgt  47428  upgrimpthslem2  47908  rege1logbrege0  48547  itcovalsuc  48656  ackvalsuc1mpt  48667  eenglngeehlnmlem2  48727  itsclc0yqsol  48753  itscnhlc0xyqsol  48754  itsclc0xyqsolr  48758  itsclinecirc0in  48764  itscnhlinecirc02p  48774  inlinecirc02plem  48775