Metamath Proof Explorer

Theorem fzoss1

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

Proof

Step	Hyp	Ref	Expression
1		sseq1	$⊢ (K ..^N) = \emptyset \to ((K ..^N) \subseteq (M ..^N) \leftrightarrow \emptyset \subseteq (M ..^N))$
2		fzon0	$⊢ (K ..^N) \neq \emptyset \leftrightarrow K \in (K ..^N)$
3		elfzoel2	$⊢ K \in (K ..^N) \to N \in ℤ$
4	2 3	sylbi	$⊢ (K ..^N) \neq \emptyset \to N \in ℤ$
5		fzss1	$⊢ K \in ℤ_{\geq M} \to (K \dots N - 1) \subseteq (M \dots N - 1)$
6	5	adantr	$⊢ (K \in ℤ_{\geq M} \land N \in ℤ) \to (K \dots N - 1) \subseteq (M \dots N - 1)$
7		fzoval	$⊢ N \in ℤ \to (K ..^N) = (K \dots N - 1)$
8	7	adantl	$⊢ (K \in ℤ_{\geq M} \land N \in ℤ) \to (K ..^N) = (K \dots N - 1)$
9		fzoval	$⊢ N \in ℤ \to (M ..^N) = (M \dots N - 1)$
10	9	adantl	$⊢ (K \in ℤ_{\geq M} \land N \in ℤ) \to (M ..^N) = (M \dots N - 1)$
11	6 8 10	3sstr4d	$⊢ (K \in ℤ_{\geq M} \land N \in ℤ) \to (K ..^N) \subseteq (M ..^N)$
12	4 11	sylan2	$⊢ (K \in ℤ_{\geq M} \land (K ..^N) \neq \emptyset) \to (K ..^N) \subseteq (M ..^N)$
13		0ss	$⊢ \emptyset \subseteq (M ..^N)$
14	13	a1i	$⊢ K \in ℤ_{\geq M} \to \emptyset \subseteq (M ..^N)$
15	1 12 14	pm2.61ne	$⊢ K \in ℤ_{\geq M} \to (K ..^N) \subseteq (M ..^N)$