Theorem elfz2z

Description: Membership of an integer in a finite set of sequential integers starting at 0. (Contributed by Alexander van der Vekens, 25-May-2018)

	Ref	Expression
Assertion	elfz2z	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfz2nn0	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) )
2		df-3an	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) ↔ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑁 ) )
3	1 2	bitri	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑁 ) )
4		nn0ge0	⊢ ( 𝐾 ∈ ℕ0 → 0 ≤ 𝐾 )
5	4	adantr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 0 ≤ 𝐾 )
6		simpll	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ≤ 𝑁 ) → 𝐾 ∈ ℤ )
7	6	anim1i	⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ≤ 𝑁 ) ∧ 0 ≤ 𝐾 ) → ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) )
8		elnn0z	⊢ ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) )
9	7 8	sylibr	⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ≤ 𝑁 ) ∧ 0 ≤ 𝐾 ) → 𝐾 ∈ ℕ0 )
10		0red	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 0 ∈ ℝ )
11		zre	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
12	11	adantr	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ℝ )
13		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
14	13	adantl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℝ )
15		letr	⊢ ( ( 0 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) → 0 ≤ 𝑁 ) )
16	10 12 14 15	syl3anc	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) → 0 ≤ 𝑁 ) )
17		elnn0z	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) )
18	17	simplbi2	⊢ ( 𝑁 ∈ ℤ → ( 0 ≤ 𝑁 → 𝑁 ∈ ℕ0 ) )
19	18	adantl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 ≤ 𝑁 → 𝑁 ∈ ℕ0 ) )
20	16 19	syld	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) → 𝑁 ∈ ℕ0 ) )
21	20	expcomd	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ≤ 𝑁 → ( 0 ≤ 𝐾 → 𝑁 ∈ ℕ0 ) ) )
22	21	imp31	⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ≤ 𝑁 ) ∧ 0 ≤ 𝐾 ) → 𝑁 ∈ ℕ0 )
23	9 22	jca	⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ≤ 𝑁 ) ∧ 0 ≤ 𝐾 ) → ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) )
24	23	ex	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ≤ 𝑁 ) → ( 0 ≤ 𝐾 → ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) )
25	5 24	impbid2	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ≤ 𝑁 ) → ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ↔ 0 ≤ 𝐾 ) )
26	25	ex	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ≤ 𝑁 → ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ↔ 0 ≤ 𝐾 ) ) )
27	26	pm5.32rd	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑁 ) ↔ ( 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
28	3 27	bitrid	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )