This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ne0gt0

Description: A nonzero nonnegative number is positive. (Contributed by NM, 20-Nov-2007)

Ref Expression
Assertion ne0gt0 ⊢ A ∈ ℝ ∧ 0 ≤ A → A ≠ 0 ↔ 0 < A

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 lttri2 ⊢ A ∈ ℝ ∧ 0 ∈ ℝ → A ≠ 0 ↔ A < 0 ∨ 0 < A
3 1 2 mpan2 ⊢ A ∈ ℝ → A ≠ 0 ↔ A < 0 ∨ 0 < A
4 3 adantr ⊢ A ∈ ℝ ∧ 0 ≤ A → A ≠ 0 ↔ A < 0 ∨ 0 < A
5 lenlt ⊢ 0 ∈ ℝ ∧ A ∈ ℝ → 0 ≤ A ↔ ¬ A < 0
6 1 5 mpan ⊢ A ∈ ℝ → 0 ≤ A ↔ ¬ A < 0
7 6 biimpa ⊢ A ∈ ℝ ∧ 0 ≤ A → ¬ A < 0
8 biorf ⊢ ¬ A < 0 → 0 < A ↔ A < 0 ∨ 0 < A
9 7 8 syl ⊢ A ∈ ℝ ∧ 0 ≤ A → 0 < A ↔ A < 0 ∨ 0 < A
10 4 9 bitr4d ⊢ A ∈ ℝ ∧ 0 ≤ A → A ≠ 0 ↔ 0 < A