Metamath Proof Explorer

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 ffvelrnd ⊢ ( 𝜑 → ( 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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑁 + 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 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) · 𝐴 ) )