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 syl6eqel ⊢ ( ¬ 𝑘 ∈ 𝐴 → 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 elfzelz ⊢ ( 𝑘 ∈ ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) → 𝑘 ∈ ℤ )
95 93 94 syl ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → 𝑘 ∈ ℤ )
96 eldifn ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → ¬ 𝑘 ∈ 𝐴 )
97 96 83 syl ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) = 0 )
98 97 84 syl6eqel ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ )
99 1 fvmpt2 ⊢ ( ( 𝑘 ∈ ℤ ∧ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
100 95 98 99 syl2anc ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
101 100 97 eqtrd ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) = 0 )
102 92 101 vtoclga ⊢ ( 𝑚 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) → ( 𝐹 ‘ 𝑚 ) = 0 )
103 102 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( 𝑀 ... ( 𝐾 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑚 ) = 0 )
104 isof1o ⊢ ( 𝐾 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) → 𝐾 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
105 f1of ⊢ ( 𝐾 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → 𝐾 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
106 9 104 105 3syl ⊢ ( 𝜑 → 𝐾 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
107 106 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 )
108 107 iftrued ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 0 ) = ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 )
109 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
110 109 107 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐾 ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
111 eluzelz ⊢ ( ( 𝐾 ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ‘ 𝑥 ) ∈ ℤ )
112 110 111 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐾 ‘ 𝑥 ) ∈ ℤ )
113 nfv ⊢ Ⅎ 𝑘 𝜑
114 nfv ⊢ Ⅎ 𝑘 ( 𝐾 ‘ 𝑥 ) ∈ 𝐴
115 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵
116 nfcv ⊢ Ⅎ 𝑘 0
117 114 115 116 nfif ⊢ Ⅎ 𝑘 if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 0 )
118 117 nfel1 ⊢ Ⅎ 𝑘 if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 0 ) ∈ ℂ
119 113 118 nfim ⊢ Ⅎ 𝑘 ( 𝜑 → if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 0 ) ∈ ℂ )
120 fvex ⊢ ( 𝐾 ‘ 𝑥 ) ∈ V
121 eleq1 ⊢ ( 𝑘 = ( 𝐾 ‘ 𝑥 ) → ( 𝑘 ∈ 𝐴 ↔ ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 ) )
122 csbeq1a ⊢ ( 𝑘 = ( 𝐾 ‘ 𝑥 ) → 𝐵 = ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 )
123 121 122 ifbieq1d ⊢ ( 𝑘 = ( 𝐾 ‘ 𝑥 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) = if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 0 ) )
124 123 eleq1d ⊢ ( 𝑘 = ( 𝐾 ‘ 𝑥 ) → ( if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ ↔ if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 0 ) ∈ ℂ ) )
125 124 imbi2d ⊢ ( 𝑘 = ( 𝐾 ‘ 𝑥 ) → ( ( 𝜑 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ ) ↔ ( 𝜑 → if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 0 ) ∈ ℂ ) ) )
126 119 120 125 86 vtoclf ⊢ ( 𝜑 → if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 0 ) ∈ ℂ )
127 126 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 0 ) ∈ ℂ )
128 eleq1 ⊢ ( 𝑛 = ( 𝐾 ‘ 𝑥 ) → ( 𝑛 ∈ 𝐴 ↔ ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 ) )
129 csbeq1 ⊢ ( 𝑛 = ( 𝐾 ‘ 𝑥 ) → ⦋ 𝑛 / 𝑘 ⦌ 𝐵 = ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 )
130 128 129 ifbieq1d ⊢ ( 𝑛 = ( 𝐾 ‘ 𝑥 ) → if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) = if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 0 ) )
131 nfcv ⊢ Ⅎ 𝑛 if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 )
132 nfv ⊢ Ⅎ 𝑘 𝑛 ∈ 𝐴
133 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ 𝐵
134 132 133 116 nfif ⊢ Ⅎ 𝑘 if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 )
135 eleq1 ⊢ ( 𝑘 = 𝑛 → ( 𝑘 ∈ 𝐴 ↔ 𝑛 ∈ 𝐴 ) )
136 csbeq1a ⊢ ( 𝑘 = 𝑛 → 𝐵 = ⦋ 𝑛 / 𝑘 ⦌ 𝐵 )
137 135 136 ifbieq1d ⊢ ( 𝑘 = 𝑛 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) = if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) )
138 131 134 137 cbvmpt ⊢ ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) = ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) )
139 1 138 eqtri ⊢ 𝐹 = ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) )
140 130 139 fvmptg ⊢ ( ( ( 𝐾 ‘ 𝑥 ) ∈ ℤ ∧ if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 0 ) ∈ ℂ ) → ( 𝐹 ‘ ( 𝐾 ‘ 𝑥 ) ) = if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 0 ) )
141 112 127 140 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐹 ‘ ( 𝐾 ‘ 𝑥 ) ) = if ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐴 , ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 , 0 ) )
142 elfznn ⊢ ( 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → 𝑥 ∈ ℕ )
143 108 127 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ∈ ℂ )
144 fveq2 ⊢ ( 𝑛 = 𝑥 → ( 𝐾 ‘ 𝑛 ) = ( 𝐾 ‘ 𝑥 ) )
145 144 csbeq1d ⊢ ( 𝑛 = 𝑥 → ⦋ ( 𝐾 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 )
146 145 4 fvmptg ⊢ ( ( 𝑥 ∈ ℕ ∧ ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ∈ ℂ ) → ( 𝐻 ‘ 𝑥 ) = ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 )
147 142 143 146 syl2an2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐻 ‘ 𝑥 ) = ⦋ ( 𝐾 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 )
148 108 141 147 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐾 ‘ 𝑥 ) ) )
149 72 74 76 77 9 78 7 91 103 148 seqcoll ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐾 ‘ 𝑁 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑁 ) )
150 5 5 jca ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝑁 ∈ ℕ ) )
151 1 2 3 4 150 8 21 summolem3 ⊢ ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ 𝑁 ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑁 ) )
152 149 151 eqtr4d ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐾 ‘ 𝑁 ) ) = ( seq 1 ( + , 𝐺 ) ‘ 𝑁 ) )
153 70 152 breqtrd ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ ( seq 1 ( + , 𝐺 ) ‘ 𝑁 ) )