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