Theorem gt0ne0d 10471

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

Syntax hints:   → wi 4   ∈ wcel 1977   ≠ wne 2780   class class class wbr 4583  ℝcr 9814  0cc0 9815   < clt 9953

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-ltxr 9958

This theorem is referenced by:  recextlem2  10537  prodgt0  10747  ltdiv1  10766  ltmuldiv  10775  ltrec  10784  lerec  10785  lediv12a  10795  recp1lt1  10800  ledivp1  10804  supmul1  10869  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  ltexp2a  12774  leexp2  12777  leexp2a  12778  expnbnd  12855  expmulnbnd  12858  discr1  12862  eqsqrt2d  13956  bpoly4  14629  isabvd  18643  gzrngunit  19631  fvmptnn04ifa  20474  chfacffsupp  20480  chfacfscmul0  20482  chfacfpmmul0  20486  stdbdxmet  22130  evth  22566  itg2monolem3  23325  mvth  23559  dvlip  23560  dvcvx  23587  ftc1lem4  23606  dgradd2  23828  radcnvlem1  23971  pilem2  24010  coseq00topi  24058  tangtx  24061  tanabsge  24062  tanord1  24087  logcnlem4  24191  cxplt  24240  atantan  24450  jensenlem2  24514  jensen  24515  lgamgulmlem2  24556  basellem3  24609  basellem4  24610  basellem8  24614  dchrmusumlema  24982  selberg3lem1  25046  abvcxp  25104  ostth2  25126  axsegconlem8  25604  axsegconlem9  25605  axsegconlem10  25606  axpaschlem  25620  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  clwwlkn0  26302  friendshipgt3  26648  his6  27340  eigrei  28077  xrge0iifcv  29308  sgnmul  29931  sgn0bi  29936  sgnmulsgp  29939  signsvfpn  29988  knoppndvlem18  31690  knoppndvlem19  31691  knoppndvlem21  31693  ftc1cnnclem  32653  areacirclem1  32670  irrapxlem2  36405  irrapxlem5  36408  pellexlem2  36412  imo72b2  37497  binomcxplemnotnn0  37577  dvdivbd  38813  dvbdfbdioolem1  38818  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  stoweidlem7  38900  stoweidlem36  38929  wallispilem3  38960  wallispilem4  38961  wallispi2lem1  38964  wallispi2lem2  38965  stirlinglem3  38969  stirlinglem6  38972  stirlinglem7  38973  stirlinglem10  38976  stirlinglem11  38977  stirlinglem12  38978  stirlinglem13  38979  stirlinglem14  38980  stirlinglem15  38981  dirkerval2  38987  dirkeritg  38995  dirkercncflem2  38997  fourierdlem6  39006  fourierdlem7  39007  fourierdlem19  39019  fourierdlem26  39026  fourierdlem30  39030  fourierdlem48  39047  fourierdlem49  39048  fourierdlem51  39050  fourierdlem63  39062  fourierdlem64  39063  fourierdlem71  39070  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  sqwvfoura  39121  fourierswlem  39123  etransclem4  39131  etransclem31  39158  etransclem32  39159  iccpartgt  39965  iswwlksnx  41042  wspn0  41131  av-friendshipgt3  41552  rege1logbrege0  42150