Theorem gt0ne0d 11819

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		0re 11257	. 2 ⊢ 0 ∈ ℝ
2		gt0ne0d.1	. 2 ⊢ (𝜑 → 0 < 𝐴)
3		ltne 11352	. 2 ⊢ ((0 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 ≠ 0)
4	1, 2, 3	sylancr 585	1 ⊢ (𝜑 → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∈ wcel 2099   ≠ wne 2930   class class class wbr 5145  ℝcr 11148  0cc0 11149   < clt 11289

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738  ax-resscn 11206  ax-1cn 11207  ax-addrcl 11210  ax-rnegex 11220  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5146  df-opab 5208  df-mpt 5229  df-id 5572  df-po 5586  df-so 5587  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-er 8726  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11291  df-mnf 11292  df-ltxr 11294

This theorem is referenced by:  recextlem2  11886  prodgt0  12106  ltdiv1  12124  ltmuldiv  12133  ltrec  12142  lerec  12143  lediv12a  12153  recp1lt1  12158  ledivp1  12162  supmul1  12229  nnne0  12292  rpnnen1lem5  13011  ltexp2a  14179  leexp2  14184  leexp2a  14185  expnbnd  14244  expmulnbnd  14247  discr1  14251  eqsqrt2d  15368  bpoly4  16056  isabvd  20787  gzrngunit  21426  fvmptnn04ifa  22840  chfacffsupp  22846  chfacfscmul0  22848  chfacfpmmul0  22852  stdbdxmet  24512  evth  24973  itg2monolem3  25770  mvth  26013  dvlip  26014  dvcvx  26041  ftc1lem4  26062  dgradd2  26293  radcnvlem1  26439  pilem2  26479  coseq00topi  26527  tangtx  26530  tanabsge  26531  cos02pilt1  26550  tanord1  26561  logcnlem4  26669  cxplt  26718  atantan  26948  jensenlem2  27013  jensen  27014  lgamgulmlem2  27055  basellem3  27108  basellem4  27109  basellem8  27113  dchrmusumlema  27519  selberg3lem1  27583  abvcxp  27641  ostth2  27663  axsegconlem8  28855  axsegconlem9  28856  axsegconlem10  28857  axpaschlem  28871  axcontlem2  28896  axcontlem4  28898  axcontlem7  28901  iswwlksnx  29771  wspn0  29855  friendshipgt3  30328  his6  31029  eigrei  31764  cycpmco2lem4  33011  cycpmco2lem5  33012  finexttrb  33557  xrge0iifcv  33762  sgnmul  34389  sgn0bi  34394  sgnmulsgp  34397  signsvfpn  34444  tgoldbachgtde  34519  tgoldbachgtda  34520  lfuhgr2  34959  knoppndvlem18  36245  knoppndvlem19  36246  knoppndvlem21  36248  ftc1cnnclem  37405  areacirclem1  37422  3lexlogpow2ineq1  41770  3lexlogpow2ineq2  41771  3lexlogpow5ineq5  41772  aks4d1p1p6  41785  aks6d1c4  41836  aks6d1c2  41842  aks6d1c6lem4  41885  sn-nnne0  42159  3cubeslem2  42379  irrapxlem2  42517  irrapxlem5  42520  pellexlem2  42524  imo72b2  43876  binomcxplemnotnn0  44067  dvdivbd  45580  dvbdfbdioolem1  45585  ioodvbdlimc1lem1  45588  ioodvbdlimc1lem2  45589  ioodvbdlimc2lem  45591  stoweidlem7  45664  stoweidlem36  45693  wallispilem3  45724  wallispilem4  45725  wallispi2lem1  45728  wallispi2lem2  45729  stirlinglem3  45733  stirlinglem6  45736  stirlinglem7  45737  stirlinglem10  45740  stirlinglem11  45741  stirlinglem12  45742  stirlinglem13  45743  stirlinglem14  45744  stirlinglem15  45745  dirkerval2  45751  dirkeritg  45759  dirkercncflem2  45761  fourierdlem6  45770  fourierdlem7  45771  fourierdlem19  45783  fourierdlem26  45790  fourierdlem30  45794  fourierdlem48  45811  fourierdlem49  45812  fourierdlem51  45814  fourierdlem63  45826  fourierdlem64  45827  fourierdlem71  45834  fourierdlem89  45852  fourierdlem90  45853  fourierdlem91  45854  fourierdlem103  45866  fourierdlem104  45867  fourierdlem112  45875  sqwvfoura  45885  fourierswlem  45887  etransclem4  45895  etransclem31  45922  etransclem32  45923  iccpartgt  47035  rege1logbrege0  47982  itcovalsuc  48091  ackvalsuc1mpt  48102  eenglngeehlnmlem2  48162  itsclc0yqsol  48188  itscnhlc0xyqsol  48189  itsclc0xyqsolr  48193  itsclinecirc0in  48199  itscnhlinecirc02p  48209  inlinecirc02plem  48210