Metamath Proof Explorer

Theorem elfzo0z

Description: Membership in a half-open range of nonnegative integers, generalization of elfzo0 requiring the upper bound to be an integer only. (Contributed by Alexander van der Vekens, 23-Sep-2018)

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

Proof

Step Hyp Ref Expression
1 elfzo0 ⊢ A ∈ 0 ..^ B ↔ A ∈ ℕ 0 ∧ B ∈ ℕ ∧ A < B
2 nnz ⊢ B ∈ ℕ → B ∈ ℤ
3 2 3anim2i ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ ∧ A < B → A ∈ ℕ 0 ∧ B ∈ ℤ ∧ A < B
4 simp1 ⊢ A ∈ ℕ 0 ∧ B ∈ ℤ ∧ A < B → A ∈ ℕ 0
5 elnn0z ⊢ A ∈ ℕ 0 ↔ A ∈ ℤ ∧ 0 ≤ A
6 0red ⊢ A ∈ ℤ ∧ B ∈ ℤ → 0 ∈ ℝ
7 zre ⊢ A ∈ ℤ → A ∈ ℝ
8 7 adantr ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ∈ ℝ
9 zre ⊢ B ∈ ℤ → B ∈ ℝ
10 9 adantl ⊢ A ∈ ℤ ∧ B ∈ ℤ → B ∈ ℝ
11 lelttr ⊢ 0 ∈ ℝ ∧ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ A ∧ A < B → 0 < B
12 6 8 10 11 syl3anc ⊢ A ∈ ℤ ∧ B ∈ ℤ → 0 ≤ A ∧ A < B → 0 < B
13 elnnz ⊢ B ∈ ℕ ↔ B ∈ ℤ ∧ 0 < B
14 13 simplbi2 ⊢ B ∈ ℤ → 0 < B → B ∈ ℕ
15 14 adantl ⊢ A ∈ ℤ ∧ B ∈ ℤ → 0 < B → B ∈ ℕ
16 12 15 syld ⊢ A ∈ ℤ ∧ B ∈ ℤ → 0 ≤ A ∧ A < B → B ∈ ℕ
17 16 expd ⊢ A ∈ ℤ ∧ B ∈ ℤ → 0 ≤ A → A < B → B ∈ ℕ
18 17 impancom ⊢ A ∈ ℤ ∧ 0 ≤ A → B ∈ ℤ → A < B → B ∈ ℕ
19 5 18 sylbi ⊢ A ∈ ℕ 0 → B ∈ ℤ → A < B → B ∈ ℕ
20 19 3imp ⊢ A ∈ ℕ 0 ∧ B ∈ ℤ ∧ A < B → B ∈ ℕ
21 simp3 ⊢ A ∈ ℕ 0 ∧ B ∈ ℤ ∧ A < B → A < B
22 4 20 21 3jca ⊢ A ∈ ℕ 0 ∧ B ∈ ℤ ∧ A < B → A ∈ ℕ 0 ∧ B ∈ ℕ ∧ A < B
23 3 22 impbii ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ ∧ A < B ↔ A ∈ ℕ 0 ∧ B ∈ ℤ ∧ A < B
24 1 23 bitri ⊢ A ∈ 0 ..^ B ↔ A ∈ ℕ 0 ∧ B ∈ ℤ ∧ A < B