Theorem gt0ne0d 11207

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

Syntax hints:   → wi 4   ∈ wcel 2113   ≠ wne 3019   class class class wbr 5069  ℝcr 10539  0cc0 10540   < clt 10678

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-resscn 10597  ax-1cn 10598  ax-addrcl 10601  ax-rnegex 10611  ax-cnre 10613  ax-pre-lttri 10614  ax-pre-lttrn 10615

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-nel 3127  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-po 5477  df-so 5478  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-er 8292  df-en 8513  df-dom 8514  df-sdom 8515  df-pnf 10680  df-mnf 10681  df-ltxr 10683

This theorem is referenced by:  recextlem2  11274  prodgt0  11490  ltdiv1  11507  ltmuldiv  11516  ltrec  11525  lerec  11526  lediv12a  11536  recp1lt1  11541  ledivp1  11545  supmul1  11613  nnne0  11674  rpnnen1lem5  12383  ltexp2a  13533  leexp2  13538  leexp2a  13539  expnbnd  13596  expmulnbnd  13599  discr1  13603  eqsqrt2d  14731  bpoly4  15416  isabvd  19594  gzrngunit  20614  fvmptnn04ifa  21461  chfacffsupp  21467  chfacfscmul0  21469  chfacfpmmul0  21473  stdbdxmet  23128  evth  23566  itg2monolem3  24356  mvth  24592  dvlip  24593  dvcvx  24620  ftc1lem4  24639  dgradd2  24861  radcnvlem1  25004  pilem2  25043  coseq00topi  25091  tangtx  25094  tanabsge  25095  cos02pilt1  25114  tanord1  25124  logcnlem4  25231  cxplt  25280  atantan  25504  jensenlem2  25568  jensen  25569  lgamgulmlem2  25610  basellem3  25663  basellem4  25664  basellem8  25668  dchrmusumlema  26072  selberg3lem1  26136  abvcxp  26194  ostth2  26216  axsegconlem8  26713  axsegconlem9  26714  axsegconlem10  26715  axpaschlem  26729  axcontlem2  26754  axcontlem4  26756  axcontlem7  26759  iswwlksnx  27621  wspn0  27706  friendshipgt3  28180  his6  28879  eigrei  29614  cycpmco2lem4  30775  cycpmco2lem5  30776  finexttrb  31056  xrge0iifcv  31181  sgnmul  31804  sgn0bi  31809  sgnmulsgp  31812  signsvfpn  31859  tgoldbachgtde  31935  tgoldbachgtda  31936  lfuhgr2  32369  knoppndvlem18  33872  knoppndvlem19  33873  knoppndvlem21  33875  ftc1cnnclem  34969  areacirclem1  34986  3cubeslem2  39288  irrapxlem2  39426  irrapxlem5  39429  pellexlem2  39433  imo72b2  40531  binomcxplemnotnn0  40694  dvdivbd  42214  dvbdfbdioolem1  42219  ioodvbdlimc1lem1  42222  ioodvbdlimc1lem2  42223  ioodvbdlimc2lem  42225  stoweidlem7  42299  stoweidlem36  42328  wallispilem3  42359  wallispilem4  42360  wallispi2lem1  42363  wallispi2lem2  42364  stirlinglem3  42368  stirlinglem6  42371  stirlinglem7  42372  stirlinglem10  42375  stirlinglem11  42376  stirlinglem12  42377  stirlinglem13  42378  stirlinglem14  42379  stirlinglem15  42380  dirkerval2  42386  dirkeritg  42394  dirkercncflem2  42396  fourierdlem6  42405  fourierdlem7  42406  fourierdlem19  42418  fourierdlem26  42425  fourierdlem30  42429  fourierdlem48  42446  fourierdlem49  42447  fourierdlem51  42449  fourierdlem63  42461  fourierdlem64  42462  fourierdlem71  42469  fourierdlem89  42487  fourierdlem90  42488  fourierdlem91  42489  fourierdlem103  42501  fourierdlem104  42502  fourierdlem112  42510  sqwvfoura  42520  fourierswlem  42522  etransclem4  42530  etransclem31  42557  etransclem32  42558  iccpartgt  43594  rege1logbrege0  44625  eenglngeehlnmlem2  44732  itsclc0yqsol  44758  itscnhlc0xyqsol  44759  itsclc0xyqsolr  44763  itsclinecirc0in  44769  itscnhlinecirc02p  44779  inlinecirc02plem  44780