seqcl2

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	seqcl2.1	$⊢ φ \to F (M) \in C$
	seqcl2.2	$⊢ (φ \land (x \in C \land y \in D)) \to x \underset{˙}{+} y \in C$
	seqcl2.3	$⊢ φ \to N \in ℤ_{\geq M}$
	seqcl2.4	$⊢ (φ \land x \in (M + 1 \dots N)) \to F (x) \in D$
Assertion	seqcl2	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) \in C$

Proof

Step	Hyp	Ref	Expression
1		seqcl2.1	$⊢ φ \to F (M) \in C$
2		seqcl2.2	$⊢ (φ \land (x \in C \land y \in D)) \to x \underset{˙}{+} y \in C$
3		seqcl2.3	$⊢ φ \to N \in ℤ_{\geq M}$
4		seqcl2.4	$⊢ (φ \land x \in (M + 1 \dots N)) \to F (x) \in D$
5		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
6	3 5	syl	$⊢ φ \to N \in (M \dots N)$
7		eleq1	$⊢ x = M \to (x \in (M \dots N) \leftrightarrow M \in (M \dots N))$
8		fveq2	$⊢ x = M \to seq M (\underset{˙}{+}, F) (x) = seq M (\underset{˙}{+}, F) (M)$
9	8	eleq1d	$⊢ x = M \to (seq M (\underset{˙}{+}, F) (x) \in C \leftrightarrow seq M (\underset{˙}{+}, F) (M) \in C)$
10	7 9	imbi12d	$⊢ x = M \to ((x \in (M \dots N) \to seq M (\underset{˙}{+}, F) (x) \in C) \leftrightarrow (M \in (M \dots N) \to seq M (\underset{˙}{+}, F) (M) \in C))$
11	10	imbi2d	$⊢ x = M \to ((φ \to (x \in (M \dots N) \to seq M (\underset{˙}{+}, F) (x) \in C)) \leftrightarrow (φ \to (M \in (M \dots N) \to seq M (\underset{˙}{+}, F) (M) \in C)))$
12		eleq1	$⊢ x = n \to (x \in (M \dots N) \leftrightarrow n \in (M \dots N))$
13		fveq2	$⊢ x = n \to seq M (\underset{˙}{+}, F) (x) = seq M (\underset{˙}{+}, F) (n)$
14	13	eleq1d	$⊢ x = n \to (seq M (\underset{˙}{+}, F) (x) \in C \leftrightarrow seq M (\underset{˙}{+}, F) (n) \in C)$
15	12 14	imbi12d	$⊢ x = n \to ((x \in (M \dots N) \to seq M (\underset{˙}{+}, F) (x) \in C) \leftrightarrow (n \in (M \dots N) \to seq M (\underset{˙}{+}, F) (n) \in C))$
16	15	imbi2d	$⊢ x = n \to ((φ \to (x \in (M \dots N) \to seq M (\underset{˙}{+}, F) (x) \in C)) \leftrightarrow (φ \to (n \in (M \dots N) \to seq M (\underset{˙}{+}, F) (n) \in C)))$
17		eleq1	$⊢ x = n + 1 \to (x \in (M \dots N) \leftrightarrow n + 1 \in (M \dots N))$
18		fveq2	$⊢ x = n + 1 \to seq M (\underset{˙}{+}, F) (x) = seq M (\underset{˙}{+}, F) (n + 1)$
19	18	eleq1d	$⊢ x = n + 1 \to (seq M (\underset{˙}{+}, F) (x) \in C \leftrightarrow seq M (\underset{˙}{+}, F) (n + 1) \in C)$
20	17 19	imbi12d	$⊢ x = n + 1 \to ((x \in (M \dots N) \to seq M (\underset{˙}{+}, F) (x) \in C) \leftrightarrow (n + 1 \in (M \dots N) \to seq M (\underset{˙}{+}, F) (n + 1) \in C))$
21	20	imbi2d	$⊢ x = n + 1 \to ((φ \to (x \in (M \dots N) \to seq M (\underset{˙}{+}, F) (x) \in C)) \leftrightarrow (φ \to (n + 1 \in (M \dots N) \to seq M (\underset{˙}{+}, F) (n + 1) \in C)))$
22		eleq1	$⊢ x = N \to (x \in (M \dots N) \leftrightarrow N \in (M \dots N))$
23		fveq2	$⊢ x = N \to seq M (\underset{˙}{+}, F) (x) = seq M (\underset{˙}{+}, F) (N)$
24	23	eleq1d	$⊢ x = N \to (seq M (\underset{˙}{+}, F) (x) \in C \leftrightarrow seq M (\underset{˙}{+}, F) (N) \in C)$
25	22 24	imbi12d	$⊢ x = N \to ((x \in (M \dots N) \to seq M (\underset{˙}{+}, F) (x) \in C) \leftrightarrow (N \in (M \dots N) \to seq M (\underset{˙}{+}, F) (N) \in C))$
26	25	imbi2d	$⊢ x = N \to ((φ \to (x \in (M \dots N) \to seq M (\underset{˙}{+}, F) (x) \in C)) \leftrightarrow (φ \to (N \in (M \dots N) \to seq M (\underset{˙}{+}, F) (N) \in C)))$
27		seq1	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, F) (M) = F (M)$
28	27	eleq1d	$⊢ M \in ℤ \to (seq M (\underset{˙}{+}, F) (M) \in C \leftrightarrow F (M) \in C)$
29	1 28	syl5ibr	$⊢ M \in ℤ \to (φ \to seq M (\underset{˙}{+}, F) (M) \in C)$
30	29	a1dd	$⊢ M \in ℤ \to (φ \to (M \in (M \dots N) \to seq M (\underset{˙}{+}, F) (M) \in C))$
31		peano2fzr	$⊢ (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to n \in (M \dots N)$
32	31	adantl	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n \in (M \dots N)$
33	32	expr	$⊢ (φ \land n \in ℤ_{\geq M}) \to (n + 1 \in (M \dots N) \to n \in (M \dots N))$
34	33	imim1d	$⊢ (φ \land n \in ℤ_{\geq M}) \to ((n \in (M \dots N) \to seq M (\underset{˙}{+}, F) (n) \in C) \to (n + 1 \in (M \dots N) \to seq M (\underset{˙}{+}, F) (n) \in C))$
35		fveq2	$⊢ x = n + 1 \to F (x) = F (n + 1)$
36	35	eleq1d	$⊢ x = n + 1 \to (F (x) \in D \leftrightarrow F (n + 1) \in D)$
37	4	ralrimiva	$⊢ φ \to \forall x \in (M + 1 \dots N) F (x) \in D$
38	37	adantr	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to \forall x \in (M + 1 \dots N) F (x) \in D$
39		eluzp1p1	$⊢ n \in ℤ_{\geq M} \to n + 1 \in ℤ_{\geq (M + 1)}$
40	39	ad2antrl	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n + 1 \in ℤ_{\geq (M + 1)}$
41		elfzuz3	$⊢ n + 1 \in (M \dots N) \to N \in ℤ_{\geq (n + 1)}$
42	41	ad2antll	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to N \in ℤ_{\geq (n + 1)}$
43		elfzuzb	$⊢ n + 1 \in (M + 1 \dots N) \leftrightarrow (n + 1 \in ℤ_{\geq (M + 1)} \land N \in ℤ_{\geq (n + 1)})$
44	40 42 43	sylanbrc	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n + 1 \in (M + 1 \dots N)$
45	36 38 44	rspcdva	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to F (n + 1) \in D$
46	2	caovclg	$⊢ (φ \land (seq M (\underset{˙}{+}, F) (n) \in C \land F (n + 1) \in D)) \to seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1) \in C$
47	46	ex	$⊢ φ \to ((seq M (\underset{˙}{+}, F) (n) \in C \land F (n + 1) \in D) \to seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1) \in C)$
48	47	adantr	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to ((seq M (\underset{˙}{+}, F) (n) \in C \land F (n + 1) \in D) \to seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1) \in C)$
49	45 48	mpan2d	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to (seq M (\underset{˙}{+}, F) (n) \in C \to seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1) \in C)$
50		seqp1	$⊢ n \in ℤ_{\geq M} \to seq M (\underset{˙}{+}, F) (n + 1) = seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)$
51	50	ad2antrl	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to seq M (\underset{˙}{+}, F) (n + 1) = seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)$
52	51	eleq1d	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to (seq M (\underset{˙}{+}, F) (n + 1) \in C \leftrightarrow seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1) \in C)$
53	49 52	sylibrd	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to (seq M (\underset{˙}{+}, F) (n) \in C \to seq M (\underset{˙}{+}, F) (n + 1) \in C)$
54	34 53	animpimp2impd	$⊢ n \in ℤ_{\geq M} \to ((φ \to (n \in (M \dots N) \to seq M (\underset{˙}{+}, F) (n) \in C)) \to (φ \to (n + 1 \in (M \dots N) \to seq M (\underset{˙}{+}, F) (n + 1) \in C)))$
55	11 16 21 26 30 54	uzind4	$⊢ N \in ℤ_{\geq M} \to (φ \to (N \in (M \dots N) \to seq M (\underset{˙}{+}, F) (N) \in C))$
56	3 55	mpcom	$⊢ φ \to (N \in (M \dots N) \to seq M (\underset{˙}{+}, F) (N) \in C)$
57	6 56	mpd	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) \in C$

Metamath Proof Explorer

Theorem seqcl2

Proof