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

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

Proof

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