Theorem gt0ne0d 11705

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

Syntax hints:   → wi 4   ≠ wne 2934   class class class wbr 5072  0cc0 11029   < clt 11170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-1cn 11087  ax-addrcl 11090  ax-rnegex 11100  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-po 5526  df-so 5527  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-ltxr 11175

This theorem is referenced by:  recextlem2  11772  prodgt0  11993  ltdiv1  12011  ltmuldiv  12020  ltrec  12029  lerec  12030  lediv12a  12040  recp1lt1  12045  ledivp1  12049  supmul1  12116  nnne0  12202  rpnnen1lem5  12922  ltexp2a  14119  leexp2  14124  leexp2a  14125  expnbnd  14185  expmulnbnd  14188  discr1  14192  eqsqrt2d  15322  bpoly4  16015  isabvd  20784  gzrngunit  21408  fvmptnn04ifa  22833  chfacffsupp  22839  chfacfscmul0  22841  chfacfpmmul0  22845  stdbdxmet  24498  evth  24944  itg2monolem3  25737  mvth  25977  dvlip  25978  dvcvx  26005  ftc1lem4  26024  dgradd2  26251  radcnvlem1  26396  pilem2  26435  coseq00topi  26484  tangtx  26487  tanabsge  26488  cos02pilt1  26508  tanord1  26519  logcnlem4  26627  cxplt  26676  atantan  26905  jensenlem2  26969  jensen  26970  lgamgulmlem2  27011  basellem3  27064  basellem4  27065  basellem8  27069  dchrmusumlema  27474  selberg3lem1  27538  abvcxp  27596  ostth2  27618  axsegconlem8  29011  axsegconlem9  29012  axsegconlem10  29013  axpaschlem  29027  axcontlem2  29052  axcontlem4  29054  axcontlem7  29057  iswwlksnx  29926  wspn0  30010  friendshipgt3  30486  his6  31188  eigrei  31923  sgnmul  32927  sgn0bi  32932  sgnmulsgp  32935  cycpmco2lem4  33210  cycpmco2lem5  33211  finexttrb  33849  fldext2rspun  33866  cos9thpiminplylem1  33966  cos9thpiminply  33972  xrge0iifcv  34118  signsvfpn  34769  tgoldbachgtde  34844  tgoldbachgtda  34845  lfuhgr2  35347  knoppndvlem18  36835  knoppndvlem19  36836  knoppndvlem21  36838  ftc1cnnclem  38058  areacirclem1  38075  3lexlogpow2ineq1  42543  3lexlogpow2ineq2  42544  3lexlogpow5ineq5  42545  aks4d1p1p6  42558  aks6d1c4  42609  aks6d1c2  42615  aks6d1c6lem4  42658  sn-nnne0  42950  sn-recgt0d  42967  mulgt0b2d  42968  mulltgt0d  42972  mullt0b2d  42974  3cubeslem2  43134  irrapxlem2  43268  irrapxlem5  43271  pellexlem2  43275  imo72b2  44616  binomcxplemnotnn0  44800  dvdivbd  46366  dvbdfbdioolem1  46371  ioodvbdlimc1lem1  46374  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  stoweidlem7  46450  stoweidlem36  46479  wallispilem3  46510  wallispilem4  46511  wallispi2lem1  46514  wallispi2lem2  46515  stirlinglem3  46519  stirlinglem6  46522  stirlinglem7  46523  stirlinglem10  46526  stirlinglem11  46527  stirlinglem12  46528  stirlinglem13  46529  stirlinglem14  46530  stirlinglem15  46531  dirkerval2  46537  dirkeritg  46545  dirkercncflem2  46547  fourierdlem6  46556  fourierdlem7  46557  fourierdlem19  46569  fourierdlem26  46576  fourierdlem30  46580  fourierdlem48  46597  fourierdlem49  46598  fourierdlem51  46600  fourierdlem63  46612  fourierdlem64  46613  fourierdlem71  46620  fourierdlem89  46638  fourierdlem90  46639  fourierdlem91  46640  fourierdlem103  46652  fourierdlem104  46653  fourierdlem112  46661  sqwvfoura  46671  fourierswlem  46673  etransclem4  46681  etransclem31  46708  etransclem32  46709  cjnpoly  47352  iccpartgt  47902  upgrimpthslem2  48399  rege1logbrege0  49049  itcovalsuc  49158  ackvalsuc1mpt  49169  eenglngeehlnmlem2  49229  itsclc0yqsol  49255  itscnhlc0xyqsol  49256  itsclc0xyqsolr  49260  itsclinecirc0in  49266  itscnhlinecirc02p  49276  inlinecirc02plem  49277