Step | Hyp | Ref
| Expression |
1 | | summo.1 |
. . 3
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) |
2 | | summo.2 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
3 | | summolem2.7 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀)) |
4 | | summolem2.9 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 Isom < , < ((1...(#‘𝐴)), 𝐴)) |
5 | | summolem2.8 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴) |
6 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢
(1...𝑁) ∈
V |
7 | 6 | f1oen 7862 |
. . . . . . . . . . . . 13
⊢ (𝑓:(1...𝑁)–1-1-onto→𝐴 → (1...𝑁) ≈ 𝐴) |
8 | 5, 7 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝑁) ≈ 𝐴) |
9 | | fzfid 12634 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
10 | 8 | ensymd 7893 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ≈ (1...𝑁)) |
11 | | enfii 8062 |
. . . . . . . . . . . . . 14
⊢
(((1...𝑁) ∈ Fin
∧ 𝐴 ≈ (1...𝑁)) → 𝐴 ∈ Fin) |
12 | 9, 10, 11 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ Fin) |
13 | | hashen 12997 |
. . . . . . . . . . . . 13
⊢
(((1...𝑁) ∈ Fin
∧ 𝐴 ∈ Fin) →
((#‘(1...𝑁)) =
(#‘𝐴) ↔
(1...𝑁) ≈ 𝐴)) |
14 | 9, 12, 13 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((#‘(1...𝑁)) = (#‘𝐴) ↔ (1...𝑁) ≈ 𝐴)) |
15 | 8, 14 | mpbird 246 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘(1...𝑁)) = (#‘𝐴)) |
16 | | summolem2.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
17 | | nnnn0 11176 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
18 | | hashfz1 12996 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ (#‘(1...𝑁)) =
𝑁) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘(1...𝑁)) = 𝑁) |
20 | 15, 19 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝐴) = 𝑁) |
21 | 20 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝜑 → (1...(#‘𝐴)) = (1...𝑁)) |
22 | | isoeq4 6470 |
. . . . . . . . 9
⊢
((1...(#‘𝐴)) =
(1...𝑁) → (𝐾 Isom < , <
((1...(#‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴))) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 Isom < , < ((1...(#‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴))) |
24 | 4, 23 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 → 𝐾 Isom < , < ((1...𝑁), 𝐴)) |
25 | | isof1o 6473 |
. . . . . . 7
⊢ (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto→𝐴) |
26 | 24, 25 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴) |
27 | | f1of 6050 |
. . . . . 6
⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → 𝐾:(1...𝑁)⟶𝐴) |
28 | 26, 27 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐾:(1...𝑁)⟶𝐴) |
29 | | nnuz 11599 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
30 | 16, 29 | syl6eleq 2698 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
31 | | eluzfz2 12220 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘1) → 𝑁 ∈ (1...𝑁)) |
32 | 30, 31 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (1...𝑁)) |
33 | 28, 32 | ffvelrnd 6268 |
. . . 4
⊢ (𝜑 → (𝐾‘𝑁) ∈ 𝐴) |
34 | 3, 33 | sseldd 3569 |
. . 3
⊢ (𝜑 → (𝐾‘𝑁) ∈ (ℤ≥‘𝑀)) |
35 | 3 | sselda 3568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℤ≥‘𝑀)) |
36 | | f1ocnvfv2 6433 |
. . . . . . . . 9
⊢ ((𝐾:(1...𝑁)–1-1-onto→𝐴 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) = 𝑛) |
37 | 26, 36 | sylan 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) = 𝑛) |
38 | | f1ocnv 6062 |
. . . . . . . . . . . 12
⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → ◡𝐾:𝐴–1-1-onto→(1...𝑁)) |
39 | | f1of 6050 |
. . . . . . . . . . . 12
⊢ (◡𝐾:𝐴–1-1-onto→(1...𝑁) → ◡𝐾:𝐴⟶(1...𝑁)) |
40 | 26, 38, 39 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ◡𝐾:𝐴⟶(1...𝑁)) |
41 | 40 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (◡𝐾‘𝑛) ∈ (1...𝑁)) |
42 | | elfzle2 12216 |
. . . . . . . . . 10
⊢ ((◡𝐾‘𝑛) ∈ (1...𝑁) → (◡𝐾‘𝑛) ≤ 𝑁) |
43 | 41, 42 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (◡𝐾‘𝑛) ≤ 𝑁) |
44 | 24 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴)) |
45 | | fzssuz 12253 |
. . . . . . . . . . . . 13
⊢
(1...𝑁) ⊆
(ℤ≥‘1) |
46 | | uzssz 11583 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘1) ⊆ ℤ |
47 | | zssre 11261 |
. . . . . . . . . . . . . 14
⊢ ℤ
⊆ ℝ |
48 | 46, 47 | sstri 3577 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘1) ⊆ ℝ |
49 | 45, 48 | sstri 3577 |
. . . . . . . . . . . 12
⊢
(1...𝑁) ⊆
ℝ |
50 | | ressxr 9962 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℝ* |
51 | 49, 50 | sstri 3577 |
. . . . . . . . . . 11
⊢
(1...𝑁) ⊆
ℝ* |
52 | 51 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (1...𝑁) ⊆
ℝ*) |
53 | 3 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ (ℤ≥‘𝑀)) |
54 | | uzssz 11583 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
55 | 54, 47 | sstri 3577 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘𝑀) ⊆ ℝ |
56 | 53, 55 | syl6ss 3580 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ ℝ) |
57 | 56, 50 | syl6ss 3580 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆
ℝ*) |
58 | 32 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ (1...𝑁)) |
59 | | leisorel 13101 |
. . . . . . . . . 10
⊢ ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ* ∧ 𝐴 ⊆ ℝ*)
∧ ((◡𝐾‘𝑛) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((◡𝐾‘𝑛) ≤ 𝑁 ↔ (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁))) |
60 | 44, 52, 57, 41, 58, 59 | syl122anc 1327 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((◡𝐾‘𝑛) ≤ 𝑁 ↔ (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁))) |
61 | 43, 60 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁)) |
62 | 37, 61 | eqbrtrrd 4607 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ≤ (𝐾‘𝑁)) |
63 | | eluzelz 11573 |
. . . . . . . . 9
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → 𝑛 ∈ ℤ) |
64 | 35, 63 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℤ) |
65 | | eluzelz 11573 |
. . . . . . . . . 10
⊢ ((𝐾‘𝑁) ∈ (ℤ≥‘𝑀) → (𝐾‘𝑁) ∈ ℤ) |
66 | 34, 65 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾‘𝑁) ∈ ℤ) |
67 | 66 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘𝑁) ∈ ℤ) |
68 | | eluz 11577 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ (𝐾‘𝑁) ∈ ℤ) → ((𝐾‘𝑁) ∈ (ℤ≥‘𝑛) ↔ 𝑛 ≤ (𝐾‘𝑁))) |
69 | 64, 67, 68 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((𝐾‘𝑁) ∈ (ℤ≥‘𝑛) ↔ 𝑛 ≤ (𝐾‘𝑁))) |
70 | 62, 69 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘𝑁) ∈ (ℤ≥‘𝑛)) |
71 | | elfzuzb 12207 |
. . . . . 6
⊢ (𝑛 ∈ (𝑀...(𝐾‘𝑁)) ↔ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝐾‘𝑁) ∈ (ℤ≥‘𝑛))) |
72 | 35, 70, 71 | sylanbrc 695 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (𝑀...(𝐾‘𝑁))) |
73 | 72 | ex 449 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ 𝐴 → 𝑛 ∈ (𝑀...(𝐾‘𝑁)))) |
74 | 73 | ssrdv 3574 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ (𝑀...(𝐾‘𝑁))) |
75 | 1, 2, 34, 74 | fsumcvg 14290 |
. 2
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘(𝐾‘𝑁))) |
76 | | addid2 10098 |
. . . . 5
⊢ (𝑚 ∈ ℂ → (0 +
𝑚) = 𝑚) |
77 | 76 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (0 + 𝑚) = 𝑚) |
78 | | addid1 10095 |
. . . . 5
⊢ (𝑚 ∈ ℂ → (𝑚 + 0) = 𝑚) |
79 | 78 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (𝑚 + 0) = 𝑚) |
80 | | addcl 9897 |
. . . . 5
⊢ ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 + 𝑥) ∈ ℂ) |
81 | 80 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 + 𝑥) ∈ ℂ) |
82 | | 0cnd 9912 |
. . . 4
⊢ (𝜑 → 0 ∈
ℂ) |
83 | 32, 21 | eleqtrrd 2691 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (1...(#‘𝐴))) |
84 | | iftrue 4042 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵) |
85 | 84 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵) |
86 | 85, 2 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
87 | 86 | ex 449 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)) |
88 | | iffalse 4045 |
. . . . . . . . 9
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0) |
89 | | 0cn 9911 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
90 | 88, 89 | syl6eqel 2696 |
. . . . . . . 8
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
91 | 87, 90 | pm2.61d1 170 |
. . . . . . 7
⊢ (𝜑 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
92 | 91 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
93 | 92, 1 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → 𝐹:ℤ⟶ℂ) |
94 | | elfzelz 12213 |
. . . . 5
⊢ (𝑚 ∈ (𝑀...(𝐾‘(#‘𝐴))) → 𝑚 ∈ ℤ) |
95 | | ffvelrn 6265 |
. . . . 5
⊢ ((𝐹:ℤ⟶ℂ ∧
𝑚 ∈ ℤ) →
(𝐹‘𝑚) ∈ ℂ) |
96 | 93, 94, 95 | syl2an 493 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀...(𝐾‘(#‘𝐴)))) → (𝐹‘𝑚) ∈ ℂ) |
97 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚)) |
98 | 97 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑘 = 𝑚 → ((𝐹‘𝑘) = 0 ↔ (𝐹‘𝑚) = 0)) |
99 | | eldifi 3694 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴) → 𝑘 ∈ (𝑀...(𝐾‘(#‘𝐴)))) |
100 | | elfzelz 12213 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝑀...(𝐾‘(#‘𝐴))) → 𝑘 ∈ ℤ) |
101 | 99, 100 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴) → 𝑘 ∈ ℤ) |
102 | | eldifn 3695 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴) → ¬ 𝑘 ∈ 𝐴) |
103 | 102, 88 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0) |
104 | 103, 89 | syl6eqel 2696 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
105 | 1 | fvmpt2 6200 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
106 | 101, 104,
105 | syl2anc 691 |
. . . . . . 7
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
107 | 106, 103 | eqtrd 2644 |
. . . . . 6
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = 0) |
108 | 98, 107 | vtoclga 3245 |
. . . . 5
⊢ (𝑚 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴) → (𝐹‘𝑚) = 0) |
109 | 108 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(#‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = 0) |
110 | | isof1o 6473 |
. . . . . . . 8
⊢ (𝐾 Isom < , <
((1...(#‘𝐴)), 𝐴) → 𝐾:(1...(#‘𝐴))–1-1-onto→𝐴) |
111 | | f1of 6050 |
. . . . . . . 8
⊢ (𝐾:(1...(#‘𝐴))–1-1-onto→𝐴 → 𝐾:(1...(#‘𝐴))⟶𝐴) |
112 | 4, 110, 111 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐾:(1...(#‘𝐴))⟶𝐴) |
113 | 112 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → (𝐾‘𝑥) ∈ 𝐴) |
114 | 113 | iftrued 4044 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
115 | 3 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → 𝐴 ⊆ (ℤ≥‘𝑀)) |
116 | 115, 113 | sseldd 3569 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → (𝐾‘𝑥) ∈ (ℤ≥‘𝑀)) |
117 | | eluzelz 11573 |
. . . . . . 7
⊢ ((𝐾‘𝑥) ∈ (ℤ≥‘𝑀) → (𝐾‘𝑥) ∈ ℤ) |
118 | 116, 117 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → (𝐾‘𝑥) ∈ ℤ) |
119 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑘𝜑 |
120 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝐾‘𝑥) ∈ 𝐴 |
121 | | nfcsb1v 3515 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵 |
122 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘0 |
123 | 120, 121,
122 | nfif 4065 |
. . . . . . . . . 10
⊢
Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) |
124 | 123 | nfel1 2765 |
. . . . . . . . 9
⊢
Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ |
125 | 119, 124 | nfim 1813 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝜑 → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) |
126 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐾‘𝑥) ∈ V |
127 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴)) |
128 | | csbeq1a 3508 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝐾‘𝑥) → 𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
129 | 127, 128 | ifbieq1d 4059 |
. . . . . . . . . 10
⊢ (𝑘 = (𝐾‘𝑥) → if(𝑘 ∈ 𝐴, 𝐵, 0) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0)) |
130 | 129 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑘 = (𝐾‘𝑥) → (if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ ↔ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)) |
131 | 130 | imbi2d 329 |
. . . . . . . 8
⊢ (𝑘 = (𝐾‘𝑥) → ((𝜑 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) ↔ (𝜑 → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ))) |
132 | 125, 126,
131, 91 | vtoclf 3231 |
. . . . . . 7
⊢ (𝜑 → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) |
133 | 132 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) |
134 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑛 = (𝐾‘𝑥) → (𝑛 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴)) |
135 | | csbeq1 3502 |
. . . . . . . 8
⊢ (𝑛 = (𝐾‘𝑥) → ⦋𝑛 / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
136 | 134, 135 | ifbieq1d 4059 |
. . . . . . 7
⊢ (𝑛 = (𝐾‘𝑥) → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0)) |
137 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑛if(𝑘 ∈ 𝐴, 𝐵, 0) |
138 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝑛 ∈ 𝐴 |
139 | | nfcsb1v 3515 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐵 |
140 | 138, 139,
122 | nfif 4065 |
. . . . . . . . 9
⊢
Ⅎ𝑘if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) |
141 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (𝑘 ∈ 𝐴 ↔ 𝑛 ∈ 𝐴)) |
142 | | csbeq1a 3508 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → 𝐵 = ⦋𝑛 / 𝑘⦌𝐵) |
143 | 141, 142 | ifbieq1d 4059 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → if(𝑘 ∈ 𝐴, 𝐵, 0) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) |
144 | 137, 140,
143 | cbvmpt 4677 |
. . . . . . . 8
⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) |
145 | 1, 144 | eqtri 2632 |
. . . . . . 7
⊢ 𝐹 = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) |
146 | 136, 145 | fvmptg 6189 |
. . . . . 6
⊢ (((𝐾‘𝑥) ∈ ℤ ∧ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0)) |
147 | 118, 133,
146 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0)) |
148 | | elfznn 12241 |
. . . . . . 7
⊢ (𝑥 ∈ (1...(#‘𝐴)) → 𝑥 ∈ ℕ) |
149 | 148 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → 𝑥 ∈ ℕ) |
150 | 114, 133 | eqeltrrd 2689 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ) |
151 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑛 = 𝑥 → (𝐾‘𝑛) = (𝐾‘𝑥)) |
152 | 151 | csbeq1d 3506 |
. . . . . . 7
⊢ (𝑛 = 𝑥 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
153 | | summolem2.4 |
. . . . . . 7
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⦋(𝐾‘𝑛) / 𝑘⦌𝐵) |
154 | 152, 153 | fvmptg 6189 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧
⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ) → (𝐻‘𝑥) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
155 | 149, 150,
154 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → (𝐻‘𝑥) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
156 | 114, 147,
155 | 3eqtr4rd 2655 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(#‘𝐴))) → (𝐻‘𝑥) = (𝐹‘(𝐾‘𝑥))) |
157 | 77, 79, 81, 82, 4, 83, 3, 96, 109, 156 | seqcoll 13105 |
. . 3
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)) = (seq1( + , 𝐻)‘𝑁)) |
158 | | summo.3 |
. . . 4
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) |
159 | 16, 16 | jca 553 |
. . . 4
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑁 ∈ ℕ)) |
160 | 1, 2, 158, 153, 159, 5, 26 | summolem3 14292 |
. . 3
⊢ (𝜑 → (seq1( + , 𝐺)‘𝑁) = (seq1( + , 𝐻)‘𝑁)) |
161 | 157, 160 | eqtr4d 2647 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)) = (seq1( + , 𝐺)‘𝑁)) |
162 | 75, 161 | breqtrd 4609 |
1
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑁)) |