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 ( 𝐴 ∈ ( 0 ..^ 𝐵 ) ↔ ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) )

Proof

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