Metamath Proof Explorer


Theorem fzssfzo

Description: Condition for an integer interval to be a subset of a half-open integer interval. (Contributed by Thierry Arnoux, 8-Oct-2018)

Ref Expression
Assertion fzssfzo ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ... 𝐾 ) ⊆ ( 𝑀 ..^ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 elfzoel2 ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
2 fzoval ( 𝑁 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
3 1 2 syl ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
4 3 eleq2d ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) )
5 4 ibi ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) )
6 elfzuz3 ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ𝐾 ) )
7 fzss2 ( ( 𝑁 − 1 ) ∈ ( ℤ𝐾 ) → ( 𝑀 ... 𝐾 ) ⊆ ( 𝑀 ... ( 𝑁 − 1 ) ) )
8 5 6 7 3syl ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ... 𝐾 ) ⊆ ( 𝑀 ... ( 𝑁 − 1 ) ) )
9 8 3 sseqtrrd ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ... 𝐾 ) ⊆ ( 𝑀 ..^ 𝑁 ) )