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 ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵 ) )