Metamath Proof Explorer

Theorem iprodefisumlem

Description: Lemma for iprodefisum . (Contributed by Scott Fenton, 11-Feb-2018)

Ref Expression
Hypotheses iprodefisumlem.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
iprodefisumlem.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
iprodefisumlem.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
Assertion iprodefisumlem ( 𝜑 → seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) = ( exp ∘ seq 𝑀 ( + , 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 iprodefisumlem.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 iprodefisumlem.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 iprodefisumlem.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
4 fvco3 ⊢ ( ( 𝐹 : 𝑍 ⟶ ℂ ∧ 𝑘 ∈ 𝑍 ) → ( ( exp ∘ 𝐹 ) ‘ 𝑘 ) = ( exp ‘ ( 𝐹 ‘ 𝑘 ) ) )
5 3 4 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( exp ∘ 𝐹 ) ‘ 𝑘 ) = ( exp ‘ ( 𝐹 ‘ 𝑘 ) ) )
6 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
7 efcl ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ → ( exp ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ )
8 6 7 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( exp ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ )
9 5 8 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( exp ∘ 𝐹 ) ‘ 𝑘 ) ∈ ℂ )
10 1 2 9 prodf ⊢ ( 𝜑 → seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) : 𝑍 ⟶ ℂ )
11 10 ffnd ⊢ ( 𝜑 → seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) Fn 𝑍 )
12 eff ⊢ exp : ℂ ⟶ ℂ
13 ffn ⊢ ( exp : ℂ ⟶ ℂ → exp Fn ℂ )
14 12 13 ax-mp ⊢ exp Fn ℂ
15 1 2 6 serf ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℂ )
16 fnfco ⊢ ( ( exp Fn ℂ ∧ seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℂ ) → ( exp ∘ seq 𝑀 ( + , 𝐹 ) ) Fn 𝑍 )
17 14 15 16 sylancr ⊢ ( 𝜑 → ( exp ∘ seq 𝑀 ( + , 𝐹 ) ) Fn 𝑍 )
18 fveq2 ⊢ ( 𝑗 = 𝑀 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑗 ) = ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑀 ) )
19 2fveq3 ⊢ ( 𝑗 = 𝑀 → ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ) )
20 18 19 eqeq12d ⊢ ( 𝑗 = 𝑀 → ( ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑗 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ↔ ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑀 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ) ) )
21 20 imbi2d ⊢ ( 𝑗 = 𝑀 → ( ( 𝜑 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑗 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ↔ ( 𝜑 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑀 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ) ) ) )
22 fveq2 ⊢ ( 𝑗 = 𝑛 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑗 ) = ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) )
23 2fveq3 ⊢ ( 𝑗 = 𝑛 → ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) )
24 22 23 eqeq12d ⊢ ( 𝑗 = 𝑛 → ( ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑗 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ↔ ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ) )
25 24 imbi2d ⊢ ( 𝑗 = 𝑛 → ( ( 𝜑 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑗 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ↔ ( 𝜑 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ) ) )
26 fveq2 ⊢ ( 𝑗 = ( 𝑛 + 1 ) → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑗 ) = ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ ( 𝑛 + 1 ) ) )
27 2fveq3 ⊢ ( 𝑗 = ( 𝑛 + 1 ) → ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) )
28 26 27 eqeq12d ⊢ ( 𝑗 = ( 𝑛 + 1 ) → ( ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑗 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ↔ ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ ( 𝑛 + 1 ) ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) )
29 28 imbi2d ⊢ ( 𝑗 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑗 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ↔ ( 𝜑 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ ( 𝑛 + 1 ) ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) ) )
30 fveq2 ⊢ ( 𝑗 = 𝑘 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑗 ) = ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑘 ) )
31 2fveq3 ⊢ ( 𝑗 = 𝑘 → ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) )
32 30 31 eqeq12d ⊢ ( 𝑗 = 𝑘 → ( ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑗 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ↔ ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑘 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) )
33 32 imbi2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝜑 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑗 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ↔ ( 𝜑 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑘 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) )
34 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
35 2 34 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
36 35 1 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
37 fvco3 ⊢ ( ( 𝐹 : 𝑍 ⟶ ℂ ∧ 𝑀 ∈ 𝑍 ) → ( ( exp ∘ 𝐹 ) ‘ 𝑀 ) = ( exp ‘ ( 𝐹 ‘ 𝑀 ) ) )
38 3 36 37 syl2anc ⊢ ( 𝜑 → ( ( exp ∘ 𝐹 ) ‘ 𝑀 ) = ( exp ‘ ( 𝐹 ‘ 𝑀 ) ) )
39 seq1 ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑀 ) = ( ( exp ∘ 𝐹 ) ‘ 𝑀 ) )
40 2 39 syl ⊢ ( 𝜑 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑀 ) = ( ( exp ∘ 𝐹 ) ‘ 𝑀 ) )
41 seq1 ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
42 2 41 syl ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
43 42 fveq2d ⊢ ( 𝜑 → ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ) = ( exp ‘ ( 𝐹 ‘ 𝑀 ) ) )
44 38 40 43 3eqtr4d ⊢ ( 𝜑 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑀 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ) )
45 44 a1i ⊢ ( 𝑀 ∈ ℤ → ( 𝜑 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑀 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ) ) )
46 oveq1 ⊢ ( ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) → ( ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) · ( ( exp ∘ 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) · ( ( exp ∘ 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) )
47 46 3ad2ant3 ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ∧ ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ) → ( ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) · ( ( exp ∘ 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) · ( ( exp ∘ 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) )
48 3 adantl ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ) → 𝐹 : 𝑍 ⟶ ℂ )
49 peano2uz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
50 49 1 eleqtrrdi ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑛 + 1 ) ∈ 𝑍 )
51 50 adantr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ) → ( 𝑛 + 1 ) ∈ 𝑍 )
52 fvco3 ⊢ ( ( 𝐹 : 𝑍 ⟶ ℂ ∧ ( 𝑛 + 1 ) ∈ 𝑍 ) → ( ( exp ∘ 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( exp ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
53 48 51 52 syl2anc ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ) → ( ( exp ∘ 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( exp ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
54 53 oveq2d ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ) → ( ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) · ( ( exp ∘ 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) · ( exp ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
55 15 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ )
56 55 expcom ⊢ ( 𝑛 ∈ 𝑍 → ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ) )
57 1 eqcomi ⊢ ( ℤ≥ ‘ 𝑀 ) = 𝑍
58 56 57 eleq2s ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ) )
59 58 imp ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ )
60 48 51 ffvelrnd ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℂ )
61 efadd ⊢ ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ∧ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℂ ) → ( exp ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) = ( ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) · ( exp ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
62 59 60 61 syl2anc ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ) → ( exp ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) = ( ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) · ( exp ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
63 54 62 eqtr4d ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ) → ( ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) · ( ( exp ∘ 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( exp ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
64 63 3adant3 ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ∧ ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ) → ( ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) · ( ( exp ∘ 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( exp ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
65 47 64 eqtrd ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ∧ ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ) → ( ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) · ( ( exp ∘ 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( exp ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
66 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) · ( ( exp ∘ 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) )
67 66 adantr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ) → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) · ( ( exp ∘ 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) )
68 67 3adant3 ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ∧ ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ) → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) · ( ( exp ∘ 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) )
69 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
70 69 adantr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
71 70 fveq2d ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ) → ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( exp ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
72 71 3adant3 ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ∧ ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ) → ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( exp ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
73 65 68 72 3eqtr4d ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝜑 ∧ ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ) → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ ( 𝑛 + 1 ) ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) )
74 73 3exp ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ ( 𝑛 + 1 ) ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) ) )
75 74 a2d ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑛 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ) → ( 𝜑 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ ( 𝑛 + 1 ) ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) ) )
76 21 25 29 33 45 75 uzind4 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑘 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) )
77 76 1 eleq2s ⊢ ( 𝑘 ∈ 𝑍 → ( 𝜑 → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑘 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) )
78 77 impcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑘 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) )
79 fvco3 ⊢ ( ( seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℂ ∧ 𝑘 ∈ 𝑍 ) → ( ( exp ∘ seq 𝑀 ( + , 𝐹 ) ) ‘ 𝑘 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) )
80 15 79 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( exp ∘ seq 𝑀 ( + , 𝐹 ) ) ‘ 𝑘 ) = ( exp ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) )
81 78 80 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) ‘ 𝑘 ) = ( ( exp ∘ seq 𝑀 ( + , 𝐹 ) ) ‘ 𝑘 ) )
82 11 17 81 eqfnfvd ⊢ ( 𝜑 → seq 𝑀 ( · , ( exp ∘ 𝐹 ) ) = ( exp ∘ seq 𝑀 ( + , 𝐹 ) ) )