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

Proof

Step	Hyp	Ref	Expression
1		clim2prod.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		clim2prod.2	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
3		clim2prod.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
4		clim2prod.4	⊢ ( 𝜑 → seq ( 𝑁 + 1 ) ( · , 𝐹 ) ⇝ 𝐴 )
5		eqid	⊢ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) = ( ℤ≥ ‘ ( 𝑁 + 1 ) )
6		uzssz	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
7	1 6	eqsstri	⊢ 𝑍 ⊆ ℤ
8	7 2	sselid	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
9	8	peano2zd	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ )
10	2 1	eleqtrdi	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
11		eluzel2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
12	10 11	syl	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
13	1 12 3	prodf	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) : 𝑍 ⟶ ℂ )
14	13 2	ffvelcdmd	⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
15		seqex	⊢ seq 𝑀 ( · , 𝐹 ) ∈ V
16	15	a1i	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ∈ V )
17		peano2uz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
18		uzss	⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
19	10 17 18	3syl	⊢ ( 𝜑 → ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
20	19 1	sseqtrrdi	⊢ ( 𝜑 → ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⊆ 𝑍 )
21	20	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ∈ 𝑍 )
22	21 3	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
23	5 9 22	prodf	⊢ ( 𝜑 → seq ( 𝑁 + 1 ) ( · , 𝐹 ) : ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⟶ ℂ )
24	23	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℂ )
25		fveq2	⊢ ( 𝑥 = ( 𝑁 + 1 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑁 + 1 ) ) )
26		fveq2	⊢ ( 𝑥 = ( 𝑁 + 1 ) → ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑁 + 1 ) ) )
27	26	oveq2d	⊢ ( 𝑥 = ( 𝑁 + 1 ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑥 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) )
28	25 27	eqeq12d	⊢ ( 𝑥 = ( 𝑁 + 1 ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑥 ) ) ↔ ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) ) )
29	28	imbi2d	⊢ ( 𝑥 = ( 𝑁 + 1 ) → ( ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) ) ) )
30		fveq2	⊢ ( 𝑥 = 𝑛 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) )
31		fveq2	⊢ ( 𝑥 = 𝑛 → ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) )
32	31	oveq2d	⊢ ( 𝑥 = 𝑛 → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑥 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) )
33	30 32	eqeq12d	⊢ ( 𝑥 = 𝑛 → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑥 ) ) ↔ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) ) )
34	33	imbi2d	⊢ ( 𝑥 = 𝑛 → ( ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) ) ) )
35		fveq2	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) )
36		fveq2	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) )
37	36	oveq2d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑥 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) )
38	35 37	eqeq12d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑥 ) ) ↔ ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) )
39	38	imbi2d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) ) )
40		fveq2	⊢ ( 𝑥 = 𝑘 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑘 ) )
41		fveq2	⊢ ( 𝑥 = 𝑘 → ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑘 ) )
42	41	oveq2d	⊢ ( 𝑥 = 𝑘 → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑥 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑘 ) ) )
43	40 42	eqeq12d	⊢ ( 𝑥 = 𝑘 → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑥 ) ) ↔ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑘 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑘 ) ) ) )
44	43	imbi2d	⊢ ( 𝑥 = 𝑘 → ( ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑘 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑘 ) ) ) ) )
45	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 + 1 ) ∈ ℤ ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
46		seqp1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
47	45 46	syl	⊢ ( ( 𝜑 ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
48		seq1	⊢ ( ( 𝑁 + 1 ) ∈ ℤ → ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( 𝐹 ‘ ( 𝑁 + 1 ) ) )
49	48	adantl	⊢ ( ( 𝜑 ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( 𝐹 ‘ ( 𝑁 + 1 ) ) )
50	49	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
51	47 50	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) )
52	51	expcom	⊢ ( ( 𝑁 + 1 ) ∈ ℤ → ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) ) )
53	19	sselda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
54		seqp1	⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
55	53 54	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
56	55	adantr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
57		oveq1	⊢ ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
58	57	adantl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
59	14	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
60	23	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ∈ ℂ )
61		peano2uz	⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
62	61 1	eleqtrrdi	⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑛 + 1 ) ∈ 𝑍 )
63	53 62	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑛 + 1 ) ∈ 𝑍 )
64	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
65		fveq2	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
66	65	eleq1d	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℂ ) )
67	66	rspcv	⊢ ( ( 𝑛 + 1 ) ∈ 𝑍 → ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℂ ) )
68	64 67	mpan9	⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℂ )
69	63 68	syldan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℂ )
70	59 60 69	mulassd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
71	70	adantr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) ) → ( ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
72		seqp1	⊢ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
73	72	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
74	73	oveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
75	74	adantr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
76	71 75	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) ) → ( ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) )
77	56 58 76	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) )
78	77	exp31	⊢ ( 𝜑 → ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) ) )
79	78	com12	⊢ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( 𝜑 → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) ) )
80	79	a2d	⊢ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑛 ) ) ) → ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) ) )
81	29 34 39 44 52 80	uzind4	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑘 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑘 ) ) ) )
82	81	impcom	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑘 ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · ( seq ( 𝑁 + 1 ) ( · , 𝐹 ) ‘ 𝑘 ) ) )
83	5 9 4 14 16 24 82	climmulc2	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · 𝐴 ) )