Theorem fzoss2

Description: Subset relationship for half-open sequences of integers. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 29-Sep-2015)

	Ref	Expression
Assertion	fzoss2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑀 ..^ 𝐾 ) ⊆ ( 𝑀 ..^ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		eluzel2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝐾 ∈ ℤ )
2		peano2zm	⊢ ( 𝐾 ∈ ℤ → ( 𝐾 − 1 ) ∈ ℤ )
3	1 2	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝐾 − 1 ) ∈ ℤ )
4		1zzd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 1 ∈ ℤ )
5		id	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
6	1	zcnd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝐾 ∈ ℂ )
7		ax-1cn	⊢ 1 ∈ ℂ
8		npcan	⊢ ( ( 𝐾 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
9	6 7 8	sylancl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
10	9	fveq2d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( ℤ≥ ‘ ( ( 𝐾 − 1 ) + 1 ) ) = ( ℤ≥ ‘ 𝐾 ) )
11	5 10	eleqtrrd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝐾 − 1 ) + 1 ) ) )
12		eluzsub	⊢ ( ( ( 𝐾 − 1 ) ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝐾 − 1 ) + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝐾 − 1 ) ) )
13	3 4 11 12	syl3anc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝐾 − 1 ) ) )
14		fzss2	⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝐾 − 1 ) ) → ( 𝑀 ... ( 𝐾 − 1 ) ) ⊆ ( 𝑀 ... ( 𝑁 − 1 ) ) )
15	13 14	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑀 ... ( 𝐾 − 1 ) ) ⊆ ( 𝑀 ... ( 𝑁 − 1 ) ) )
16		fzoval	⊢ ( 𝐾 ∈ ℤ → ( 𝑀 ..^ 𝐾 ) = ( 𝑀 ... ( 𝐾 − 1 ) ) )
17	1 16	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑀 ..^ 𝐾 ) = ( 𝑀 ... ( 𝐾 − 1 ) ) )
18		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝑁 ∈ ℤ )
19		fzoval	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
20	18 19	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
21	15 17 20	3sstr4d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑀 ..^ 𝐾 ) ⊆ ( 𝑀 ..^ 𝑁 ) )