Theorem gt0ne0d 11396

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

Syntax hints:   → wi 4   ∈ wcel 2110   ≠ wne 2940   class class class wbr 5053  ℝcr 10728  0cc0 10729   < clt 10867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-resscn 10786  ax-1cn 10787  ax-addrcl 10790  ax-rnegex 10800  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-po 5468  df-so 5469  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-pnf 10869  df-mnf 10870  df-ltxr 10872

This theorem is referenced by:  recextlem2  11463  prodgt0  11679  ltdiv1  11696  ltmuldiv  11705  ltrec  11714  lerec  11715  lediv12a  11725  recp1lt1  11730  ledivp1  11734  supmul1  11801  nnne0  11864  rpnnen1lem5  12577  ltexp2a  13736  leexp2  13741  leexp2a  13742  expnbnd  13799  expmulnbnd  13802  discr1  13806  eqsqrt2d  14932  bpoly4  15621  isabvd  19856  gzrngunit  20429  fvmptnn04ifa  21747  chfacffsupp  21753  chfacfscmul0  21755  chfacfpmmul0  21759  stdbdxmet  23413  evth  23856  itg2monolem3  24650  mvth  24889  dvlip  24890  dvcvx  24917  ftc1lem4  24936  dgradd2  25162  radcnvlem1  25305  pilem2  25344  coseq00topi  25392  tangtx  25395  tanabsge  25396  cos02pilt1  25415  tanord1  25426  logcnlem4  25533  cxplt  25582  atantan  25806  jensenlem2  25870  jensen  25871  lgamgulmlem2  25912  basellem3  25965  basellem4  25966  basellem8  25970  dchrmusumlema  26374  selberg3lem1  26438  abvcxp  26496  ostth2  26518  axsegconlem8  27015  axsegconlem9  27016  axsegconlem10  27017  axpaschlem  27031  axcontlem2  27056  axcontlem4  27058  axcontlem7  27061  iswwlksnx  27924  wspn0  28008  friendshipgt3  28481  his6  29180  eigrei  29915  cycpmco2lem4  31115  cycpmco2lem5  31116  finexttrb  31451  xrge0iifcv  31598  sgnmul  32221  sgn0bi  32226  sgnmulsgp  32229  signsvfpn  32276  tgoldbachgtde  32352  tgoldbachgtda  32353  lfuhgr2  32793  knoppndvlem18  34446  knoppndvlem19  34447  knoppndvlem21  34449  ftc1cnnclem  35585  areacirclem1  35602  3lexlogpow2ineq1  39800  3lexlogpow2ineq2  39801  3lexlogpow5ineq5  39802  aks4d1p1p6  39814  3cubeslem2  40210  irrapxlem2  40348  irrapxlem5  40351  pellexlem2  40355  imo72b2  41461  binomcxplemnotnn0  41647  dvdivbd  43139  dvbdfbdioolem1  43144  ioodvbdlimc1lem1  43147  ioodvbdlimc1lem2  43148  ioodvbdlimc2lem  43150  stoweidlem7  43223  stoweidlem36  43252  wallispilem3  43283  wallispilem4  43284  wallispi2lem1  43287  wallispi2lem2  43288  stirlinglem3  43292  stirlinglem6  43295  stirlinglem7  43296  stirlinglem10  43299  stirlinglem11  43300  stirlinglem12  43301  stirlinglem13  43302  stirlinglem14  43303  stirlinglem15  43304  dirkerval2  43310  dirkeritg  43318  dirkercncflem2  43320  fourierdlem6  43329  fourierdlem7  43330  fourierdlem19  43342  fourierdlem26  43349  fourierdlem30  43353  fourierdlem48  43370  fourierdlem49  43371  fourierdlem51  43373  fourierdlem63  43385  fourierdlem64  43386  fourierdlem71  43393  fourierdlem89  43411  fourierdlem90  43412  fourierdlem91  43413  fourierdlem103  43425  fourierdlem104  43426  fourierdlem112  43434  sqwvfoura  43444  fourierswlem  43446  etransclem4  43454  etransclem31  43481  etransclem32  43482  iccpartgt  44552  rege1logbrege0  45577  itcovalsuc  45686  ackvalsuc1mpt  45697  eenglngeehlnmlem2  45757  itsclc0yqsol  45783  itscnhlc0xyqsol  45784  itsclc0xyqsolr  45788  itsclinecirc0in  45794  itscnhlinecirc02p  45804  inlinecirc02plem  45805