Theorem elfz2nn0

Description: Membership in a finite set of sequential nonnegative integers. (Contributed by NM, 16-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Assertion	elfz2nn0	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elnn0uz	⊢ ( 𝐾 ∈ ℕ0 ↔ 𝐾 ∈ ( ℤ≥ ‘ 0 ) )
2	1	anbi1i	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) )
3		eluznn0	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑁 ∈ ℕ0 )
4		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝐾 ≤ 𝑁 )
5	4	adantl	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐾 ≤ 𝑁 )
6	3 5	jca	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) )
7		nn0z	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℤ )
8		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
9		eluz	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ↔ 𝐾 ≤ 𝑁 ) )
10	7 8 9	syl2an	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ↔ 𝐾 ≤ 𝑁 ) )
11	10	biimprd	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 ≤ 𝑁 → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) )
12	11	impr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
13	6 12	impbida	⊢ ( 𝐾 ∈ ℕ0 → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ↔ ( 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) ) )
14	13	pm5.32i	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ↔ ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) ) )
15	2 14	bitr3i	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ↔ ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) ) )
16		elfzuzb	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) )
17		3anass	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) ↔ ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) ) )
18	15 16 17	3bitr4i	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) )