clim2prod

Description: The limit of an infinite product with an initial segment added. (Contributed by Scott Fenton, 18-Dec-2017)

	Ref	Expression
Hypotheses	clim2prod.1	$⊢ Z = ℤ_{\geq M}$
	clim2prod.2	$⊢ φ \to N \in Z$
	clim2prod.3	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
	clim2prod.4	$⊢ φ \to seq (N + 1) (\times F) ⇝ A$
Assertion	clim2prod	$⊢ φ \to seq M (\times F) ⇝ seq M (\times F) (N) A$

Proof

Step	Hyp	Ref	Expression
1		clim2prod.1	$⊢ Z = ℤ_{\geq M}$
2		clim2prod.2	$⊢ φ \to N \in Z$
3		clim2prod.3	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
4		clim2prod.4	$⊢ φ \to seq (N + 1) (\times F) ⇝ A$
5		eqid	$⊢ ℤ_{\geq (N + 1)} = ℤ_{\geq (N + 1)}$
6		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
7	1 6	eqsstri	$⊢ Z \subseteq ℤ$
8	7 2	sselid	$⊢ φ \to N \in ℤ$
9	8	peano2zd	$⊢ φ \to N + 1 \in ℤ$
10	2 1	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq M}$
11		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
12	10 11	syl	$⊢ φ \to M \in ℤ$
13	1 12 3	prodf	$⊢ φ \to seq M (\times F) : Z ⟶ ℂ$
14	13 2	ffvelrnd	$⊢ φ \to seq M (\times F) (N) \in ℂ$
15		seqex	$⊢ seq M (\times F) \in V$
16	15	a1i	$⊢ φ \to seq M (\times F) \in V$
17		peano2uz	$⊢ N \in ℤ_{\geq M} \to N + 1 \in ℤ_{\geq M}$
18		uzss	$⊢ N + 1 \in ℤ_{\geq M} \to ℤ_{\geq (N + 1)} \subseteq ℤ_{\geq M}$
19	10 17 18	3syl	$⊢ φ \to ℤ_{\geq (N + 1)} \subseteq ℤ_{\geq M}$
20	19 1	sseqtrrdi	$⊢ φ \to ℤ_{\geq (N + 1)} \subseteq Z$
21	20	sselda	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to k \in Z$
22	21 3	syldan	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to F (k) \in ℂ$
23	5 9 22	prodf	$⊢ φ \to seq (N + 1) (\times F) : ℤ_{\geq (N + 1)} ⟶ ℂ$
24	23	ffvelrnda	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to seq (N + 1) (\times F) (k) \in ℂ$
25		fveq2	$⊢ x = N + 1 \to seq M (\times F) (x) = seq M (\times F) (N + 1)$
26		fveq2	$⊢ x = N + 1 \to seq (N + 1) (\times F) (x) = seq (N + 1) (\times F) (N + 1)$
27	26	oveq2d	$⊢ x = N + 1 \to seq M (\times F) (N) seq (N + 1) (\times F) (x) = seq M (\times F) (N) seq (N + 1) (\times F) (N + 1)$
28	25 27	eqeq12d	$⊢ x = N + 1 \to (seq M (\times F) (x) = seq M (\times F) (N) seq (N + 1) (\times F) (x) \leftrightarrow seq M (\times F) (N + 1) = seq M (\times F) (N) seq (N + 1) (\times F) (N + 1))$
29	28	imbi2d	$⊢ x = N + 1 \to ((φ \to seq M (\times F) (x) = seq M (\times F) (N) seq (N + 1) (\times F) (x)) \leftrightarrow (φ \to seq M (\times F) (N + 1) = seq M (\times F) (N) seq (N + 1) (\times F) (N + 1)))$
30		fveq2	$⊢ x = n \to seq M (\times F) (x) = seq M (\times F) (n)$
31		fveq2	$⊢ x = n \to seq (N + 1) (\times F) (x) = seq (N + 1) (\times F) (n)$
32	31	oveq2d	$⊢ x = n \to seq M (\times F) (N) seq (N + 1) (\times F) (x) = seq M (\times F) (N) seq (N + 1) (\times F) (n)$
33	30 32	eqeq12d	$⊢ x = n \to (seq M (\times F) (x) = seq M (\times F) (N) seq (N + 1) (\times F) (x) \leftrightarrow seq M (\times F) (n) = seq M (\times F) (N) seq (N + 1) (\times F) (n))$
34	33	imbi2d	$⊢ x = n \to ((φ \to seq M (\times F) (x) = seq M (\times F) (N) seq (N + 1) (\times F) (x)) \leftrightarrow (φ \to seq M (\times F) (n) = seq M (\times F) (N) seq (N + 1) (\times F) (n)))$
35		fveq2	$⊢ x = n + 1 \to seq M (\times F) (x) = seq M (\times F) (n + 1)$
36		fveq2	$⊢ x = n + 1 \to seq (N + 1) (\times F) (x) = seq (N + 1) (\times F) (n + 1)$
37	36	oveq2d	$⊢ x = n + 1 \to seq M (\times F) (N) seq (N + 1) (\times F) (x) = seq M (\times F) (N) seq (N + 1) (\times F) (n + 1)$
38	35 37	eqeq12d	$⊢ x = n + 1 \to (seq M (\times F) (x) = seq M (\times F) (N) seq (N + 1) (\times F) (x) \leftrightarrow seq M (\times F) (n + 1) = seq M (\times F) (N) seq (N + 1) (\times F) (n + 1))$
39	38	imbi2d	$⊢ x = n + 1 \to ((φ \to seq M (\times F) (x) = seq M (\times F) (N) seq (N + 1) (\times F) (x)) \leftrightarrow (φ \to seq M (\times F) (n + 1) = seq M (\times F) (N) seq (N + 1) (\times F) (n + 1)))$
40		fveq2	$⊢ x = k \to seq M (\times F) (x) = seq M (\times F) (k)$
41		fveq2	$⊢ x = k \to seq (N + 1) (\times F) (x) = seq (N + 1) (\times F) (k)$
42	41	oveq2d	$⊢ x = k \to seq M (\times F) (N) seq (N + 1) (\times F) (x) = seq M (\times F) (N) seq (N + 1) (\times F) (k)$
43	40 42	eqeq12d	$⊢ x = k \to (seq M (\times F) (x) = seq M (\times F) (N) seq (N + 1) (\times F) (x) \leftrightarrow seq M (\times F) (k) = seq M (\times F) (N) seq (N + 1) (\times F) (k))$
44	43	imbi2d	$⊢ x = k \to ((φ \to seq M (\times F) (x) = seq M (\times F) (N) seq (N + 1) (\times F) (x)) \leftrightarrow (φ \to seq M (\times F) (k) = seq M (\times F) (N) seq (N + 1) (\times F) (k)))$
45	10	adantr	$⊢ (φ \land N + 1 \in ℤ) \to N \in ℤ_{\geq M}$
46		seqp1	$⊢ N \in ℤ_{\geq M} \to seq M (\times F) (N + 1) = seq M (\times F) (N) F (N + 1)$
47	45 46	syl	$⊢ (φ \land N + 1 \in ℤ) \to seq M (\times F) (N + 1) = seq M (\times F) (N) F (N + 1)$
48		seq1	$⊢ N + 1 \in ℤ \to seq (N + 1) (\times F) (N + 1) = F (N + 1)$
49	48	adantl	$⊢ (φ \land N + 1 \in ℤ) \to seq (N + 1) (\times F) (N + 1) = F (N + 1)$
50	49	oveq2d	$⊢ (φ \land N + 1 \in ℤ) \to seq M (\times F) (N) seq (N + 1) (\times F) (N + 1) = seq M (\times F) (N) F (N + 1)$
51	47 50	eqtr4d	$⊢ (φ \land N + 1 \in ℤ) \to seq M (\times F) (N + 1) = seq M (\times F) (N) seq (N + 1) (\times F) (N + 1)$
52	51	expcom	$⊢ N + 1 \in ℤ \to (φ \to seq M (\times F) (N + 1) = seq M (\times F) (N) seq (N + 1) (\times F) (N + 1))$
53	19	sselda	$⊢ (φ \land n \in ℤ_{\geq (N + 1)}) \to n \in ℤ_{\geq M}$
54		seqp1	$⊢ n \in ℤ_{\geq M} \to seq M (\times F) (n + 1) = seq M (\times F) (n) F (n + 1)$
55	53 54	syl	$⊢ (φ \land n \in ℤ_{\geq (N + 1)}) \to seq M (\times F) (n + 1) = seq M (\times F) (n) F (n + 1)$
56	55	adantr	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land seq M (\times F) (n) = seq M (\times F) (N) seq (N + 1) (\times F) (n)) \to seq M (\times F) (n + 1) = seq M (\times F) (n) F (n + 1)$
57		oveq1	$⊢ seq M (\times F) (n) = seq M (\times F) (N) seq (N + 1) (\times F) (n) \to seq M (\times F) (n) F (n + 1) = seq M (\times F) (N) seq (N + 1) (\times F) (n) F (n + 1)$
58	57	adantl	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land seq M (\times F) (n) = seq M (\times F) (N) seq (N + 1) (\times F) (n)) \to seq M (\times F) (n) F (n + 1) = seq M (\times F) (N) seq (N + 1) (\times F) (n) F (n + 1)$
59	14	adantr	$⊢ (φ \land n \in ℤ_{\geq (N + 1)}) \to seq M (\times F) (N) \in ℂ$
60	23	ffvelrnda	$⊢ (φ \land n \in ℤ_{\geq (N + 1)}) \to seq (N + 1) (\times F) (n) \in ℂ$
61		peano2uz	$⊢ n \in ℤ_{\geq M} \to n + 1 \in ℤ_{\geq M}$
62	61 1	eleqtrrdi	$⊢ n \in ℤ_{\geq M} \to n + 1 \in Z$
63	53 62	syl	$⊢ (φ \land n \in ℤ_{\geq (N + 1)}) \to n + 1 \in Z$
64	3	ralrimiva	$⊢ φ \to \forall k \in Z F (k) \in ℂ$
65		fveq2	$⊢ k = n + 1 \to F (k) = F (n + 1)$
66	65	eleq1d	$⊢ k = n + 1 \to (F (k) \in ℂ \leftrightarrow F (n + 1) \in ℂ)$
67	66	rspcv	$⊢ n + 1 \in Z \to (\forall k \in Z F (k) \in ℂ \to F (n + 1) \in ℂ)$
68	64 67	mpan9	$⊢ (φ \land n + 1 \in Z) \to F (n + 1) \in ℂ$
69	63 68	syldan	$⊢ (φ \land n \in ℤ_{\geq (N + 1)}) \to F (n + 1) \in ℂ$
70	59 60 69	mulassd	$⊢ (φ \land n \in ℤ_{\geq (N + 1)}) \to seq M (\times F) (N) seq (N + 1) (\times F) (n) F (n + 1) = seq M (\times F) (N) seq (N + 1) (\times F) (n) F (n + 1)$
71	70	adantr	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land seq M (\times F) (n) = seq M (\times F) (N) seq (N + 1) (\times F) (n)) \to seq M (\times F) (N) seq (N + 1) (\times F) (n) F (n + 1) = seq M (\times F) (N) seq (N + 1) (\times F) (n) F (n + 1)$
72		seqp1	$⊢ n \in ℤ_{\geq (N + 1)} \to seq (N + 1) (\times F) (n + 1) = seq (N + 1) (\times F) (n) F (n + 1)$
73	72	adantl	$⊢ (φ \land n \in ℤ_{\geq (N + 1)}) \to seq (N + 1) (\times F) (n + 1) = seq (N + 1) (\times F) (n) F (n + 1)$
74	73	oveq2d	$⊢ (φ \land n \in ℤ_{\geq (N + 1)}) \to seq M (\times F) (N) seq (N + 1) (\times F) (n + 1) = seq M (\times F) (N) seq (N + 1) (\times F) (n) F (n + 1)$
75	74	adantr	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land seq M (\times F) (n) = seq M (\times F) (N) seq (N + 1) (\times F) (n)) \to seq M (\times F) (N) seq (N + 1) (\times F) (n + 1) = seq M (\times F) (N) seq (N + 1) (\times F) (n) F (n + 1)$
76	71 75	eqtr4d	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land seq M (\times F) (n) = seq M (\times F) (N) seq (N + 1) (\times F) (n)) \to seq M (\times F) (N) seq (N + 1) (\times F) (n) F (n + 1) = seq M (\times F) (N) seq (N + 1) (\times F) (n + 1)$
77	56 58 76	3eqtrd	$⊢ ((φ \land n \in ℤ_{\geq (N + 1)}) \land seq M (\times F) (n) = seq M (\times F) (N) seq (N + 1) (\times F) (n)) \to seq M (\times F) (n + 1) = seq M (\times F) (N) seq (N + 1) (\times F) (n + 1)$
78	77	exp31	$⊢ φ \to (n \in ℤ_{\geq (N + 1)} \to (seq M (\times F) (n) = seq M (\times F) (N) seq (N + 1) (\times F) (n) \to seq M (\times F) (n + 1) = seq M (\times F) (N) seq (N + 1) (\times F) (n + 1)))$
79	78	com12	$⊢ n \in ℤ_{\geq (N + 1)} \to (φ \to (seq M (\times F) (n) = seq M (\times F) (N) seq (N + 1) (\times F) (n) \to seq M (\times F) (n + 1) = seq M (\times F) (N) seq (N + 1) (\times F) (n + 1)))$
80	79	a2d	$⊢ n \in ℤ_{\geq (N + 1)} \to ((φ \to seq M (\times F) (n) = seq M (\times F) (N) seq (N + 1) (\times F) (n)) \to (φ \to seq M (\times F) (n + 1) = seq M (\times F) (N) seq (N + 1) (\times F) (n + 1)))$
81	29 34 39 44 52 80	uzind4	$⊢ k \in ℤ_{\geq (N + 1)} \to (φ \to seq M (\times F) (k) = seq M (\times F) (N) seq (N + 1) (\times F) (k))$
82	81	impcom	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to seq M (\times F) (k) = seq M (\times F) (N) seq (N + 1) (\times F) (k)$
83	5 9 4 14 16 24 82	climmulc2	$⊢ φ \to seq M (\times F) ⇝ seq M (\times F) (N) A$

Metamath Proof Explorer

Theorem clim2prod

Proof