Theorem gt0ne0d 11676

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

Syntax hints:   → wi 4   ≠ wne 2928   class class class wbr 5086  0cc0 11001   < clt 11141

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-resscn 11058  ax-1cn 11059  ax-addrcl 11062  ax-rnegex 11072  ax-cnre 11074  ax-pre-lttri 11075  ax-pre-lttrn 11076

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-po 5519  df-so 5520  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11143  df-mnf 11144  df-ltxr 11146

This theorem is referenced by:  recextlem2  11743  prodgt0  11963  ltdiv1  11981  ltmuldiv  11990  ltrec  11999  lerec  12000  lediv12a  12010  recp1lt1  12015  ledivp1  12019  supmul1  12086  nnne0  12154  rpnnen1lem5  12874  ltexp2a  14068  leexp2  14073  leexp2a  14074  expnbnd  14134  expmulnbnd  14137  discr1  14141  eqsqrt2d  15271  bpoly4  15961  isabvd  20722  gzrngunit  21365  fvmptnn04ifa  22760  chfacffsupp  22766  chfacfscmul0  22768  chfacfpmmul0  22772  stdbdxmet  24425  evth  24880  itg2monolem3  25675  mvth  25919  dvlip  25920  dvcvx  25947  ftc1lem4  25968  dgradd2  26196  radcnvlem1  26344  pilem2  26384  coseq00topi  26433  tangtx  26436  tanabsge  26437  cos02pilt1  26457  tanord1  26468  logcnlem4  26576  cxplt  26625  atantan  26855  jensenlem2  26920  jensen  26921  lgamgulmlem2  26962  basellem3  27015  basellem4  27016  basellem8  27020  dchrmusumlema  27426  selberg3lem1  27490  abvcxp  27548  ostth2  27570  axsegconlem8  28897  axsegconlem9  28898  axsegconlem10  28899  axpaschlem  28913  axcontlem2  28938  axcontlem4  28940  axcontlem7  28943  iswwlksnx  29813  wspn0  29897  friendshipgt3  30370  his6  31071  eigrei  31806  sgnmul  32810  sgn0bi  32815  sgnmulsgp  32818  cycpmco2lem4  33090  cycpmco2lem5  33091  finexttrb  33670  fldext2rspun  33687  cos9thpiminplylem1  33787  cos9thpiminply  33793  xrge0iifcv  33939  signsvfpn  34590  tgoldbachgtde  34665  tgoldbachgtda  34666  lfuhgr2  35155  knoppndvlem18  36563  knoppndvlem19  36564  knoppndvlem21  36566  ftc1cnnclem  37731  areacirclem1  37748  3lexlogpow2ineq1  42091  3lexlogpow2ineq2  42092  3lexlogpow5ineq5  42093  aks4d1p1p6  42106  aks6d1c4  42157  aks6d1c2  42163  aks6d1c6lem4  42206  sn-nnne0  42493  sn-recgt0d  42510  mulgt0b2d  42511  mulltgt0d  42515  mullt0b2d  42517  3cubeslem2  42718  irrapxlem2  42856  irrapxlem5  42859  pellexlem2  42863  imo72b2  44205  binomcxplemnotnn0  44389  dvdivbd  45961  dvbdfbdioolem1  45966  ioodvbdlimc1lem1  45969  ioodvbdlimc1lem2  45970  ioodvbdlimc2lem  45972  stoweidlem7  46045  stoweidlem36  46074  wallispilem3  46105  wallispilem4  46106  wallispi2lem1  46109  wallispi2lem2  46110  stirlinglem3  46114  stirlinglem6  46117  stirlinglem7  46118  stirlinglem10  46121  stirlinglem11  46122  stirlinglem12  46123  stirlinglem13  46124  stirlinglem14  46125  stirlinglem15  46126  dirkerval2  46132  dirkeritg  46140  dirkercncflem2  46142  fourierdlem6  46151  fourierdlem7  46152  fourierdlem19  46164  fourierdlem26  46171  fourierdlem30  46175  fourierdlem48  46192  fourierdlem49  46193  fourierdlem51  46195  fourierdlem63  46207  fourierdlem64  46208  fourierdlem71  46215  fourierdlem89  46233  fourierdlem90  46234  fourierdlem91  46235  fourierdlem103  46247  fourierdlem104  46248  fourierdlem112  46256  sqwvfoura  46266  fourierswlem  46268  etransclem4  46276  etransclem31  46303  etransclem32  46304  cjnpoly  46920  iccpartgt  47458  upgrimpthslem2  47939  rege1logbrege0  48590  itcovalsuc  48699  ackvalsuc1mpt  48710  eenglngeehlnmlem2  48770  itsclc0yqsol  48796  itscnhlc0xyqsol  48797  itsclc0xyqsolr  48801  itsclinecirc0in  48807  itscnhlinecirc02p  48817  inlinecirc02plem  48818