Theorem nn0p1elfzo

Description: A nonnegative integer increased by 1 which is less than or equal to another integer is an element of a half-open range of integers. (Contributed by AV, 27-Feb-2021)

	Ref	Expression
Assertion	nn0p1elfzo	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) → 𝐾 ∈ ( 0 ..^ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0ltp1le	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 < 𝑁 ↔ ( 𝐾 + 1 ) ≤ 𝑁 ) )
2	1	biimp3ar	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) → 𝐾 < 𝑁 )
3		simpl1	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) ∧ 𝐾 < 𝑁 ) → 𝐾 ∈ ℕ0 )
4		simpr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
5	4	adantr	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐾 < 𝑁 ) → 𝑁 ∈ ℕ0 )
6		nn0ge0	⊢ ( 𝐾 ∈ ℕ0 → 0 ≤ 𝐾 )
7	6	adantr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 0 ≤ 𝐾 )
8		0re	⊢ 0 ∈ ℝ
9		nn0re	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
10		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
11		lelttr	⊢ ( ( 0 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) → 0 < 𝑁 ) )
12	8 9 10 11	mp3an3an	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) → 0 < 𝑁 ) )
13	7 12	mpand	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 < 𝑁 → 0 < 𝑁 ) )
14	13	imp	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐾 < 𝑁 ) → 0 < 𝑁 )
15		elnnnn0b	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 0 < 𝑁 ) )
16	5 14 15	sylanbrc	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐾 < 𝑁 ) → 𝑁 ∈ ℕ )
17	16	3adantl3	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) ∧ 𝐾 < 𝑁 ) → 𝑁 ∈ ℕ )
18		simpr	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) ∧ 𝐾 < 𝑁 ) → 𝐾 < 𝑁 )
19	3 17 18	3jca	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) ∧ 𝐾 < 𝑁 ) → ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) )
20	2 19	mpdan	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) → ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) )
21		elfzo0	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) )
22	20 21	sylibr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) → 𝐾 ∈ ( 0 ..^ 𝑁 ) )