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