Theorem gt0ne0d 11920

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

This proof depends on syntax axioms:   → wi 4   ≠ wne 2959   class class class wbr 5108  0cc0 11239   < clt 11382

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-resscn 11296  ax-1cn 11297  ax-addrcl 11300  ax-rnegex 11310  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-po 5566  df-so 5567  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-pnf 11384  df-mnf 11385  df-ltxr 11387

This theorem is used by:  recextlem2  11987  prodgt0  12204  ltdiv1  12221  ltmuldiv  12230  ltrec  12239  lerec  12240  lediv12a  12250  recp1lt1  12255  ledivp1  12259  supmul1  12326  nnne0  12412  rpnnen1lem5  13149  ltexp2a  14349  leexp2  14354  leexp2a  14355  expnbnd  14417  expmulnbnd  14420  discr1  14424  sgn0bi  15299  sgnmul  15303  eqsqrt2d  15580  bpoly4  16269  isabvd  21120  gzrngunit  21793  fvmptnn04ifa  23223  chfacffsupp  23229  chfacfscmul0  23231  chfacfpmmul0  23235  stdbdxmet  24889  evth  25335  itg2monolem3  26128  mvth  26367  dvlip  26368  dvcvx  26395  ftc1lem4  26414  dgradd2  26642  radcnvlem1  26797  pilem2  26836  coseq00topi  26888  tangtx  26891  tanabsge  26892  cos02pilt1  26911  tanord1  26922  logcnlem4  27030  cxplt  27079  atantan  27308  jensenlem2  27372  jensen  27373  lgamgulmlem2  27414  basellem3  27467  basellem4  27468  basellem8  27472  dchrmusumlema  27877  selberg3lem1  27941  abvcxp  27999  ostth2  28021  axsegconlem8  29559  axsegconlem9  29560  axsegconlem10  29561  axpaschlem  29575  axcontlem2  29600  axcontlem4  29602  axcontlem7  29605  lfuhgr2  29784  iswwlksnx  30486  wspn0  30570  friendshipgt3  31056  his6  31758  eigrei  32493  sgnmulsgp  33519  cycpmco2lem4  33789  cycpmco2lem5  33790  finexttrb  34408  fldext2rspun  34425  cos9thpiminplylem1  34525  cos9thpiminply  34531  xrge0iifcv  34677  signsvfpn  35325  tgoldbachgtde  35400  tgoldbachgtda  35401  knoppndvlem18  37610  knoppndvlem19  37611  knoppndvlem21  37613  ftc1cnnclem  38877  areacirclem1  38894  3lexlogpow2ineq1  43374  3lexlogpow2ineq2  43375  3lexlogpow5ineq5  43376  aks4d1p1p6  43389  aks6d1c4  43440  aks6d1c2  43446  aks6d1c6lem4  43489  sn-nnne0  43790  sn-recgt0d  43807  mulgt0b2d  43808  mulltgt0d  43812  mullt0b2d  43814  3cubeslem2  43961  irrapxlem2  44096  irrapxlem5  44099  pellexlem2  44103  imo72b2  45433  binomcxplemnotnn0  45601  dvdivbd  47206  dvbdfbdioolem1  47211  ioodvbdlimc1lem1  47214  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  stoweidlem7  47290  stoweidlem36  47319  wallispilem3  47350  wallispilem4  47351  wallispi2lem1  47354  wallispi2lem2  47355  stirlinglem3  47359  stirlinglem6  47362  stirlinglem7  47363  stirlinglem10  47366  stirlinglem11  47367  stirlinglem12  47368  stirlinglem13  47369  stirlinglem14  47370  stirlinglem15  47371  dirkerval2  47377  dirkeritg  47385  dirkercncflem2  47387  fourierdlem6  47396  fourierdlem7  47397  fourierdlem19  47409  fourierdlem26  47416  fourierdlem30  47420  fourierdlem48  47437  fourierdlem49  47438  fourierdlem51  47440  fourierdlem63  47452  fourierdlem64  47453  fourierdlem71  47460  fourierdlem89  47478  fourierdlem90  47479  fourierdlem91  47480  fourierdlem103  47492  fourierdlem104  47493  fourierdlem112  47501  sqwvfoura  47511  fourierswlem  47513  etransclem4  47521  etransclem31  47548  etransclem32  47549  cjnpoly  48212  iccpartgt  48782  upgrimpthslem2  49279  rege1logbrege0  50001  itcovalsuc  50110  ackvalsuc1mpt  50121  eenglngeehlnmlem2  50182  itsclc0yqsol  50207  itscnhlc0xyqsol  50208  itsclc0xyqsolr  50212  itsclinecirc0in  50218  itscnhlinecirc02p  50228  inlinecirc02plem  50229