Metamath Proof Explorer


Theorem summolem2a

Description: Lemma for summo . (Contributed by Mario Carneiro, 3-Apr-2014) (Revised by Mario Carneiro, 20-Apr-2014)

Ref Expression
Hypotheses summo.1 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 0 ) )
summo.2 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
summo.3 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 )
summolem2.4 𝐻 = ( 𝑛 ∈ ℕ ↦ ( 𝐾𝑛 ) / 𝑘 𝐵 )
summolem2.5 ( 𝜑𝑁 ∈ ℕ )
summolem2.6 ( 𝜑𝑀 ∈ ℤ )
summolem2.7 ( 𝜑𝐴 ⊆ ( ℤ𝑀 ) )
summolem2.8 ( 𝜑𝑓 : ( 1 ... 𝑁 ) –1-1-onto𝐴 )
summolem2.9 ( 𝜑𝐾 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
Assertion summolem2a ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ ( seq 1 ( + , 𝐺 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 summo.1 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 0 ) )
2 summo.2 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
3 summo.3 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 )
4 summolem2.4 𝐻 = ( 𝑛 ∈ ℕ ↦ ( 𝐾𝑛 ) / 𝑘 𝐵 )
5 summolem2.5 ( 𝜑𝑁 ∈ ℕ )
6 summolem2.6 ( 𝜑𝑀 ∈ ℤ )
7 summolem2.7 ( 𝜑𝐴 ⊆ ( ℤ𝑀 ) )
8 summolem2.8 ( 𝜑𝑓 : ( 1 ... 𝑁 ) –1-1-onto𝐴 )
9 summolem2.9 ( 𝜑𝐾 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
10 fzfid ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
11 10 8 hasheqf1od ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = ( ♯ ‘ 𝐴 ) )
12 nnnn0 ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
13 hashfz1 ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
14 5 12 13 3syl ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
15 11 14 eqtr3d ( 𝜑 → ( ♯ ‘ 𝐴 ) = 𝑁 )
16 15 oveq2d ( 𝜑 → ( 1 ... ( ♯ ‘ 𝐴 ) ) = ( 1 ... 𝑁 ) )
17 isoeq4 ( ( 1 ... ( ♯ ‘ 𝐴 ) ) = ( 1 ... 𝑁 ) → ( 𝐾 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ↔ 𝐾 Isom < , < ( ( 1 ... 𝑁 ) , 𝐴 ) ) )
18 16 17 syl ( 𝜑 → ( 𝐾 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ↔ 𝐾 Isom < , < ( ( 1 ... 𝑁 ) , 𝐴 ) ) )
19 9 18 mpbid ( 𝜑𝐾 Isom < , < ( ( 1 ... 𝑁 ) , 𝐴 ) )
20 isof1o ( 𝐾 Isom < , < ( ( 1 ... 𝑁 ) , 𝐴 ) → 𝐾 : ( 1 ... 𝑁 ) –1-1-onto𝐴 )
21 19 20 syl ( 𝜑𝐾 : ( 1 ... 𝑁 ) –1-1-onto𝐴 )
22 f1of ( 𝐾 : ( 1 ... 𝑁 ) –1-1-onto𝐴𝐾 : ( 1 ... 𝑁 ) ⟶ 𝐴 )
23 21 22 syl ( 𝜑𝐾 : ( 1 ... 𝑁 ) ⟶ 𝐴 )
24 nnuz ℕ = ( ℤ ‘ 1 )
25 5 24 eleqtrdi ( 𝜑𝑁 ∈ ( ℤ ‘ 1 ) )
26 eluzfz2 ( 𝑁 ∈ ( ℤ ‘ 1 ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
27 25 26 syl ( 𝜑𝑁 ∈ ( 1 ... 𝑁 ) )
28 23 27 ffvelrnd ( 𝜑 → ( 𝐾𝑁 ) ∈ 𝐴 )
29 7 28 sseldd ( 𝜑 → ( 𝐾𝑁 ) ∈ ( ℤ𝑀 ) )
30 7 sselda ( ( 𝜑𝑛𝐴 ) → 𝑛 ∈ ( ℤ𝑀 ) )
31 f1ocnvfv2 ( ( 𝐾 : ( 1 ... 𝑁 ) –1-1-onto𝐴𝑛𝐴 ) → ( 𝐾 ‘ ( 𝐾𝑛 ) ) = 𝑛 )
32 21 31 sylan ( ( 𝜑𝑛𝐴 ) → ( 𝐾 ‘ ( 𝐾𝑛 ) ) = 𝑛 )
33 f1ocnv ( 𝐾 : ( 1 ... 𝑁 ) –1-1-onto𝐴 𝐾 : 𝐴1-1-onto→ ( 1 ... 𝑁 ) )
34 f1of ( 𝐾 : 𝐴1-1-onto→ ( 1 ... 𝑁 ) → 𝐾 : 𝐴 ⟶ ( 1 ... 𝑁 ) )
35 21 33 34 3syl ( 𝜑 𝐾 : 𝐴 ⟶ ( 1 ... 𝑁 ) )
36 35 ffvelrnda ( ( 𝜑𝑛𝐴 ) → ( 𝐾𝑛 ) ∈ ( 1 ... 𝑁 ) )
37 elfzle2 ( ( 𝐾𝑛 ) ∈ ( 1 ... 𝑁 ) → ( 𝐾𝑛 ) ≤ 𝑁 )
38 36 37 syl ( ( 𝜑𝑛𝐴 ) → ( 𝐾𝑛 ) ≤ 𝑁 )
39 19 adantr ( ( 𝜑𝑛𝐴 ) → 𝐾 Isom < , < ( ( 1 ... 𝑁 ) , 𝐴 ) )
40 fzssuz ( 1 ... 𝑁 ) ⊆ ( ℤ ‘ 1 )
41 uzssz ( ℤ ‘ 1 ) ⊆ ℤ
42 zssre ℤ ⊆ ℝ
43 41 42 sstri ( ℤ ‘ 1 ) ⊆ ℝ
44 40 43 sstri ( 1 ... 𝑁 ) ⊆ ℝ
45 ressxr ℝ ⊆ ℝ*
46 44 45 sstri ( 1 ... 𝑁 ) ⊆ ℝ*
47 46 a1i ( ( 𝜑𝑛𝐴 ) → ( 1 ... 𝑁 ) ⊆ ℝ* )
48 7 adantr ( ( 𝜑𝑛𝐴 ) → 𝐴 ⊆ ( ℤ𝑀 ) )
49 uzssz ( ℤ𝑀 ) ⊆ ℤ
50 49 42 sstri ( ℤ𝑀 ) ⊆ ℝ
51 48 50 sstrdi ( ( 𝜑𝑛𝐴 ) → 𝐴 ⊆ ℝ )
52 51 45 sstrdi ( ( 𝜑𝑛𝐴 ) → 𝐴 ⊆ ℝ* )
53 27 adantr ( ( 𝜑𝑛𝐴 ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
54 leisorel ( ( 𝐾 Isom < , < ( ( 1 ... 𝑁 ) , 𝐴 ) ∧ ( ( 1 ... 𝑁 ) ⊆ ℝ*𝐴 ⊆ ℝ* ) ∧ ( ( 𝐾𝑛 ) ∈ ( 1 ... 𝑁 ) ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ) ) → ( ( 𝐾𝑛 ) ≤ 𝑁 ↔ ( 𝐾 ‘ ( 𝐾𝑛 ) ) ≤ ( 𝐾𝑁 ) ) )
55 39 47 52 36 53 54 syl122anc ( ( 𝜑𝑛𝐴 ) → ( ( 𝐾𝑛 ) ≤ 𝑁 ↔ ( 𝐾 ‘ ( 𝐾𝑛 ) ) ≤ ( 𝐾𝑁 ) ) )
56 38 55 mpbid ( ( 𝜑𝑛𝐴 ) → ( 𝐾 ‘ ( 𝐾𝑛 ) ) ≤ ( 𝐾𝑁 ) )
57 32 56 eqbrtrrd ( ( 𝜑𝑛𝐴 ) → 𝑛 ≤ ( 𝐾𝑁 ) )
58 eluzelz ( 𝑛 ∈ ( ℤ𝑀 ) → 𝑛 ∈ ℤ )
59 30 58 syl ( ( 𝜑𝑛𝐴 ) → 𝑛 ∈ ℤ )
60 eluzelz ( ( 𝐾𝑁 ) ∈ ( ℤ𝑀 ) → ( 𝐾𝑁 ) ∈ ℤ )
61 29 60 syl ( 𝜑 → ( 𝐾𝑁 ) ∈ ℤ )
62 61 adantr ( ( 𝜑𝑛𝐴 ) → ( 𝐾𝑁 ) ∈ ℤ )
63 eluz ( ( 𝑛 ∈ ℤ ∧ ( 𝐾𝑁 ) ∈ ℤ ) → ( ( 𝐾𝑁 ) ∈ ( ℤ𝑛 ) ↔ 𝑛 ≤ ( 𝐾𝑁 ) ) )
64 59 62 63 syl2anc ( ( 𝜑𝑛𝐴 ) → ( ( 𝐾𝑁 ) ∈ ( ℤ𝑛 ) ↔ 𝑛 ≤ ( 𝐾𝑁 ) ) )
65 57 64 mpbird ( ( 𝜑𝑛𝐴 ) → ( 𝐾𝑁 ) ∈ ( ℤ𝑛 ) )
66 elfzuzb ( 𝑛 ∈ ( 𝑀 ... ( 𝐾𝑁 ) ) ↔ ( 𝑛 ∈ ( ℤ𝑀 ) ∧ ( 𝐾𝑁 ) ∈ ( ℤ𝑛 ) ) )
67 30 65 66 sylanbrc ( ( 𝜑𝑛𝐴 ) → 𝑛 ∈ ( 𝑀 ... ( 𝐾𝑁 ) ) )
68 67 ex ( 𝜑 → ( 𝑛𝐴𝑛 ∈ ( 𝑀 ... ( 𝐾𝑁 ) ) ) )
69 68 ssrdv ( 𝜑𝐴 ⊆ ( 𝑀 ... ( 𝐾𝑁 ) ) )
70 1 2 29 69 fsumcvg ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐾𝑁 ) ) )
71 addid2 ( 𝑚 ∈ ℂ → ( 0 + 𝑚 ) = 𝑚 )
72 71 adantl ( ( 𝜑𝑚 ∈ ℂ ) → ( 0 + 𝑚 ) = 𝑚 )
73 addid1 ( 𝑚 ∈ ℂ → ( 𝑚 + 0 ) = 𝑚 )
74 73 adantl ( ( 𝜑𝑚 ∈ ℂ ) → ( 𝑚 + 0 ) = 𝑚 )
75 addcl ( ( 𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑚 + 𝑥 ) ∈ ℂ )
76 75 adantl ( ( 𝜑 ∧ ( 𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑚 + 𝑥 ) ∈ ℂ )
77 0cnd ( 𝜑 → 0 ∈ ℂ )
78 27 16 eleqtrrd ( 𝜑𝑁 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
79 iftrue ( 𝑘𝐴 → if ( 𝑘𝐴 , 𝐵 , 0 ) = 𝐵 )
80 79 adantl ( ( 𝜑𝑘𝐴 ) → if ( 𝑘𝐴 , 𝐵 , 0 ) = 𝐵 )
81 80 2 eqeltrd ( ( 𝜑𝑘𝐴 ) → if ( 𝑘𝐴 , 𝐵 , 0 ) ∈ ℂ )
82 81 ex ( 𝜑 → ( 𝑘𝐴 → if ( 𝑘𝐴 , 𝐵 , 0 ) ∈ ℂ ) )
83 iffalse ( ¬ 𝑘𝐴 → if ( 𝑘𝐴 , 𝐵 , 0 ) = 0 )
84 0cn 0 ∈ ℂ
85 83 84 eqeltrdi ( ¬ 𝑘𝐴 → if ( 𝑘𝐴 , 𝐵 , 0 ) ∈ ℂ )
86 82 85 pm2.61d1 ( 𝜑 → if ( 𝑘𝐴 , 𝐵 , 0 ) ∈ ℂ )
87 86 adantr ( ( 𝜑𝑘 ∈ ℤ ) → if ( 𝑘𝐴 , 𝐵 , 0 ) ∈ ℂ )
88 87 1 fmptd ( 𝜑𝐹 : ℤ ⟶ ℂ )
89 elfzelz ( 𝑚 ∈ ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) → 𝑚 ∈ ℤ )
90 ffvelrn ( ( 𝐹 : ℤ ⟶ ℂ ∧ 𝑚 ∈ ℤ ) → ( 𝐹𝑚 ) ∈ ℂ )
91 88 89 90 syl2an ( ( 𝜑𝑚 ∈ ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ) → ( 𝐹𝑚 ) ∈ ℂ )
92 fveqeq2 ( 𝑘 = 𝑚 → ( ( 𝐹𝑘 ) = 0 ↔ ( 𝐹𝑚 ) = 0 ) )
93 eldifi ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → 𝑘 ∈ ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) )
94 93 elfzelzd ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → 𝑘 ∈ ℤ )
95 eldifn ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → ¬ 𝑘𝐴 )
96 95 83 syl ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → if ( 𝑘𝐴 , 𝐵 , 0 ) = 0 )
97 96 84 eqeltrdi ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → if ( 𝑘𝐴 , 𝐵 , 0 ) ∈ ℂ )
98 1 fvmpt2 ( ( 𝑘 ∈ ℤ ∧ if ( 𝑘𝐴 , 𝐵 , 0 ) ∈ ℂ ) → ( 𝐹𝑘 ) = if ( 𝑘𝐴 , 𝐵 , 0 ) )
99 94 97 98 syl2anc ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → ( 𝐹𝑘 ) = if ( 𝑘𝐴 , 𝐵 , 0 ) )
100 99 96 eqtrd ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → ( 𝐹𝑘 ) = 0 )
101 92 100 vtoclga ( 𝑚 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → ( 𝐹𝑚 ) = 0 )
102 101 adantl ( ( 𝜑𝑚 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) ) → ( 𝐹𝑚 ) = 0 )
103 isof1o ( 𝐾 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) → 𝐾 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 )
104 f1of ( 𝐾 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴𝐾 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
105 9 103 104 3syl ( 𝜑𝐾 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
106 105 ffvelrnda ( ( 𝜑𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐾𝑥 ) ∈ 𝐴 )
107 106 iftrued ( ( 𝜑𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → if ( ( 𝐾𝑥 ) ∈ 𝐴 , ( 𝐾𝑥 ) / 𝑘 𝐵 , 0 ) = ( 𝐾𝑥 ) / 𝑘 𝐵 )
108 7 adantr ( ( 𝜑𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝐴 ⊆ ( ℤ𝑀 ) )
109 108 106 sseldd ( ( 𝜑𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐾𝑥 ) ∈ ( ℤ𝑀 ) )
110 eluzelz ( ( 𝐾𝑥 ) ∈ ( ℤ𝑀 ) → ( 𝐾𝑥 ) ∈ ℤ )
111 109 110 syl ( ( 𝜑𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐾𝑥 ) ∈ ℤ )
112 nfv 𝑘 𝜑
113 nfv 𝑘 ( 𝐾𝑥 ) ∈ 𝐴
114 nfcsb1v 𝑘 ( 𝐾𝑥 ) / 𝑘 𝐵
115 nfcv 𝑘 0
116 113 114 115 nfif 𝑘 if ( ( 𝐾𝑥 ) ∈ 𝐴 , ( 𝐾𝑥 ) / 𝑘 𝐵 , 0 )
117 116 nfel1 𝑘 if ( ( 𝐾𝑥 ) ∈ 𝐴 , ( 𝐾𝑥 ) / 𝑘 𝐵 , 0 ) ∈ ℂ
118 112 117 nfim 𝑘 ( 𝜑 → if ( ( 𝐾𝑥 ) ∈ 𝐴 , ( 𝐾𝑥 ) / 𝑘 𝐵 , 0 ) ∈ ℂ )
119 fvex ( 𝐾𝑥 ) ∈ V
120 eleq1 ( 𝑘 = ( 𝐾𝑥 ) → ( 𝑘𝐴 ↔ ( 𝐾𝑥 ) ∈ 𝐴 ) )
121 csbeq1a ( 𝑘 = ( 𝐾𝑥 ) → 𝐵 = ( 𝐾𝑥 ) / 𝑘 𝐵 )
122 120 121 ifbieq1d ( 𝑘 = ( 𝐾𝑥 ) → if ( 𝑘𝐴 , 𝐵 , 0 ) = if ( ( 𝐾𝑥 ) ∈ 𝐴 , ( 𝐾𝑥 ) / 𝑘 𝐵 , 0 ) )
123 122 eleq1d ( 𝑘 = ( 𝐾𝑥 ) → ( if ( 𝑘𝐴 , 𝐵 , 0 ) ∈ ℂ ↔ if ( ( 𝐾𝑥 ) ∈ 𝐴 , ( 𝐾𝑥 ) / 𝑘 𝐵 , 0 ) ∈ ℂ ) )
124 123 imbi2d ( 𝑘 = ( 𝐾𝑥 ) → ( ( 𝜑 → if ( 𝑘𝐴 , 𝐵 , 0 ) ∈ ℂ ) ↔ ( 𝜑 → if ( ( 𝐾𝑥 ) ∈ 𝐴 , ( 𝐾𝑥 ) / 𝑘 𝐵 , 0 ) ∈ ℂ ) ) )
125 118 119 124 86 vtoclf ( 𝜑 → if ( ( 𝐾𝑥 ) ∈ 𝐴 , ( 𝐾𝑥 ) / 𝑘 𝐵 , 0 ) ∈ ℂ )
126 125 adantr ( ( 𝜑𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → if ( ( 𝐾𝑥 ) ∈ 𝐴 , ( 𝐾𝑥 ) / 𝑘 𝐵 , 0 ) ∈ ℂ )
127 eleq1 ( 𝑛 = ( 𝐾𝑥 ) → ( 𝑛𝐴 ↔ ( 𝐾𝑥 ) ∈ 𝐴 ) )
128 csbeq1 ( 𝑛 = ( 𝐾𝑥 ) → 𝑛 / 𝑘 𝐵 = ( 𝐾𝑥 ) / 𝑘 𝐵 )
129 127 128 ifbieq1d ( 𝑛 = ( 𝐾𝑥 ) → if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) = if ( ( 𝐾𝑥 ) ∈ 𝐴 , ( 𝐾𝑥 ) / 𝑘 𝐵 , 0 ) )
130 nfcv 𝑛 if ( 𝑘𝐴 , 𝐵 , 0 )
131 nfv 𝑘 𝑛𝐴
132 nfcsb1v 𝑘 𝑛 / 𝑘 𝐵
133 131 132 115 nfif 𝑘 if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 )
134 eleq1 ( 𝑘 = 𝑛 → ( 𝑘𝐴𝑛𝐴 ) )
135 csbeq1a ( 𝑘 = 𝑛𝐵 = 𝑛 / 𝑘 𝐵 )
136 134 135 ifbieq1d ( 𝑘 = 𝑛 → if ( 𝑘𝐴 , 𝐵 , 0 ) = if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) )
137 130 133 136 cbvmpt ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 0 ) ) = ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) )
138 1 137 eqtri 𝐹 = ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) )
139 129 138 fvmptg ( ( ( 𝐾𝑥 ) ∈ ℤ ∧ if ( ( 𝐾𝑥 ) ∈ 𝐴 , ( 𝐾𝑥 ) / 𝑘 𝐵 , 0 ) ∈ ℂ ) → ( 𝐹 ‘ ( 𝐾𝑥 ) ) = if ( ( 𝐾𝑥 ) ∈ 𝐴 , ( 𝐾𝑥 ) / 𝑘 𝐵 , 0 ) )
140 111 126 139 syl2anc ( ( 𝜑𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐹 ‘ ( 𝐾𝑥 ) ) = if ( ( 𝐾𝑥 ) ∈ 𝐴 , ( 𝐾𝑥 ) / 𝑘 𝐵 , 0 ) )
141 elfznn ( 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → 𝑥 ∈ ℕ )
142 107 126 eqeltrrd ( ( 𝜑𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐾𝑥 ) / 𝑘 𝐵 ∈ ℂ )
143 fveq2 ( 𝑛 = 𝑥 → ( 𝐾𝑛 ) = ( 𝐾𝑥 ) )
144 143 csbeq1d ( 𝑛 = 𝑥 ( 𝐾𝑛 ) / 𝑘 𝐵 = ( 𝐾𝑥 ) / 𝑘 𝐵 )
145 144 4 fvmptg ( ( 𝑥 ∈ ℕ ∧ ( 𝐾𝑥 ) / 𝑘 𝐵 ∈ ℂ ) → ( 𝐻𝑥 ) = ( 𝐾𝑥 ) / 𝑘 𝐵 )
146 141 142 145 syl2an2 ( ( 𝜑𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐻𝑥 ) = ( 𝐾𝑥 ) / 𝑘 𝐵 )
147 107 140 146 3eqtr4rd ( ( 𝜑𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐻𝑥 ) = ( 𝐹 ‘ ( 𝐾𝑥 ) ) )
148 72 74 76 77 9 78 7 91 102 147 seqcoll ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐾𝑁 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑁 ) )
149 5 5 jca ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝑁 ∈ ℕ ) )
150 1 2 3 4 149 8 21 summolem3 ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ 𝑁 ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑁 ) )
151 148 150 eqtr4d ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐾𝑁 ) ) = ( seq 1 ( + , 𝐺 ) ‘ 𝑁 ) )
152 70 151 breqtrd ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ ( seq 1 ( + , 𝐺 ) ‘ 𝑁 ) )