Theorem gt0ne0d 11824

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

Syntax hints:   → wi 4   ∈ wcel 2105   ≠ wne 2937   class class class wbr 5147  ℝcr 11151  0cc0 11152   < clt 11292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-1cn 11210  ax-addrcl 11213  ax-rnegex 11223  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-ltxr 11297

This theorem is referenced by:  recextlem2  11891  prodgt0  12111  ltdiv1  12129  ltmuldiv  12138  ltrec  12147  lerec  12148  lediv12a  12158  recp1lt1  12163  ledivp1  12167  supmul1  12234  nnne0  12297  rpnnen1lem5  13020  ltexp2a  14202  leexp2  14207  leexp2a  14208  expnbnd  14267  expmulnbnd  14270  discr1  14274  eqsqrt2d  15403  bpoly4  16091  isabvd  20829  gzrngunit  21468  fvmptnn04ifa  22871  chfacffsupp  22877  chfacfscmul0  22879  chfacfpmmul0  22883  stdbdxmet  24543  evth  25004  itg2monolem3  25801  mvth  26045  dvlip  26046  dvcvx  26073  ftc1lem4  26094  dgradd2  26322  radcnvlem1  26470  pilem2  26510  coseq00topi  26558  tangtx  26561  tanabsge  26562  cos02pilt1  26582  tanord1  26593  logcnlem4  26701  cxplt  26750  atantan  26980  jensenlem2  27045  jensen  27046  lgamgulmlem2  27087  basellem3  27140  basellem4  27141  basellem8  27145  dchrmusumlema  27551  selberg3lem1  27615  abvcxp  27673  ostth2  27695  axsegconlem8  28953  axsegconlem9  28954  axsegconlem10  28955  axpaschlem  28969  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  iswwlksnx  29869  wspn0  29953  friendshipgt3  30426  his6  31127  eigrei  31862  cycpmco2lem4  33131  cycpmco2lem5  33132  finexttrb  33689  xrge0iifcv  33894  sgnmul  34523  sgn0bi  34528  sgnmulsgp  34531  signsvfpn  34578  tgoldbachgtde  34653  tgoldbachgtda  34654  lfuhgr2  35102  knoppndvlem18  36511  knoppndvlem19  36512  knoppndvlem21  36514  ftc1cnnclem  37677  areacirclem1  37694  3lexlogpow2ineq1  42039  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1p1p6  42054  aks6d1c4  42105  aks6d1c2  42111  aks6d1c6lem4  42154  sn-nnne0  42454  3cubeslem2  42672  irrapxlem2  42810  irrapxlem5  42813  pellexlem2  42817  imo72b2  44161  binomcxplemnotnn0  44351  dvdivbd  45878  dvbdfbdioolem1  45883  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  stoweidlem7  45962  stoweidlem36  45991  wallispilem3  46022  wallispilem4  46023  wallispi2lem1  46026  wallispi2lem2  46027  stirlinglem3  46031  stirlinglem6  46034  stirlinglem7  46035  stirlinglem10  46038  stirlinglem11  46039  stirlinglem12  46040  stirlinglem13  46041  stirlinglem14  46042  stirlinglem15  46043  dirkerval2  46049  dirkeritg  46057  dirkercncflem2  46059  fourierdlem6  46068  fourierdlem7  46069  fourierdlem19  46081  fourierdlem26  46088  fourierdlem30  46092  fourierdlem48  46109  fourierdlem49  46110  fourierdlem51  46112  fourierdlem63  46124  fourierdlem64  46125  fourierdlem71  46132  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  sqwvfoura  46183  fourierswlem  46185  etransclem4  46193  etransclem31  46220  etransclem32  46221  iccpartgt  47351  rege1logbrege0  48407  itcovalsuc  48516  ackvalsuc1mpt  48527  eenglngeehlnmlem2  48587  itsclc0yqsol  48613  itscnhlc0xyqsol  48614  itsclc0xyqsolr  48618  itsclinecirc0in  48624  itscnhlinecirc02p  48634  inlinecirc02plem  48635