Theorem gt0ne0d 11802

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

This proof depends on syntax axioms:   → wi 4   ≠ wne 2955   class class class wbr 5103  0cc0 11124   < clt 11267

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-resscn 11181  ax-1cn 11182  ax-addrcl 11185  ax-rnegex 11195  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199

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 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-ltxr 11272

This theorem is used by:  recextlem2  11869  prodgt0  12086  ltdiv1  12103  ltmuldiv  12112  ltrec  12121  lerec  12122  lediv12a  12132  recp1lt1  12137  ledivp1  12141  supmul1  12208  nnne0  12294  rpnnen1lem5  13031  ltexp2a  14230  leexp2  14235  leexp2a  14236  expnbnd  14296  expmulnbnd  14299  discr1  14303  sgn0bi  15176  sgnmul  15180  eqsqrt2d  15456  bpoly4  16145  isabvd  20978  gzrngunit  21646  fvmptnn04ifa  23075  chfacffsupp  23081  chfacfscmul0  23083  chfacfpmmul0  23087  stdbdxmet  24741  evth  25187  itg2monolem3  25980  mvth  26219  dvlip  26220  dvcvx  26247  ftc1lem4  26266  dgradd2  26494  radcnvlem1  26649  pilem2  26688  coseq00topi  26740  tangtx  26743  tanabsge  26744  cos02pilt1  26763  tanord1  26774  logcnlem4  26882  cxplt  26931  atantan  27160  jensenlem2  27224  jensen  27225  lgamgulmlem2  27266  basellem3  27319  basellem4  27320  basellem8  27324  dchrmusumlema  27729  selberg3lem1  27793  abvcxp  27851  ostth2  27873  axsegconlem8  29381  axsegconlem9  29382  axsegconlem10  29383  axpaschlem  29397  axcontlem2  29422  axcontlem4  29424  axcontlem7  29427  lfuhgr2  29606  iswwlksnx  30308  wspn0  30392  friendshipgt3  30878  his6  31580  eigrei  32315  sgnmulsgp  33302  cycpmco2lem4  33569  cycpmco2lem5  33570  finexttrb  34175  fldext2rspun  34192  cos9thpiminplylem1  34292  cos9thpiminply  34298  xrge0iifcv  34444  signsvfpn  35093  tgoldbachgtde  35168  tgoldbachgtda  35169  knoppndvlem18  37226  knoppndvlem19  37227  knoppndvlem21  37229  ftc1cnnclem  38440  areacirclem1  38457  3lexlogpow2ineq1  42924  3lexlogpow2ineq2  42925  3lexlogpow5ineq5  42926  aks4d1p1p6  42939  aks6d1c4  42990  aks6d1c2  42996  aks6d1c6lem4  43039  sn-nnne0  43348  sn-recgt0d  43365  mulgt0b2d  43366  mulltgt0d  43370  mullt0b2d  43372  3cubeslem2  43530  irrapxlem2  43664  irrapxlem5  43667  pellexlem2  43671  imo72b2  45012  binomcxplemnotnn0  45180  dvdivbd  46751  dvbdfbdioolem1  46756  ioodvbdlimc1lem1  46759  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  stoweidlem7  46835  stoweidlem36  46864  wallispilem3  46895  wallispilem4  46896  wallispi2lem1  46899  wallispi2lem2  46900  stirlinglem3  46904  stirlinglem6  46907  stirlinglem7  46908  stirlinglem10  46911  stirlinglem11  46912  stirlinglem12  46913  stirlinglem13  46914  stirlinglem14  46915  stirlinglem15  46916  dirkerval2  46922  dirkeritg  46930  dirkercncflem2  46932  fourierdlem6  46941  fourierdlem7  46942  fourierdlem19  46954  fourierdlem26  46961  fourierdlem30  46965  fourierdlem48  46982  fourierdlem49  46983  fourierdlem51  46985  fourierdlem63  46997  fourierdlem64  46998  fourierdlem71  47005  fourierdlem89  47023  fourierdlem90  47024  fourierdlem91  47025  fourierdlem103  47037  fourierdlem104  47038  fourierdlem112  47046  sqwvfoura  47056  fourierswlem  47058  etransclem4  47066  etransclem31  47093  etransclem32  47094  cjnpoly  47757  iccpartgt  48327  upgrimpthslem2  48824  rege1logbrege0  49488  itcovalsuc  49597  ackvalsuc1mpt  49608  eenglngeehlnmlem2  49668  itsclc0yqsol  49694  itscnhlc0xyqsol  49695  itsclc0xyqsolr  49699  itsclinecirc0in  49705  itscnhlinecirc02p  49715  inlinecirc02plem  49716