Step | Hyp | Ref
| Expression |
1 | | isummo.1 |
. . 3
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) |
2 | | isummo.2 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
3 | | isummolem2a.dc |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴) |
4 | | summolem2.7 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀)) |
5 | | summolem2.9 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴)) |
6 | | 1zzd 9226 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℤ) |
7 | | summolem2.5 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℕ) |
8 | 7 | nnzd 9320 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℤ) |
9 | 6, 8 | fzfigd 10374 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
10 | | summolem2.8 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴) |
11 | 9, 10 | fihasheqf1od 10711 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘(1...𝑁)) = (♯‘𝐴)) |
12 | | nnnn0 9129 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
13 | | hashfz1 10704 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ (♯‘(1...𝑁)) = 𝑁) |
14 | 7, 12, 13 | 3syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁) |
15 | 11, 14 | eqtr3d 2205 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝐴) = 𝑁) |
16 | 15 | oveq2d 5866 |
. . . . . . . . 9
⊢ (𝜑 → (1...(♯‘𝐴)) = (1...𝑁)) |
17 | | isoeq4 5780 |
. . . . . . . . 9
⊢
((1...(♯‘𝐴)) = (1...𝑁) → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴))) |
18 | 16, 17 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴))) |
19 | 5, 18 | mpbid 146 |
. . . . . . 7
⊢ (𝜑 → 𝐾 Isom < , < ((1...𝑁), 𝐴)) |
20 | | isof1o 5783 |
. . . . . . 7
⊢ (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto→𝐴) |
21 | 19, 20 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴) |
22 | | f1of 5440 |
. . . . . 6
⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → 𝐾:(1...𝑁)⟶𝐴) |
23 | 21, 22 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝐾:(1...𝑁)⟶𝐴) |
24 | | nnuz 9509 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
25 | 7, 24 | eleqtrdi 2263 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
26 | | eluzfz2 9975 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘1) → 𝑁 ∈ (1...𝑁)) |
27 | 25, 26 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (1...𝑁)) |
28 | 23, 27 | ffvelrnd 5629 |
. . . 4
⊢ (𝜑 → (𝐾‘𝑁) ∈ 𝐴) |
29 | 4, 28 | sseldd 3148 |
. . 3
⊢ (𝜑 → (𝐾‘𝑁) ∈ (ℤ≥‘𝑀)) |
30 | 4 | sselda 3147 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℤ≥‘𝑀)) |
31 | | f1ocnvfv2 5754 |
. . . . . . . . 9
⊢ ((𝐾:(1...𝑁)–1-1-onto→𝐴 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) = 𝑛) |
32 | 21, 31 | sylan 281 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) = 𝑛) |
33 | | f1ocnv 5453 |
. . . . . . . . . . . 12
⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → ◡𝐾:𝐴–1-1-onto→(1...𝑁)) |
34 | | f1of 5440 |
. . . . . . . . . . . 12
⊢ (◡𝐾:𝐴–1-1-onto→(1...𝑁) → ◡𝐾:𝐴⟶(1...𝑁)) |
35 | 21, 33, 34 | 3syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ◡𝐾:𝐴⟶(1...𝑁)) |
36 | 35 | ffvelrnda 5628 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (◡𝐾‘𝑛) ∈ (1...𝑁)) |
37 | | elfzle2 9971 |
. . . . . . . . . 10
⊢ ((◡𝐾‘𝑛) ∈ (1...𝑁) → (◡𝐾‘𝑛) ≤ 𝑁) |
38 | 36, 37 | syl 14 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (◡𝐾‘𝑛) ≤ 𝑁) |
39 | 19 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴)) |
40 | | fzssuz 10008 |
. . . . . . . . . . . . 13
⊢
(1...𝑁) ⊆
(ℤ≥‘1) |
41 | | uzssz 9493 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘1) ⊆ ℤ |
42 | | zssre 9206 |
. . . . . . . . . . . . . 14
⊢ ℤ
⊆ ℝ |
43 | 41, 42 | sstri 3156 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘1) ⊆ ℝ |
44 | 40, 43 | sstri 3156 |
. . . . . . . . . . . 12
⊢
(1...𝑁) ⊆
ℝ |
45 | | ressxr 7950 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℝ* |
46 | 44, 45 | sstri 3156 |
. . . . . . . . . . 11
⊢
(1...𝑁) ⊆
ℝ* |
47 | 46 | a1i 9 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (1...𝑁) ⊆
ℝ*) |
48 | 4 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ (ℤ≥‘𝑀)) |
49 | | uzssz 9493 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
50 | 49, 42 | sstri 3156 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘𝑀) ⊆ ℝ |
51 | 48, 50 | sstrdi 3159 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ ℝ) |
52 | 51, 45 | sstrdi 3159 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆
ℝ*) |
53 | 27 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ (1...𝑁)) |
54 | | leisorel 10759 |
. . . . . . . . . 10
⊢ ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ* ∧ 𝐴 ⊆ ℝ*)
∧ ((◡𝐾‘𝑛) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((◡𝐾‘𝑛) ≤ 𝑁 ↔ (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁))) |
55 | 39, 47, 52, 36, 53, 54 | syl122anc 1242 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((◡𝐾‘𝑛) ≤ 𝑁 ↔ (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁))) |
56 | 38, 55 | mpbid 146 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁)) |
57 | 32, 56 | eqbrtrrd 4011 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ≤ (𝐾‘𝑁)) |
58 | | eluzelz 9483 |
. . . . . . . . 9
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → 𝑛 ∈ ℤ) |
59 | 30, 58 | syl 14 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℤ) |
60 | | eluzelz 9483 |
. . . . . . . . . 10
⊢ ((𝐾‘𝑁) ∈ (ℤ≥‘𝑀) → (𝐾‘𝑁) ∈ ℤ) |
61 | 29, 60 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾‘𝑁) ∈ ℤ) |
62 | 61 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘𝑁) ∈ ℤ) |
63 | | eluz 9487 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ (𝐾‘𝑁) ∈ ℤ) → ((𝐾‘𝑁) ∈ (ℤ≥‘𝑛) ↔ 𝑛 ≤ (𝐾‘𝑁))) |
64 | 59, 62, 63 | syl2anc 409 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((𝐾‘𝑁) ∈ (ℤ≥‘𝑛) ↔ 𝑛 ≤ (𝐾‘𝑁))) |
65 | 57, 64 | mpbird 166 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘𝑁) ∈ (ℤ≥‘𝑛)) |
66 | | elfzuzb 9962 |
. . . . . 6
⊢ (𝑛 ∈ (𝑀...(𝐾‘𝑁)) ↔ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝐾‘𝑁) ∈ (ℤ≥‘𝑛))) |
67 | 30, 65, 66 | sylanbrc 415 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (𝑀...(𝐾‘𝑁))) |
68 | 67 | ex 114 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ 𝐴 → 𝑛 ∈ (𝑀...(𝐾‘𝑁)))) |
69 | 68 | ssrdv 3153 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ (𝑀...(𝐾‘𝑁))) |
70 | 1, 2, 3, 29, 69 | fsum3cvg 11328 |
. 2
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘(𝐾‘𝑁))) |
71 | | addid2 8045 |
. . . . 5
⊢ (𝑚 ∈ ℂ → (0 +
𝑚) = 𝑚) |
72 | 71 | adantl 275 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (0 + 𝑚) = 𝑚) |
73 | | addid1 8044 |
. . . . 5
⊢ (𝑚 ∈ ℂ → (𝑚 + 0) = 𝑚) |
74 | 73 | adantl 275 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (𝑚 + 0) = 𝑚) |
75 | | addcl 7886 |
. . . . 5
⊢ ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 + 𝑥) ∈ ℂ) |
76 | 75 | adantl 275 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 + 𝑥) ∈ ℂ) |
77 | | 0cnd 7900 |
. . . 4
⊢ (𝜑 → 0 ∈
ℂ) |
78 | 27, 16 | eleqtrrd 2250 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴))) |
79 | | iftrue 3530 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵) |
80 | 79 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵) |
81 | 80, 2 | eqeltrd 2247 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
82 | 81 | adantlr 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
83 | 82 | adantlr 474 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
84 | | iffalse 3533 |
. . . . . . . . . 10
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0) |
85 | | 0cn 7899 |
. . . . . . . . . 10
⊢ 0 ∈
ℂ |
86 | 84, 85 | eqeltrdi 2261 |
. . . . . . . . 9
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
87 | 86 | adantl 275 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ ¬ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
88 | 3 | adantlr 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID
𝑘 ∈ 𝐴) |
89 | | exmiddc 831 |
. . . . . . . . 9
⊢
(DECID 𝑘 ∈ 𝐴 → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴)) |
90 | 88, 89 | syl 14 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴)) |
91 | 83, 87, 90 | mpjaodan 793 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
92 | | simpll 524 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈
(ℤ≥‘𝑀)) → 𝜑) |
93 | | simpr 109 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈
(ℤ≥‘𝑀)) → ¬ 𝑘 ∈ (ℤ≥‘𝑀)) |
94 | 4 | ssneld 3149 |
. . . . . . . . 9
⊢ (𝜑 → (¬ 𝑘 ∈ (ℤ≥‘𝑀) → ¬ 𝑘 ∈ 𝐴)) |
95 | 92, 93, 94 | sylc 62 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈
(ℤ≥‘𝑀)) → ¬ 𝑘 ∈ 𝐴) |
96 | 95, 86 | syl 14 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈
(ℤ≥‘𝑀)) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
97 | | summolem2.6 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
98 | | eluzdc 9556 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) →
DECID 𝑘
∈ (ℤ≥‘𝑀)) |
99 | 97, 98 | sylan 281 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → DECID
𝑘 ∈
(ℤ≥‘𝑀)) |
100 | | exmiddc 831 |
. . . . . . . 8
⊢
(DECID 𝑘 ∈ (ℤ≥‘𝑀) → (𝑘 ∈ (ℤ≥‘𝑀) ∨ ¬ 𝑘 ∈ (ℤ≥‘𝑀))) |
101 | 99, 100 | syl 14 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ (ℤ≥‘𝑀) ∨ ¬ 𝑘 ∈ (ℤ≥‘𝑀))) |
102 | 91, 96, 101 | mpjaodan 793 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
103 | 102, 1 | fmptd 5647 |
. . . . 5
⊢ (𝜑 → 𝐹:ℤ⟶ℂ) |
104 | | eluzelz 9483 |
. . . . 5
⊢ (𝑚 ∈
(ℤ≥‘𝑀) → 𝑚 ∈ ℤ) |
105 | | ffvelrn 5626 |
. . . . 5
⊢ ((𝐹:ℤ⟶ℂ ∧
𝑚 ∈ ℤ) →
(𝐹‘𝑚) ∈ ℂ) |
106 | 103, 104,
105 | syl2an 287 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑚) ∈ ℂ) |
107 | | elnnuz 9510 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ ↔ 𝑚 ∈
(ℤ≥‘1)) |
108 | 107 | biimpri 132 |
. . . . . . 7
⊢ (𝑚 ∈
(ℤ≥‘1) → 𝑚 ∈ ℕ) |
109 | 108 | adantl 275 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ 𝑚 ∈
ℕ) |
110 | | isof1o 5783 |
. . . . . . . . . . . 12
⊢ (𝐾 Isom < , <
((1...(♯‘𝐴)),
𝐴) → 𝐾:(1...(♯‘𝐴))–1-1-onto→𝐴) |
111 | | f1of 5440 |
. . . . . . . . . . . 12
⊢ (𝐾:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝐾:(1...(♯‘𝐴))⟶𝐴) |
112 | 5, 110, 111 | 3syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾:(1...(♯‘𝐴))⟶𝐴) |
113 | 112 | ad2antrr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → 𝐾:(1...(♯‘𝐴))⟶𝐴) |
114 | | 1zzd 9226 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → 1 ∈
ℤ) |
115 | 15, 8 | eqeltrd 2247 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘𝐴) ∈
ℤ) |
116 | 115 | ad2antrr 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → (♯‘𝐴) ∈
ℤ) |
117 | | eluzelz 9483 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈
(ℤ≥‘1) → 𝑚 ∈ ℤ) |
118 | 117 | ad2antlr 486 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ ℤ) |
119 | 114, 116,
118 | 3jca 1172 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → (1 ∈ ℤ ∧
(♯‘𝐴) ∈
ℤ ∧ 𝑚 ∈
ℤ)) |
120 | | eluzle 9486 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈
(ℤ≥‘1) → 1 ≤ 𝑚) |
121 | 120 | ad2antlr 486 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → 1 ≤ 𝑚) |
122 | | simpr 109 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → 𝑚 ≤ 𝑁) |
123 | 15 | breq2d 3999 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑚 ≤ (♯‘𝐴) ↔ 𝑚 ≤ 𝑁)) |
124 | 123 | ad2antrr 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → (𝑚 ≤ (♯‘𝐴) ↔ 𝑚 ≤ 𝑁)) |
125 | 122, 124 | mpbird 166 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → 𝑚 ≤ (♯‘𝐴)) |
126 | 121, 125 | jca 304 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → (1 ≤ 𝑚 ∧ 𝑚 ≤ (♯‘𝐴))) |
127 | | elfz2 9959 |
. . . . . . . . . . 11
⊢ (𝑚 ∈
(1...(♯‘𝐴))
↔ ((1 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (1 ≤ 𝑚 ∧ 𝑚 ≤ (♯‘𝐴)))) |
128 | 119, 126,
127 | sylanbrc 415 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ (1...(♯‘𝐴))) |
129 | 113, 128 | ffvelrnd 5629 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ 𝐴) |
130 | 129 | iftrued 3532 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵) |
131 | 4 | ad2antrr 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → 𝐴 ⊆ (ℤ≥‘𝑀)) |
132 | 23 | ad2antrr 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → 𝐾:(1...𝑁)⟶𝐴) |
133 | 16 | eleq2d 2240 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...𝑁))) |
134 | 133 | ad2antrr 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → (𝑚 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...𝑁))) |
135 | 128, 134 | mpbid 146 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ (1...𝑁)) |
136 | 132, 135 | ffvelrnd 5629 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ 𝐴) |
137 | 131, 136 | sseldd 3148 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ (ℤ≥‘𝑀)) |
138 | 49, 137 | sselid 3145 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ ℤ) |
139 | 102 | ralrimiva 2543 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
140 | 139 | ad2antrr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → ∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
141 | | nfv 1521 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘(𝐾‘𝑚) ∈ 𝐴 |
142 | | nfcsb1v 3082 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵 |
143 | | nfcv 2312 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘0 |
144 | 141, 142,
143 | nfif 3553 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) |
145 | 144 | nfel1 2323 |
. . . . . . . . . 10
⊢
Ⅎ𝑘if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ |
146 | | eleq1 2233 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝐾‘𝑚) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑚) ∈ 𝐴)) |
147 | | csbeq1a 3058 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝐾‘𝑚) → 𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵) |
148 | 146, 147 | ifbieq1d 3547 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝐾‘𝑚) → if(𝑘 ∈ 𝐴, 𝐵, 0) = if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0)) |
149 | 148 | eleq1d 2239 |
. . . . . . . . . 10
⊢ (𝑘 = (𝐾‘𝑚) → (if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ ↔ if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ)) |
150 | 145, 149 | rspc 2828 |
. . . . . . . . 9
⊢ ((𝐾‘𝑚) ∈ ℤ → (∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ)) |
151 | 138, 140,
150 | sylc 62 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ) |
152 | 130, 151 | eqeltrrd 2248 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ 𝑚 ≤ 𝑁) → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) |
153 | | 0cnd 7900 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
∧ ¬ 𝑚 ≤ 𝑁) → 0 ∈
ℂ) |
154 | 109 | nnzd 9320 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ 𝑚 ∈
ℤ) |
155 | 8 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ 𝑁 ∈
ℤ) |
156 | | zdcle 9275 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
DECID 𝑚 ≤
𝑁) |
157 | 154, 155,
156 | syl2anc 409 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ DECID 𝑚 ≤ 𝑁) |
158 | 152, 153,
157 | ifcldadc 3554 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ) |
159 | | breq1 3990 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑛 ≤ 𝑁 ↔ 𝑚 ≤ 𝑁)) |
160 | | fveq2 5494 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝐾‘𝑛) = (𝐾‘𝑚)) |
161 | 160 | csbeq1d 3056 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵) |
162 | 159, 161 | ifbieq1d 3547 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0)) |
163 | | isummolem2a.h |
. . . . . . 7
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0)) |
164 | 162, 163 | fvmptg 5570 |
. . . . . 6
⊢ ((𝑚 ∈ ℕ ∧ if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐻‘𝑚) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0)) |
165 | 109, 158,
164 | syl2anc 409 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ (𝐻‘𝑚) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0)) |
166 | 165, 158 | eqeltrd 2247 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ (𝐻‘𝑚) ∈
ℂ) |
167 | | fveqeq2 5503 |
. . . . . 6
⊢ (𝑘 = 𝑚 → ((𝐹‘𝑘) = 0 ↔ (𝐹‘𝑚) = 0)) |
168 | | eldifi 3249 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴)))) |
169 | | elfzelz 9968 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴))) → 𝑘 ∈ ℤ) |
170 | 168, 169 | syl 14 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ ℤ) |
171 | | eldifn 3250 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → ¬ 𝑘 ∈ 𝐴) |
172 | 171, 84 | syl 14 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0) |
173 | 172, 85 | eqeltrdi 2261 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) |
174 | 1 | fvmpt2 5577 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
175 | 170, 173,
174 | syl2anc 409 |
. . . . . . 7
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0)) |
176 | 175, 172 | eqtrd 2203 |
. . . . . 6
⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = 0) |
177 | 167, 176 | vtoclga 2796 |
. . . . 5
⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑚) = 0) |
178 | 177 | adantl 275 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = 0) |
179 | 112 | ffvelrnda 5628 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ 𝐴) |
180 | 179 | iftrued 3532 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
181 | 4 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ≥‘𝑀)) |
182 | 181, 179 | sseldd 3148 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ (ℤ≥‘𝑀)) |
183 | | eluzelz 9483 |
. . . . . . 7
⊢ ((𝐾‘𝑥) ∈ (ℤ≥‘𝑀) → (𝐾‘𝑥) ∈ ℤ) |
184 | 182, 183 | syl 14 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ ℤ) |
185 | | simpl 108 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝜑) |
186 | 185, 184 | jca 304 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝜑 ∧ (𝐾‘𝑥) ∈ ℤ)) |
187 | | nfv 1521 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) |
188 | | nfv 1521 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝐾‘𝑥) ∈ 𝐴 |
189 | | nfcsb1v 3082 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵 |
190 | 188, 189,
143 | nfif 3553 |
. . . . . . . . . 10
⊢
Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) |
191 | 190 | nfel1 2323 |
. . . . . . . . 9
⊢
Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ |
192 | 187, 191 | nfim 1565 |
. . . . . . . 8
⊢
Ⅎ𝑘((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) |
193 | | eleq1 2233 |
. . . . . . . . . 10
⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ ℤ ↔ (𝐾‘𝑥) ∈ ℤ)) |
194 | 193 | anbi2d 461 |
. . . . . . . . 9
⊢ (𝑘 = (𝐾‘𝑥) → ((𝜑 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝐾‘𝑥) ∈ ℤ))) |
195 | | eleq1 2233 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴)) |
196 | | csbeq1a 3058 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝐾‘𝑥) → 𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
197 | 195, 196 | ifbieq1d 3547 |
. . . . . . . . . 10
⊢ (𝑘 = (𝐾‘𝑥) → if(𝑘 ∈ 𝐴, 𝐵, 0) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0)) |
198 | 197 | eleq1d 2239 |
. . . . . . . . 9
⊢ (𝑘 = (𝐾‘𝑥) → (if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ ↔ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)) |
199 | 194, 198 | imbi12d 233 |
. . . . . . . 8
⊢ (𝑘 = (𝐾‘𝑥) → (((𝜑 ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) ↔ ((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ))) |
200 | 192, 199,
102 | vtoclg1f 2789 |
. . . . . . 7
⊢ ((𝐾‘𝑥) ∈ 𝐴 → ((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)) |
201 | 179, 186,
200 | sylc 62 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) |
202 | | eleq1 2233 |
. . . . . . . 8
⊢ (𝑛 = (𝐾‘𝑥) → (𝑛 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴)) |
203 | | csbeq1 3052 |
. . . . . . . 8
⊢ (𝑛 = (𝐾‘𝑥) → ⦋𝑛 / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
204 | 202, 203 | ifbieq1d 3547 |
. . . . . . 7
⊢ (𝑛 = (𝐾‘𝑥) → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0)) |
205 | | nfcv 2312 |
. . . . . . . . 9
⊢
Ⅎ𝑛if(𝑘 ∈ 𝐴, 𝐵, 0) |
206 | | nfv 1521 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝑛 ∈ 𝐴 |
207 | | nfcsb1v 3082 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐵 |
208 | 206, 207,
143 | nfif 3553 |
. . . . . . . . 9
⊢
Ⅎ𝑘if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) |
209 | | eleq1 2233 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (𝑘 ∈ 𝐴 ↔ 𝑛 ∈ 𝐴)) |
210 | | csbeq1a 3058 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → 𝐵 = ⦋𝑛 / 𝑘⦌𝐵) |
211 | 209, 210 | ifbieq1d 3547 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → if(𝑘 ∈ 𝐴, 𝐵, 0) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) |
212 | 205, 208,
211 | cbvmpt 4082 |
. . . . . . . 8
⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) |
213 | 1, 212 | eqtri 2191 |
. . . . . . 7
⊢ 𝐹 = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) |
214 | 204, 213 | fvmptg 5570 |
. . . . . 6
⊢ (((𝐾‘𝑥) ∈ ℤ ∧ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0)) |
215 | 184, 201,
214 | syl2anc 409 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0)) |
216 | | elfznn 9997 |
. . . . . . . 8
⊢ (𝑥 ∈
(1...(♯‘𝐴))
→ 𝑥 ∈
ℕ) |
217 | 216 | adantl 275 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ∈ ℕ) |
218 | | elfzle2 9971 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
(1...(♯‘𝐴))
→ 𝑥 ≤
(♯‘𝐴)) |
219 | 218 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ≤ (♯‘𝐴)) |
220 | 15 | breq2d 3999 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ≤ (♯‘𝐴) ↔ 𝑥 ≤ 𝑁)) |
221 | 220 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝑥 ≤ (♯‘𝐴) ↔ 𝑥 ≤ 𝑁)) |
222 | 219, 221 | mpbid 146 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ≤ 𝑁) |
223 | 222 | iftrued 3532 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
224 | 180, 201 | eqeltrrd 2248 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ) |
225 | 223, 224 | eqeltrd 2247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) |
226 | | breq1 3990 |
. . . . . . . . 9
⊢ (𝑛 = 𝑥 → (𝑛 ≤ 𝑁 ↔ 𝑥 ≤ 𝑁)) |
227 | | fveq2 5494 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑥 → (𝐾‘𝑛) = (𝐾‘𝑥)) |
228 | 227 | csbeq1d 3056 |
. . . . . . . . 9
⊢ (𝑛 = 𝑥 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
229 | 226, 228 | ifbieq1d 3547 |
. . . . . . . 8
⊢ (𝑛 = 𝑥 → if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0)) |
230 | 229, 163 | fvmptg 5570 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ ∧ if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐻‘𝑥) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0)) |
231 | 217, 225,
230 | syl2anc 409 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0)) |
232 | 231, 223 | eqtrd 2203 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵) |
233 | 180, 215,
232 | 3eqtr4rd 2214 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = (𝐹‘(𝐾‘𝑥))) |
234 | 72, 74, 76, 77, 5, 78, 4, 106, 166, 178, 233 | seq3coll 10764 |
. . 3
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)) = (seq1( + , 𝐻)‘𝑁)) |
235 | 15, 7 | eqeltrd 2247 |
. . . . 5
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ) |
236 | 235, 7 | jca 304 |
. . . 4
⊢ (𝜑 → ((♯‘𝐴) ∈ ℕ ∧ 𝑁 ∈
ℕ)) |
237 | 16 | eqcomd 2176 |
. . . . . 6
⊢ (𝜑 → (1...𝑁) = (1...(♯‘𝐴))) |
238 | | f1oeq2 5430 |
. . . . . 6
⊢
((1...𝑁) =
(1...(♯‘𝐴))
→ (𝑓:(1...𝑁)–1-1-onto→𝐴 ↔ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) |
239 | 237, 238 | syl 14 |
. . . . 5
⊢ (𝜑 → (𝑓:(1...𝑁)–1-1-onto→𝐴 ↔ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) |
240 | 10, 239 | mpbid 146 |
. . . 4
⊢ (𝜑 → 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) |
241 | | isummolem2a.g |
. . . 4
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) |
242 | 1, 2, 236, 240, 21, 241, 163 | summodclem3 11330 |
. . 3
⊢ (𝜑 → (seq1( + , 𝐺)‘(♯‘𝐴)) = (seq1( + , 𝐻)‘𝑁)) |
243 | 15 | fveq2d 5498 |
. . 3
⊢ (𝜑 → (seq1( + , 𝐺)‘(♯‘𝐴)) = (seq1( + , 𝐺)‘𝑁)) |
244 | 234, 242,
243 | 3eqtr2d 2209 |
. 2
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)) = (seq1( + , 𝐺)‘𝑁)) |
245 | 70, 244 | breqtrd 4013 |
1
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑁)) |