Metamath Proof Explorer

Theorem lbfzo0

Description: An integer is strictly greater than zero iff it is a member of NN . (Contributed by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion lbfzo0 ⊢ 0 ∈ 0 ..^ A ↔ A ∈ ℕ

Proof

Step Hyp Ref Expression
1 0z ⊢ 0 ∈ ℤ
2 3anass ⊢ 0 ∈ ℤ ∧ A ∈ ℤ ∧ 0 < A ↔ 0 ∈ ℤ ∧ A ∈ ℤ ∧ 0 < A
3 1 2 mpbiran ⊢ 0 ∈ ℤ ∧ A ∈ ℤ ∧ 0 < A ↔ A ∈ ℤ ∧ 0 < A
4 fzolb ⊢ 0 ∈ 0 ..^ A ↔ 0 ∈ ℤ ∧ A ∈ ℤ ∧ 0 < A
5 elnnz ⊢ A ∈ ℕ ↔ A ∈ ℤ ∧ 0 < A
6 3 4 5 3bitr4i ⊢ 0 ∈ 0 ..^ A ↔ A ∈ ℕ