Theorem 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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	clim2div.2	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
	clim2div.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
	clim2div.4	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ 𝐴 )
	clim2div.5	⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ≠ 0 )
Assertion	clim2div	⊢ ( 𝜑 → seq ( 𝑁 + 1 ) ( · , 𝐹 ) ⇝ ( 𝐴 / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		clim2div.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		clim2div.2	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
3		clim2div.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
4		clim2div.4	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ 𝐴 )
5		clim2div.5	⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ≠ 0 )
6		eqid	⊢ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) = ( ℤ≥ ‘ ( 𝑁 + 1 ) )
7		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
8	7 1	eleq2s	⊢ ( 𝑁 ∈ 𝑍 → 𝑁 ∈ ℤ )
9	2 8	syl	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
10	9	peano2zd	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ )
11		eluzel2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
12	11 1	eleq2s	⊢ ( 𝑁 ∈ 𝑍 → 𝑀 ∈ ℤ )
13	2 12	syl	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
14	1 13 3	prodf	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) : 𝑍 ⟶ ℂ )
15	14 2	ffvelcdmd	⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
16	15 5	reccld	⊢ ( 𝜑 → ( 1 / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) ∈ ℂ )
17		seqex	⊢ seq ( 𝑁 + 1 ) ( · , 𝐹 ) ∈ V
18	17	a1i	⊢ ( 𝜑 → seq ( 𝑁 + 1 ) ( · , 𝐹 ) ∈ V )
19	2 1	eleqtrdi	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
20		peano2uz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
21	19 20	syl	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
22	21 1	eleqtrrdi	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ 𝑍 )
23	1	uztrn2	⊢ ( ( ( 𝑁 + 1 ) ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑗 ∈ 𝑍 )
24	22 23	sylan	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑗 ∈ 𝑍 )
25	14	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
26	24 25	syldan	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
27		mulcl	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
28	27	adantl	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
29		mulass	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑘 · 𝑥 ) · 𝑦 ) = ( 𝑘 · ( 𝑥 · 𝑦 ) ) )
30	29	adantl	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( ( 𝑘 · 𝑥 ) · 𝑦 ) = ( 𝑘 · ( 𝑥 · 𝑦 ) ) )
31		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
32	19	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
33		elfzuz	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
34	33 1	eleqtrrdi	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ 𝑍 )
35	34 3	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
36	35	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
37	28 30 31 32 36	seqsplit	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑗 ) ) )
38	37	eqcomd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑗 ) ) = ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) )
39	15	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
40	1	uztrn2	⊢ ( ( ( 𝑁 + 1 ) ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ∈ 𝑍 )
41	22 40	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ∈ 𝑍 )
42	41 3	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
43	6 10 42	prodf	⊢ ( 𝜑 → seq ( 𝑁 + 1 ) ( · , 𝐹 ) : ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⟶ ℂ )
44	43	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
45	5	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ≠ 0 )
46	26 39 44 45	divmuld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) = ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑗 ) ↔ ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑗 ) ) = ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) ) )
47	38 46	mpbird	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) = ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑗 ) )
48	26 39 45	divrec2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) = ( ( 1 / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) · ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) ) )
49	47 48	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑗 ) = ( ( 1 / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) · ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑗 ) ) )
50	6 10 4 16 18 26 49	climmulc2	⊢ ( 𝜑 → seq ( 𝑁 + 1 ) ( · , 𝐹 ) ⇝ ( ( 1 / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) · 𝐴 ) )
51		climcl	⊢ ( seq 𝑀 ( · , 𝐹 ) ⇝ 𝐴 → 𝐴 ∈ ℂ )
52	4 51	syl	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
53	52 15 5	divrec2d	⊢ ( 𝜑 → ( 𝐴 / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) = ( ( 1 / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) · 𝐴 ) )
54	50 53	breqtrrd	⊢ ( 𝜑 → seq ( 𝑁 + 1 ) ( · , 𝐹 ) ⇝ ( 𝐴 / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) )