Metamath Proof Explorer


Theorem elfzouz2

Description: The upper bound of a half-open range is greater than or equal to an element of the range. (Contributed by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion elfzouz2 ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ( ℤ𝐾 ) )

Proof

Step Hyp Ref Expression
1 elfzoelz ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 ∈ ℤ )
2 elfzoel2 ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
3 elfzolt2 ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 < 𝑁 )
4 zre ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
5 zre ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
6 ltle ( ( 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐾 < 𝑁𝐾𝑁 ) )
7 4 5 6 syl2an ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 < 𝑁𝐾𝑁 ) )
8 1 2 7 syl2anc ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐾 < 𝑁𝐾𝑁 ) )
9 3 8 mpd ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾𝑁 )
10 eluz2 ( 𝑁 ∈ ( ℤ𝐾 ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾𝑁 ) )
11 1 2 9 10 syl3anbrc ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ( ℤ𝐾 ) )