Theorem gt0ne0d 11701

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

Syntax hints:   → wi 4   ≠ wne 2932   class class class wbr 5098  0cc0 11026   < clt 11166

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 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-addrcl 11087  ax-rnegex 11097  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-ltxr 11171

This theorem is referenced by:  recextlem2  11768  prodgt0  11988  ltdiv1  12006  ltmuldiv  12015  ltrec  12024  lerec  12025  lediv12a  12035  recp1lt1  12040  ledivp1  12044  supmul1  12111  nnne0  12179  rpnnen1lem5  12894  ltexp2a  14089  leexp2  14094  leexp2a  14095  expnbnd  14155  expmulnbnd  14158  discr1  14162  eqsqrt2d  15292  bpoly4  15982  isabvd  20745  gzrngunit  21388  fvmptnn04ifa  22794  chfacffsupp  22800  chfacfscmul0  22802  chfacfpmmul0  22806  stdbdxmet  24459  evth  24914  itg2monolem3  25709  mvth  25953  dvlip  25954  dvcvx  25981  ftc1lem4  26002  dgradd2  26230  radcnvlem1  26378  pilem2  26418  coseq00topi  26467  tangtx  26470  tanabsge  26471  cos02pilt1  26491  tanord1  26502  logcnlem4  26610  cxplt  26659  atantan  26889  jensenlem2  26954  jensen  26955  lgamgulmlem2  26996  basellem3  27049  basellem4  27050  basellem8  27054  dchrmusumlema  27460  selberg3lem1  27524  abvcxp  27582  ostth2  27604  axsegconlem8  28997  axsegconlem9  28998  axsegconlem10  28999  axpaschlem  29013  axcontlem2  29038  axcontlem4  29040  axcontlem7  29043  iswwlksnx  29913  wspn0  29997  friendshipgt3  30473  his6  31174  eigrei  31909  sgnmul  32916  sgn0bi  32921  sgnmulsgp  32924  cycpmco2lem4  33211  cycpmco2lem5  33212  finexttrb  33822  fldext2rspun  33839  cos9thpiminplylem1  33939  cos9thpiminply  33945  xrge0iifcv  34091  signsvfpn  34742  tgoldbachgtde  34817  tgoldbachgtda  34818  lfuhgr2  35313  knoppndvlem18  36729  knoppndvlem19  36730  knoppndvlem21  36732  ftc1cnnclem  37892  areacirclem1  37909  3lexlogpow2ineq1  42312  3lexlogpow2ineq2  42313  3lexlogpow5ineq5  42314  aks4d1p1p6  42327  aks6d1c4  42378  aks6d1c2  42384  aks6d1c6lem4  42427  sn-nnne0  42715  sn-recgt0d  42732  mulgt0b2d  42733  mulltgt0d  42737  mullt0b2d  42739  3cubeslem2  42927  irrapxlem2  43065  irrapxlem5  43068  pellexlem2  43072  imo72b2  44413  binomcxplemnotnn0  44597  dvdivbd  46167  dvbdfbdioolem1  46172  ioodvbdlimc1lem1  46175  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  stoweidlem7  46251  stoweidlem36  46280  wallispilem3  46311  wallispilem4  46312  wallispi2lem1  46315  wallispi2lem2  46316  stirlinglem3  46320  stirlinglem6  46323  stirlinglem7  46324  stirlinglem10  46327  stirlinglem11  46328  stirlinglem12  46329  stirlinglem13  46330  stirlinglem14  46331  stirlinglem15  46332  dirkerval2  46338  dirkeritg  46346  dirkercncflem2  46348  fourierdlem6  46357  fourierdlem7  46358  fourierdlem19  46370  fourierdlem26  46377  fourierdlem30  46381  fourierdlem48  46398  fourierdlem49  46399  fourierdlem51  46401  fourierdlem63  46413  fourierdlem64  46414  fourierdlem71  46421  fourierdlem89  46439  fourierdlem90  46440  fourierdlem91  46441  fourierdlem103  46453  fourierdlem104  46454  fourierdlem112  46462  sqwvfoura  46472  fourierswlem  46474  etransclem4  46482  etransclem31  46509  etransclem32  46510  cjnpoly  47135  iccpartgt  47673  upgrimpthslem2  48154  rege1logbrege0  48804  itcovalsuc  48913  ackvalsuc1mpt  48924  eenglngeehlnmlem2  48984  itsclc0yqsol  49010  itscnhlc0xyqsol  49011  itsclc0xyqsolr  49015  itsclinecirc0in  49021  itscnhlinecirc02p  49031  inlinecirc02plem  49032