Theorem gt0ne0d 11749

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

Syntax hints:   → wi 4   ≠ wne 2926   class class class wbr 5110  0cc0 11075   < clt 11215

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-addrcl 11136  ax-rnegex 11146  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220

This theorem is referenced by:  recextlem2  11816  prodgt0  12036  ltdiv1  12054  ltmuldiv  12063  ltrec  12072  lerec  12073  lediv12a  12083  recp1lt1  12088  ledivp1  12092  supmul1  12159  nnne0  12227  rpnnen1lem5  12947  ltexp2a  14138  leexp2  14143  leexp2a  14144  expnbnd  14204  expmulnbnd  14207  discr1  14211  eqsqrt2d  15342  bpoly4  16032  isabvd  20728  gzrngunit  21357  fvmptnn04ifa  22744  chfacffsupp  22750  chfacfscmul0  22752  chfacfpmmul0  22756  stdbdxmet  24410  evth  24865  itg2monolem3  25660  mvth  25904  dvlip  25905  dvcvx  25932  ftc1lem4  25953  dgradd2  26181  radcnvlem1  26329  pilem2  26369  coseq00topi  26418  tangtx  26421  tanabsge  26422  cos02pilt1  26442  tanord1  26453  logcnlem4  26561  cxplt  26610  atantan  26840  jensenlem2  26905  jensen  26906  lgamgulmlem2  26947  basellem3  27000  basellem4  27001  basellem8  27005  dchrmusumlema  27411  selberg3lem1  27475  abvcxp  27533  ostth2  27555  axsegconlem8  28858  axsegconlem9  28859  axsegconlem10  28860  axpaschlem  28874  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  iswwlksnx  29777  wspn0  29861  friendshipgt3  30334  his6  31035  eigrei  31770  sgnmul  32767  sgn0bi  32772  sgnmulsgp  32775  cycpmco2lem4  33093  cycpmco2lem5  33094  finexttrb  33667  fldext2rspun  33684  cos9thpiminplylem1  33779  cos9thpiminply  33785  xrge0iifcv  33931  signsvfpn  34583  tgoldbachgtde  34658  tgoldbachgtda  34659  lfuhgr2  35113  knoppndvlem18  36524  knoppndvlem19  36525  knoppndvlem21  36527  ftc1cnnclem  37692  areacirclem1  37709  3lexlogpow2ineq1  42053  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  aks4d1p1p6  42068  aks6d1c4  42119  aks6d1c2  42125  aks6d1c6lem4  42168  sn-nnne0  42455  sn-recgt0d  42472  mulgt0b2d  42473  mulltgt0d  42477  mullt0b2d  42479  3cubeslem2  42680  irrapxlem2  42818  irrapxlem5  42821  pellexlem2  42825  imo72b2  44168  binomcxplemnotnn0  44352  dvdivbd  45928  dvbdfbdioolem1  45933  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  stoweidlem7  46012  stoweidlem36  46041  wallispilem3  46072  wallispilem4  46073  wallispi2lem1  46076  wallispi2lem2  46077  stirlinglem3  46081  stirlinglem6  46084  stirlinglem7  46085  stirlinglem10  46088  stirlinglem11  46089  stirlinglem12  46090  stirlinglem13  46091  stirlinglem14  46092  stirlinglem15  46093  dirkerval2  46099  dirkeritg  46107  dirkercncflem2  46109  fourierdlem6  46118  fourierdlem7  46119  fourierdlem19  46131  fourierdlem26  46138  fourierdlem30  46142  fourierdlem48  46159  fourierdlem49  46160  fourierdlem51  46162  fourierdlem63  46174  fourierdlem64  46175  fourierdlem71  46182  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  sqwvfoura  46233  fourierswlem  46235  etransclem4  46243  etransclem31  46270  etransclem32  46271  iccpartgt  47432  upgrimpthslem2  47912  rege1logbrege0  48551  itcovalsuc  48660  ackvalsuc1mpt  48671  eenglngeehlnmlem2  48731  itsclc0yqsol  48757  itscnhlc0xyqsol  48758  itsclc0xyqsolr  48762  itsclinecirc0in  48768  itscnhlinecirc02p  48778  inlinecirc02plem  48779