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	$⊢ N \in ℤ_{\geq K} \to (M ..^K) \subseteq (M ..^N)$

Proof

Step	Hyp	Ref	Expression
1		eluzel2	$⊢ N \in ℤ_{\geq K} \to K \in ℤ$
2		peano2zm	$⊢ K \in ℤ \to K - 1 \in ℤ$
3	1 2	syl	$⊢ N \in ℤ_{\geq K} \to K - 1 \in ℤ$
4		1zzd	$⊢ N \in ℤ_{\geq K} \to 1 \in ℤ$
5		id	$⊢ N \in ℤ_{\geq K} \to N \in ℤ_{\geq K}$
6	1	zcnd	$⊢ N \in ℤ_{\geq K} \to K \in ℂ$
7		ax-1cn	$⊢ 1 \in ℂ$
8		npcan	$⊢ (K \in ℂ \land 1 \in ℂ) \to K - 1 + 1 = K$
9	6 7 8	sylancl	$⊢ N \in ℤ_{\geq K} \to K - 1 + 1 = K$
10	9	fveq2d	$⊢ N \in ℤ_{\geq K} \to ℤ_{\geq (K - 1 + 1)} = ℤ_{\geq K}$
11	5 10	eleqtrrd	$⊢ N \in ℤ_{\geq K} \to N \in ℤ_{\geq (K - 1 + 1)}$
12		eluzsub	$⊢ (K - 1 \in ℤ \land 1 \in ℤ \land N \in ℤ_{\geq (K - 1 + 1)}) \to N - 1 \in ℤ_{\geq (K - 1)}$
13	3 4 11 12	syl3anc	$⊢ N \in ℤ_{\geq K} \to N - 1 \in ℤ_{\geq (K - 1)}$
14		fzss2	$⊢ N - 1 \in ℤ_{\geq (K - 1)} \to (M \dots K - 1) \subseteq (M \dots N - 1)$
15	13 14	syl	$⊢ N \in ℤ_{\geq K} \to (M \dots K - 1) \subseteq (M \dots N - 1)$
16		fzoval	$⊢ K \in ℤ \to (M ..^K) = (M \dots K - 1)$
17	1 16	syl	$⊢ N \in ℤ_{\geq K} \to (M ..^K) = (M \dots K - 1)$
18		eluzelz	$⊢ N \in ℤ_{\geq K} \to N \in ℤ$
19		fzoval	$⊢ N \in ℤ \to (M ..^N) = (M \dots N - 1)$
20	18 19	syl	$⊢ N \in ℤ_{\geq K} \to (M ..^N) = (M \dots N - 1)$
21	15 17 20	3sstr4d	$⊢ N \in ℤ_{\geq K} \to (M ..^K) \subseteq (M ..^N)$

Metamath Proof Explorer

Theorem fzoss2

Proof