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

Metamath Proof Explorer

Theorem elfzo0

Description: Membership in a half-open integer range based at 0. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion elfzo0 ⊢ A ∈ 0 ..^ B ↔ A ∈ ℕ 0 ∧ B ∈ ℕ ∧ A < B

Proof

Step Hyp Ref Expression
1 elfzouz ⊢ A ∈ 0 ..^ B → A ∈ ℤ ≥ 0
2 elnn0uz ⊢ A ∈ ℕ 0 ↔ A ∈ ℤ ≥ 0
3 1 2 sylibr ⊢ A ∈ 0 ..^ B → A ∈ ℕ 0
4 elfzolt3b ⊢ A ∈ 0 ..^ B → 0 ∈ 0 ..^ B
5 lbfzo0 ⊢ 0 ∈ 0 ..^ B ↔ B ∈ ℕ
6 4 5 sylib ⊢ A ∈ 0 ..^ B → B ∈ ℕ
7 elfzolt2 ⊢ A ∈ 0 ..^ B → A < B
8 3 6 7 3jca ⊢ A ∈ 0 ..^ B → A ∈ ℕ 0 ∧ B ∈ ℕ ∧ A < B
9 simp1 ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ ∧ A < B → A ∈ ℕ 0
10 9 2 sylib ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ ∧ A < B → A ∈ ℤ ≥ 0
11 nnz ⊢ B ∈ ℕ → B ∈ ℤ
12 11 3ad2ant2 ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ ∧ A < B → B ∈ ℤ
13 simp3 ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ ∧ A < B → A < B
14 elfzo2 ⊢ A ∈ 0 ..^ B ↔ A ∈ ℤ ≥ 0 ∧ B ∈ ℤ ∧ A < B
15 10 12 13 14 syl3anbrc ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ ∧ A < B → A ∈ 0 ..^ B
16 8 15 impbii ⊢ A ∈ 0 ..^ B ↔ A ∈ ℕ 0 ∧ B ∈ ℕ ∧ A < B