Theorem elfzop1le2

Description: A member in a half-open integer interval plus 1 is less than or equal to the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	elfzop1le2	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐾 + 1 ) ≤ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		elfzolt2	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 < 𝑁 )
2		elfzoelz	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 ∈ ℤ )
3		elfzoel2	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
4		zltp1le	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 < 𝑁 ↔ ( 𝐾 + 1 ) ≤ 𝑁 ) )
5	2 3 4	syl2anc	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐾 < 𝑁 ↔ ( 𝐾 + 1 ) ≤ 𝑁 ) )
6	1 5	mpbid	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐾 + 1 ) ≤ 𝑁 )