Metamath Proof Explorer

Theorem seqcl

Description: Closure properties of the recursive sequence builder. (Contributed by Mario Carneiro, 2-Jul-2013) (Revised by Mario Carneiro, 27-May-2014)

		Ref	Expression
	Hypotheses	seqcl.1	$⊢ φ \to N \in ℤ_{\geq M}$
		seqcl.2	$⊢ (φ \land x \in (M \dots N)) \to F (x) \in S$
		seqcl.3	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
	Assertion	seqcl	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) \in S$

Proof

Step	Hyp	Ref	Expression
1		seqcl.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		seqcl.2	$⊢ (φ \land x \in (M \dots N)) \to F (x) \in S$
3		seqcl.3	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
4		fveq2	$⊢ x = M \to F (x) = F (M)$
5	4	eleq1d	$⊢ x = M \to (F (x) \in S \leftrightarrow F (M) \in S)$
6	2	ralrimiva	$⊢ φ \to \forall x \in (M \dots N) F (x) \in S$
7		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
8	1 7	syl	$⊢ φ \to M \in (M \dots N)$
9	5 6 8	rspcdva	$⊢ φ \to F (M) \in S$
10		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
11	1 10	syl	$⊢ φ \to M \in ℤ$
12		fzp1ss	$⊢ M \in ℤ \to (M + 1 \dots N) \subseteq (M \dots N)$
13	11 12	syl	$⊢ φ \to (M + 1 \dots N) \subseteq (M \dots N)$
14	13	sselda	$⊢ (φ \land x \in (M + 1 \dots N)) \to x \in (M \dots N)$
15	14 2	syldan	$⊢ (φ \land x \in (M + 1 \dots N)) \to F (x) \in S$
16	9 3 1 15	seqcl2	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) \in S$