Theorem gt0ne0d 11713

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		0red 11147	. 2 ⊢ (𝜑 → 0 ∈ ℝ)
2		gt0ne0d.1	. 2 ⊢ (𝜑 → 0 < 𝐴)
3	1, 2	gtned 11280	1 ⊢ (𝜑 → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ≠ wne 2933   class class class wbr 5100  0cc0 11038   < clt 11178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-addrcl 11099  ax-rnegex 11109  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-ltxr 11183

This theorem is referenced by:  recextlem2  11780  prodgt0  12000  ltdiv1  12018  ltmuldiv  12027  ltrec  12036  lerec  12037  lediv12a  12047  recp1lt1  12052  ledivp1  12056  supmul1  12123  nnne0  12191  rpnnen1lem5  12906  ltexp2a  14101  leexp2  14106  leexp2a  14107  expnbnd  14167  expmulnbnd  14170  discr1  14174  eqsqrt2d  15304  bpoly4  15994  isabvd  20757  gzrngunit  21400  fvmptnn04ifa  22806  chfacffsupp  22812  chfacfscmul0  22814  chfacfpmmul0  22818  stdbdxmet  24471  evth  24926  itg2monolem3  25721  mvth  25965  dvlip  25966  dvcvx  25993  ftc1lem4  26014  dgradd2  26242  radcnvlem1  26390  pilem2  26430  coseq00topi  26479  tangtx  26482  tanabsge  26483  cos02pilt1  26503  tanord1  26514  logcnlem4  26622  cxplt  26671  atantan  26901  jensenlem2  26966  jensen  26967  lgamgulmlem2  27008  basellem3  27061  basellem4  27062  basellem8  27066  dchrmusumlema  27472  selberg3lem1  27536  abvcxp  27594  ostth2  27616  axsegconlem8  29009  axsegconlem9  29010  axsegconlem10  29011  axpaschlem  29025  axcontlem2  29050  axcontlem4  29052  axcontlem7  29055  iswwlksnx  29925  wspn0  30009  friendshipgt3  30485  his6  31187  eigrei  31922  sgnmul  32927  sgn0bi  32932  sgnmulsgp  32935  cycpmco2lem4  33223  cycpmco2lem5  33224  finexttrb  33843  fldext2rspun  33860  cos9thpiminplylem1  33960  cos9thpiminply  33966  xrge0iifcv  34112  signsvfpn  34763  tgoldbachgtde  34838  tgoldbachgtda  34839  lfuhgr2  35335  knoppndvlem18  36751  knoppndvlem19  36752  knoppndvlem21  36754  ftc1cnnclem  37942  areacirclem1  37959  3lexlogpow2ineq1  42428  3lexlogpow2ineq2  42429  3lexlogpow5ineq5  42430  aks4d1p1p6  42443  aks6d1c4  42494  aks6d1c2  42500  aks6d1c6lem4  42543  sn-nnne0  42830  sn-recgt0d  42847  mulgt0b2d  42848  mulltgt0d  42852  mullt0b2d  42854  3cubeslem2  43042  irrapxlem2  43180  irrapxlem5  43183  pellexlem2  43187  imo72b2  44528  binomcxplemnotnn0  44712  dvdivbd  46281  dvbdfbdioolem1  46286  ioodvbdlimc1lem1  46289  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  stoweidlem7  46365  stoweidlem36  46394  wallispilem3  46425  wallispilem4  46426  wallispi2lem1  46429  wallispi2lem2  46430  stirlinglem3  46434  stirlinglem6  46437  stirlinglem7  46438  stirlinglem10  46441  stirlinglem11  46442  stirlinglem12  46443  stirlinglem13  46444  stirlinglem14  46445  stirlinglem15  46446  dirkerval2  46452  dirkeritg  46460  dirkercncflem2  46462  fourierdlem6  46471  fourierdlem7  46472  fourierdlem19  46484  fourierdlem26  46491  fourierdlem30  46495  fourierdlem48  46512  fourierdlem49  46513  fourierdlem51  46515  fourierdlem63  46527  fourierdlem64  46528  fourierdlem71  46535  fourierdlem89  46553  fourierdlem90  46554  fourierdlem91  46555  fourierdlem103  46567  fourierdlem104  46568  fourierdlem112  46576  sqwvfoura  46586  fourierswlem  46588  etransclem4  46596  etransclem31  46623  etransclem32  46624  cjnpoly  47249  iccpartgt  47787  upgrimpthslem2  48268  rege1logbrege0  48918  itcovalsuc  49027  ackvalsuc1mpt  49038  eenglngeehlnmlem2  49098  itsclc0yqsol  49124  itscnhlc0xyqsol  49125  itsclc0xyqsolr  49129  itsclinecirc0in  49135  itscnhlinecirc02p  49145  inlinecirc02plem  49146