Theorem gt0ne0d 11718

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

Syntax hints:   → wi 4   ≠ wne 2925   class class class wbr 5102  0cc0 11044   < clt 11184

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-addrcl 11105  ax-rnegex 11115  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-ltxr 11189

This theorem is referenced by:  recextlem2  11785  prodgt0  12005  ltdiv1  12023  ltmuldiv  12032  ltrec  12041  lerec  12042  lediv12a  12052  recp1lt1  12057  ledivp1  12061  supmul1  12128  nnne0  12196  rpnnen1lem5  12916  ltexp2a  14107  leexp2  14112  leexp2a  14113  expnbnd  14173  expmulnbnd  14176  discr1  14180  eqsqrt2d  15311  bpoly4  16001  isabvd  20697  gzrngunit  21326  fvmptnn04ifa  22713  chfacffsupp  22719  chfacfscmul0  22721  chfacfpmmul0  22725  stdbdxmet  24379  evth  24834  itg2monolem3  25629  mvth  25873  dvlip  25874  dvcvx  25901  ftc1lem4  25922  dgradd2  26150  radcnvlem1  26298  pilem2  26338  coseq00topi  26387  tangtx  26390  tanabsge  26391  cos02pilt1  26411  tanord1  26422  logcnlem4  26530  cxplt  26579  atantan  26809  jensenlem2  26874  jensen  26875  lgamgulmlem2  26916  basellem3  26969  basellem4  26970  basellem8  26974  dchrmusumlema  27380  selberg3lem1  27444  abvcxp  27502  ostth2  27524  axsegconlem8  28827  axsegconlem9  28828  axsegconlem10  28829  axpaschlem  28843  axcontlem2  28868  axcontlem4  28870  axcontlem7  28873  iswwlksnx  29743  wspn0  29827  friendshipgt3  30300  his6  31001  eigrei  31736  sgnmul  32733  sgn0bi  32738  sgnmulsgp  32741  cycpmco2lem4  33059  cycpmco2lem5  33060  finexttrb  33633  fldext2rspun  33650  cos9thpiminplylem1  33745  cos9thpiminply  33751  xrge0iifcv  33897  signsvfpn  34549  tgoldbachgtde  34624  tgoldbachgtda  34625  lfuhgr2  35079  knoppndvlem18  36490  knoppndvlem19  36491  knoppndvlem21  36493  ftc1cnnclem  37658  areacirclem1  37675  3lexlogpow2ineq1  42019  3lexlogpow2ineq2  42020  3lexlogpow5ineq5  42021  aks4d1p1p6  42034  aks6d1c4  42085  aks6d1c2  42091  aks6d1c6lem4  42134  sn-nnne0  42421  sn-recgt0d  42438  mulgt0b2d  42439  mulltgt0d  42443  mullt0b2d  42445  3cubeslem2  42646  irrapxlem2  42784  irrapxlem5  42787  pellexlem2  42791  imo72b2  44134  binomcxplemnotnn0  44318  dvdivbd  45894  dvbdfbdioolem1  45899  ioodvbdlimc1lem1  45902  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  stoweidlem7  45978  stoweidlem36  46007  wallispilem3  46038  wallispilem4  46039  wallispi2lem1  46042  wallispi2lem2  46043  stirlinglem3  46047  stirlinglem6  46050  stirlinglem7  46051  stirlinglem10  46054  stirlinglem11  46055  stirlinglem12  46056  stirlinglem13  46057  stirlinglem14  46058  stirlinglem15  46059  dirkerval2  46065  dirkeritg  46073  dirkercncflem2  46075  fourierdlem6  46084  fourierdlem7  46085  fourierdlem19  46097  fourierdlem26  46104  fourierdlem30  46108  fourierdlem48  46125  fourierdlem49  46126  fourierdlem51  46128  fourierdlem63  46140  fourierdlem64  46141  fourierdlem71  46148  fourierdlem89  46166  fourierdlem90  46167  fourierdlem91  46168  fourierdlem103  46180  fourierdlem104  46181  fourierdlem112  46189  sqwvfoura  46199  fourierswlem  46201  etransclem4  46209  etransclem31  46236  etransclem32  46237  cjnpoly  46863  iccpartgt  47401  upgrimpthslem2  47881  rege1logbrege0  48520  itcovalsuc  48629  ackvalsuc1mpt  48640  eenglngeehlnmlem2  48700  itsclc0yqsol  48726  itscnhlc0xyqsol  48727  itsclc0xyqsolr  48731  itsclinecirc0in  48737  itscnhlinecirc02p  48747  inlinecirc02plem  48748