Theorem gt0ne0d 11745

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

Syntax hints:   → wi 4   ≠ wne 2956   class class class wbr 5097  0cc0 11067   < clt 11210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-resscn 11124  ax-1cn 11125  ax-addrcl 11128  ax-rnegex 11138  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-po 5551  df-so 5552  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-ltxr 11215

This theorem is referenced by:  recextlem2  11812  prodgt0  12032  ltdiv1  12050  ltmuldiv  12059  ltrec  12068  lerec  12069  lediv12a  12079  recp1lt1  12084  ledivp1  12088  supmul1  12155  nnne0  12241  rpnnen1lem5  12976  ltexp2a  14173  leexp2  14178  leexp2a  14179  expnbnd  14239  expmulnbnd  14242  discr1  14246  sgn0bi  15107  sgnmul  15111  eqsqrt2d  15387  bpoly4  16080  isabvd  20849  gzrngunit  21473  fvmptnn04ifa  22898  chfacffsupp  22904  chfacfscmul0  22906  chfacfpmmul0  22910  stdbdxmet  24563  evth  25009  itg2monolem3  25802  mvth  26042  dvlip  26043  dvcvx  26070  ftc1lem4  26089  dgradd2  26316  radcnvlem1  26464  pilem2  26503  coseq00topi  26555  tangtx  26558  tanabsge  26559  cos02pilt1  26579  tanord1  26590  logcnlem4  26698  cxplt  26747  atantan  26976  jensenlem2  27040  jensen  27041  lgamgulmlem2  27082  basellem3  27135  basellem4  27136  basellem8  27140  dchrmusumlema  27545  selberg3lem1  27609  abvcxp  27667  ostth2  27689  axsegconlem8  29082  axsegconlem9  29083  axsegconlem10  29084  axpaschlem  29098  axcontlem2  29123  axcontlem4  29125  axcontlem7  29128  iswwlksnx  29997  wspn0  30081  friendshipgt3  30557  his6  31259  eigrei  31994  sgnmulsgp  32995  cycpmco2lem4  33270  cycpmco2lem5  33271  finexttrb  33923  fldext2rspun  33940  cos9thpiminplylem1  34040  cos9thpiminply  34046  xrge0iifcv  34192  signsvfpn  34840  tgoldbachgtde  34915  tgoldbachgtda  34916  lfuhgr2  35430  knoppndvlem18  36928  knoppndvlem19  36929  knoppndvlem21  36931  ftc1cnnclem  38151  areacirclem1  38168  3lexlogpow2ineq1  42636  3lexlogpow2ineq2  42637  3lexlogpow5ineq5  42638  aks4d1p1p6  42651  aks6d1c4  42702  aks6d1c2  42708  aks6d1c6lem4  42751  sn-nnne0  43043  sn-recgt0d  43060  mulgt0b2d  43061  mulltgt0d  43065  mullt0b2d  43067  3cubeslem2  43227  irrapxlem2  43361  irrapxlem5  43364  pellexlem2  43368  imo72b2  44709  binomcxplemnotnn0  44893  dvdivbd  46458  dvbdfbdioolem1  46463  ioodvbdlimc1lem1  46466  ioodvbdlimc1lem2  46467  ioodvbdlimc2lem  46469  stoweidlem7  46542  stoweidlem36  46571  wallispilem3  46602  wallispilem4  46603  wallispi2lem1  46606  wallispi2lem2  46607  stirlinglem3  46611  stirlinglem6  46614  stirlinglem7  46615  stirlinglem10  46618  stirlinglem11  46619  stirlinglem12  46620  stirlinglem13  46621  stirlinglem14  46622  stirlinglem15  46623  dirkerval2  46629  dirkeritg  46637  dirkercncflem2  46639  fourierdlem6  46648  fourierdlem7  46649  fourierdlem19  46661  fourierdlem26  46668  fourierdlem30  46672  fourierdlem48  46689  fourierdlem49  46690  fourierdlem51  46692  fourierdlem63  46704  fourierdlem64  46705  fourierdlem71  46712  fourierdlem89  46730  fourierdlem90  46731  fourierdlem91  46732  fourierdlem103  46744  fourierdlem104  46745  fourierdlem112  46753  sqwvfoura  46763  fourierswlem  46765  etransclem4  46773  etransclem31  46800  etransclem32  46801  cjnpoly  47444  iccpartgt  47994  upgrimpthslem2  48491  rege1logbrege0  49141  itcovalsuc  49250  ackvalsuc1mpt  49261  eenglngeehlnmlem2  49321  itsclc0yqsol  49347  itscnhlc0xyqsol  49348  itsclc0xyqsolr  49352  itsclinecirc0in  49358  itscnhlinecirc02p  49368  inlinecirc02plem  49369