clim2div

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

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

Proof

Step	Hyp	Ref	Expression
1		clim2div.1	$⊢ Z = ℤ_{\geq M}$
2		clim2div.2	$⊢ φ \to N \in Z$
3		clim2div.3	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
4		clim2div.4	$⊢ φ \to seq M (\times F) ⇝ A$
5		clim2div.5	$⊢ φ \to seq M (\times F) (N) \neq 0$
6		eqid	$⊢ ℤ_{\geq (N + 1)} = ℤ_{\geq (N + 1)}$
7		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
8	7 1	eleq2s	$⊢ N \in Z \to N \in ℤ$
9	2 8	syl	$⊢ φ \to N \in ℤ$
10	9	peano2zd	$⊢ φ \to N + 1 \in ℤ$
11		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
12	11 1	eleq2s	$⊢ N \in Z \to M \in ℤ$
13	2 12	syl	$⊢ φ \to M \in ℤ$
14	1 13 3	prodf	$⊢ φ \to seq M (\times F) : Z ⟶ ℂ$
15	14 2	ffvelcdmd	$⊢ φ \to seq M (\times F) (N) \in ℂ$
16	15 5	reccld	$⊢ φ \to \frac{1}{seq M (\times F) (N)} \in ℂ$
17		seqex	$⊢ seq (N + 1) (\times F) \in V$
18	17	a1i	$⊢ φ \to seq (N + 1) (\times F) \in V$
19	2 1	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq M}$
20		peano2uz	$⊢ N \in ℤ_{\geq M} \to N + 1 \in ℤ_{\geq M}$
21	19 20	syl	$⊢ φ \to N + 1 \in ℤ_{\geq M}$
22	21 1	eleqtrrdi	$⊢ φ \to N + 1 \in Z$
23	1	uztrn2	$⊢ (N + 1 \in Z \land j \in ℤ_{\geq (N + 1)}) \to j \in Z$
24	22 23	sylan	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to j \in Z$
25	14	ffvelcdmda	$⊢ (φ \land j \in Z) \to seq M (\times F) (j) \in ℂ$
26	24 25	syldan	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq M (\times F) (j) \in ℂ$
27		mulcl	$⊢ (k \in ℂ \land x \in ℂ) \to k x \in ℂ$
28	27	adantl	$⊢ ((φ \land j \in ℤ_{\geq (N + 1)}) \land (k \in ℂ \land x \in ℂ)) \to k x \in ℂ$
29		mulass	$⊢ (k \in ℂ \land x \in ℂ \land y \in ℂ) \to k x y = k x y$
30	29	adantl	$⊢ ((φ \land j \in ℤ_{\geq (N + 1)}) \land (k \in ℂ \land x \in ℂ \land y \in ℂ)) \to k x y = k x y$
31		simpr	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to j \in ℤ_{\geq (N + 1)}$
32	19	adantr	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to N \in ℤ_{\geq M}$
33		elfzuz	$⊢ k \in (M \dots j) \to k \in ℤ_{\geq M}$
34	33 1	eleqtrrdi	$⊢ k \in (M \dots j) \to k \in Z$
35	34 3	sylan2	$⊢ (φ \land k \in (M \dots j)) \to F (k) \in ℂ$
36	35	adantlr	$⊢ ((φ \land j \in ℤ_{\geq (N + 1)}) \land k \in (M \dots j)) \to F (k) \in ℂ$
37	28 30 31 32 36	seqsplit	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq M (\times F) (j) = seq M (\times F) (N) seq (N + 1) (\times F) (j)$
38	37	eqcomd	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq M (\times F) (N) seq (N + 1) (\times F) (j) = seq M (\times F) (j)$
39	15	adantr	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq M (\times F) (N) \in ℂ$
40	1	uztrn2	$⊢ (N + 1 \in Z \land k \in ℤ_{\geq (N + 1)}) \to k \in Z$
41	22 40	sylan	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to k \in Z$
42	41 3	syldan	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to F (k) \in ℂ$
43	6 10 42	prodf	$⊢ φ \to seq (N + 1) (\times F) : ℤ_{\geq (N + 1)} ⟶ ℂ$
44	43	ffvelcdmda	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq (N + 1) (\times F) (j) \in ℂ$
45	5	adantr	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq M (\times F) (N) \neq 0$
46	26 39 44 45	divmuld	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to (\frac{seq M (\times F) (j)}{seq M (\times F) (N)} = seq (N + 1) (\times F) (j) \leftrightarrow seq M (\times F) (N) seq (N + 1) (\times F) (j) = seq M (\times F) (j))$
47	38 46	mpbird	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to \frac{seq M (\times F) (j)}{seq M (\times F) (N)} = seq (N + 1) (\times F) (j)$
48	26 39 45	divrec2d	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to \frac{seq M (\times F) (j)}{seq M (\times F) (N)} = (\frac{1}{seq M (\times F) (N)}) seq M (\times F) (j)$
49	47 48	eqtr3d	$⊢ (φ \land j \in ℤ_{\geq (N + 1)}) \to seq (N + 1) (\times F) (j) = (\frac{1}{seq M (\times F) (N)}) seq M (\times F) (j)$
50	6 10 4 16 18 26 49	climmulc2	$⊢ φ \to seq (N + 1) (\times F) ⇝ (\frac{1}{seq M (\times F) (N)}) A$
51		climcl	$⊢ seq M (\times F) ⇝ A \to A \in ℂ$
52	4 51	syl	$⊢ φ \to A \in ℂ$
53	52 15 5	divrec2d	$⊢ φ \to \frac{A}{seq M (\times F) (N)} = (\frac{1}{seq M (\times F) (N)}) A$
54	50 53	breqtrrd	$⊢ φ \to seq (N + 1) (\times F) ⇝ (\frac{A}{seq M (\times F) (N)})$

Metamath Proof Explorer

Theorem clim2div

Proof