Theorem gt0ne0 11638

Description: Positive implies nonzero. (Contributed by NM, 3-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)

Assertion

Ref	Expression
gt0ne0	⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 ≠ 0)

Proof of Theorem gt0ne0

Step	Hyp	Ref	Expression
1		0red 11170	. 2 ⊢ (𝐴 ∈ ℝ → 0 ∈ ℝ)
2		ltne 11266	. 2 ⊢ ((0 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 ≠ 0)
3	1, 2	sylan 588	1 ⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2132   ≠ wne 2947   class class class wbr 5090  ℝcr 11058  0cc0 11059   < clt 11202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703  ax-resscn 11116  ax-1cn 11117  ax-addrcl 11120  ax-rnegex 11130  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-nel 3052  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-po 5544  df-so 5545  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514  df-er 8662  df-en 8913  df-dom 8914  df-sdom 8915  df-pnf 11204  df-mnf 11205  df-ltxr 11207

This theorem is referenced by:  recgt0  12023  lemul1  12029  lediv1  12043  gt0div  12044  ge0div  12045  mulge0b  12048  ltdivmul  12053  ledivmul  12054  lt2mul2div  12056  lemuldiv  12058  ltdiv2  12064  ltrec1  12065  lerec2  12066  ledivdiv  12067  lediv2  12068  ltdiv23  12069  lediv23  12070  lediv12a  12071  recreclt  12077  nnrecl  12465  elnnz  12564  recnz  12634  rpne0  12996  divelunit  13484  resqrex  15249  sqrtgt0  15257  argregt0  26641  argimgt0  26643  logneg2  26646  logcnlem3  26675  atanlogsublem  26946  leopmul  32272  cdj1i  32571  lediv2aALT  35965  nndivlub  36756  knoppndvlem15  36902  knoppndvlem17  36904  sineq0ALT  45450  eenglngeehlnmlem1  49297  eenglngeehlnmlem2  49298