Step | Hyp | Ref
| Expression |
1 | | addcl 7617 |
. . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 + 𝑗) ∈ ℂ) |
2 | 1 | adantl 273 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 + 𝑗) ∈ ℂ) |
3 | | addcom 7770 |
. . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 + 𝑗) = (𝑗 + 𝑚)) |
4 | 3 | adantl 273 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 + 𝑗) = (𝑗 + 𝑚)) |
5 | | addass 7622 |
. . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑚 + 𝑗) + 𝑦) = (𝑚 + (𝑗 + 𝑦))) |
6 | 5 | adantl 273 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝑚 + 𝑗) + 𝑦) = (𝑚 + (𝑗 + 𝑦))) |
7 | | isummolem3.5 |
. . . . 5
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) |
8 | 7 | simpld 111 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) |
9 | | nnuz 9211 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
10 | 8, 9 | syl6eleq 2192 |
. . 3
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
11 | | isummolem3.6 |
. . . . . 6
⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴) |
12 | | f1ocnv 5314 |
. . . . . 6
⊢ (𝑓:(1...𝑀)–1-1-onto→𝐴 → ◡𝑓:𝐴–1-1-onto→(1...𝑀)) |
13 | 11, 12 | syl 14 |
. . . . 5
⊢ (𝜑 → ◡𝑓:𝐴–1-1-onto→(1...𝑀)) |
14 | | isummolem3.7 |
. . . . 5
⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴) |
15 | | f1oco 5324 |
. . . . 5
⊢ ((◡𝑓:𝐴–1-1-onto→(1...𝑀) ∧ 𝐾:(1...𝑁)–1-1-onto→𝐴) → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀)) |
16 | 13, 14, 15 | syl2anc 406 |
. . . 4
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀)) |
17 | | isummo.1 |
. . . . . . . 8
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) |
18 | | isummo.2 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
19 | 17, 18, 7, 11, 14 | isummolemnm 10987 |
. . . . . . 7
⊢ (𝜑 → 𝑁 = 𝑀) |
20 | 19 | eqcomd 2105 |
. . . . . 6
⊢ (𝜑 → 𝑀 = 𝑁) |
21 | 20 | oveq2d 5722 |
. . . . 5
⊢ (𝜑 → (1...𝑀) = (1...𝑁)) |
22 | | f1oeq2 5293 |
. . . . 5
⊢
((1...𝑀) =
(1...𝑁) → ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) ↔ (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀))) |
23 | 21, 22 | syl 14 |
. . . 4
⊢ (𝜑 → ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) ↔ (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀))) |
24 | 16, 23 | mpbird 166 |
. . 3
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀)) |
25 | | elnnuz 9212 |
. . . 4
⊢ (𝑚 ∈ ℕ ↔ 𝑚 ∈
(ℤ≥‘1)) |
26 | | isummolem3.g |
. . . . . . 7
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) |
27 | | breq1 3878 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑛 ≤ 𝑀 ↔ 𝑚 ≤ 𝑀)) |
28 | | fveq2 5353 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚)) |
29 | 28 | csbeq1d 2961 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
30 | 27, 29 | ifbieq1d 3441 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑚 ≤ 𝑀, ⦋(𝑓‘𝑚) / 𝑘⦌𝐵, 0)) |
31 | | simplr 500 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → 𝑚 ∈ ℕ) |
32 | | elfzle2 9649 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (1...𝑀) → 𝑚 ≤ 𝑀) |
33 | 32 | adantl 273 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → 𝑚 ≤ 𝑀) |
34 | 33 | iftrued 3428 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → if(𝑚 ≤ 𝑀, ⦋(𝑓‘𝑚) / 𝑘⦌𝐵, 0) = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
35 | | f1of 5301 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...𝑀)–1-1-onto→𝐴 → 𝑓:(1...𝑀)⟶𝐴) |
36 | 11, 35 | syl 14 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑓:(1...𝑀)⟶𝐴) |
37 | 36 | ffvelrnda 5487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝑓‘𝑚) ∈ 𝐴) |
38 | 18 | ralrimiva 2464 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
39 | 38 | adantr 272 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
40 | | nfcsb1v 2985 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 |
41 | 40 | nfel1 2251 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ |
42 | | csbeq1a 2963 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑓‘𝑚) → 𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
43 | 42 | eleq1d 2168 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑓‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
44 | 41, 43 | rspc 2738 |
. . . . . . . . . 10
⊢ ((𝑓‘𝑚) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
45 | 37, 39, 44 | sylc 62 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) |
46 | 45 | adantlr 464 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) |
47 | 34, 46 | eqeltrd 2176 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → if(𝑚 ≤ 𝑀, ⦋(𝑓‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ) |
48 | 26, 30, 31, 47 | fvmptd3 5446 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → (𝐺‘𝑚) = if(𝑚 ≤ 𝑀, ⦋(𝑓‘𝑚) / 𝑘⦌𝐵, 0)) |
49 | 48, 47 | eqeltrd 2176 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → (𝐺‘𝑚) ∈ ℂ) |
50 | | simplr 500 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑚 ∈
ℕ) |
51 | 8 | ad2antrr 475 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℕ) |
52 | 51 | nnzd 9024 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℤ) |
53 | | eluzp1l 9200 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑚 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑚) |
54 | 52, 53 | sylancom 414 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑚) |
55 | 50 | nnzd 9024 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑚 ∈
ℤ) |
56 | | zltnle 8952 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀 < 𝑚 ↔ ¬ 𝑚 ≤ 𝑀)) |
57 | 52, 55, 56 | syl2anc 406 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑀 < 𝑚 ↔ ¬ 𝑚 ≤ 𝑀)) |
58 | 54, 57 | mpbid 146 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → ¬ 𝑚 ≤ 𝑀) |
59 | 58 | iffalsed 3431 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → if(𝑚 ≤ 𝑀, ⦋(𝑓‘𝑚) / 𝑘⦌𝐵, 0) = 0) |
60 | | 0cn 7630 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
61 | 59, 60 | syl6eqel 2190 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → if(𝑚 ≤ 𝑀, ⦋(𝑓‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ) |
62 | 26, 30, 50, 61 | fvmptd3 5446 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐺‘𝑚) = if(𝑚 ≤ 𝑀, ⦋(𝑓‘𝑚) / 𝑘⦌𝐵, 0)) |
63 | 62, 61 | eqeltrd 2176 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐺‘𝑚) ∈ ℂ) |
64 | | nnsplit 9755 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ℕ =
((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) |
65 | 8, 64 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → ℕ = ((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) |
66 | 65 | eleq2d 2169 |
. . . . . . 7
⊢ (𝜑 → (𝑚 ∈ ℕ ↔ 𝑚 ∈ ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1))))) |
67 | 66 | biimpa 292 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1)))) |
68 | | elun 3164 |
. . . . . 6
⊢ (𝑚 ∈ ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1))) ↔ (𝑚 ∈ (1...𝑀) ∨ 𝑚 ∈ (ℤ≥‘(𝑀 + 1)))) |
69 | 67, 68 | sylib 121 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 ∈ (1...𝑀) ∨ 𝑚 ∈ (ℤ≥‘(𝑀 + 1)))) |
70 | 49, 63, 69 | mpjaodan 753 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚) ∈ ℂ) |
71 | 25, 70 | sylan2br 284 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ (𝐺‘𝑚) ∈
ℂ) |
72 | 19 | oveq2d 5722 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝑁) = (1...𝑀)) |
73 | 72 | eleq2d 2169 |
. . . . . . . 8
⊢ (𝜑 → (𝑚 ∈ (1...𝑁) ↔ 𝑚 ∈ (1...𝑀))) |
74 | 73 | adantr 272 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 ∈ (1...𝑁) ↔ 𝑚 ∈ (1...𝑀))) |
75 | 74 | pm5.32i 445 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) ↔ ((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀))) |
76 | | isummolem3.4 |
. . . . . . . 8
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0)) |
77 | | breq1 3878 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝑛 ≤ 𝑁 ↔ 𝑚 ≤ 𝑁)) |
78 | | fveq2 5353 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (𝐾‘𝑛) = (𝐾‘𝑚)) |
79 | 78 | csbeq1d 2961 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵) |
80 | 77, 79 | ifbieq1d 3441 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0)) |
81 | | simplr 500 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → 𝑚 ∈ ℕ) |
82 | | elfzle2 9649 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (1...𝑁) → 𝑚 ≤ 𝑁) |
83 | 82 | adantl 273 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → 𝑚 ≤ 𝑁) |
84 | 83 | iftrued 3428 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵) |
85 | | f1of 5301 |
. . . . . . . . . . . . 13
⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → 𝐾:(1...𝑁)⟶𝐴) |
86 | 14, 85 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾:(1...𝑁)⟶𝐴) |
87 | 86 | ffvelrnda 5487 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑁)) → (𝐾‘𝑚) ∈ 𝐴) |
88 | 38 | adantr 272 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑁)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
89 | | nfcsb1v 2985 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵 |
90 | 89 | nfel1 2251 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ |
91 | | csbeq1a 2963 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝐾‘𝑚) → 𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵) |
92 | 91 | eleq1d 2168 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝐾‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
93 | 90, 92 | rspc 2738 |
. . . . . . . . . . 11
⊢ ((𝐾‘𝑚) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
94 | 87, 88, 93 | sylc 62 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑁)) → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) |
95 | 94 | adantlr 464 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) |
96 | 84, 95 | eqeltrd 2176 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ) |
97 | 76, 80, 81, 96 | fvmptd3 5446 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐻‘𝑚) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0)) |
98 | 97, 96 | eqeltrd 2176 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐻‘𝑚) ∈ ℂ) |
99 | 75, 98 | sylbir 134 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → (𝐻‘𝑚) ∈ ℂ) |
100 | 19 | breq2d 3887 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑚 ≤ 𝑁 ↔ 𝑚 ≤ 𝑀)) |
101 | 100 | notbid 633 |
. . . . . . . . . . 11
⊢ (𝜑 → (¬ 𝑚 ≤ 𝑁 ↔ ¬ 𝑚 ≤ 𝑀)) |
102 | 101 | ad2antrr 475 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → (¬ 𝑚 ≤ 𝑁 ↔ ¬ 𝑚 ≤ 𝑀)) |
103 | 58, 102 | mpbird 166 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → ¬ 𝑚 ≤ 𝑁) |
104 | 103 | iffalsed 3431 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) = 0) |
105 | 104, 60 | syl6eqel 2190 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ) |
106 | 76, 80, 50, 105 | fvmptd3 5446 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐻‘𝑚) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0)) |
107 | 106, 105 | eqeltrd 2176 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐻‘𝑚) ∈ ℂ) |
108 | 99, 107, 69 | mpjaodan 753 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘𝑚) ∈ ℂ) |
109 | 25, 108 | sylan2br 284 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1))
→ (𝐻‘𝑚) ∈
ℂ) |
110 | | f1oeq2 5293 |
. . . . . . . . . . 11
⊢
((1...𝑀) =
(1...𝑁) → (𝐾:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐾:(1...𝑁)–1-1-onto→𝐴)) |
111 | 21, 110 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐾:(1...𝑁)–1-1-onto→𝐴)) |
112 | 14, 111 | mpbird 166 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾:(1...𝑀)–1-1-onto→𝐴) |
113 | | f1of 5301 |
. . . . . . . . 9
⊢ (𝐾:(1...𝑀)–1-1-onto→𝐴 → 𝐾:(1...𝑀)⟶𝐴) |
114 | 112, 113 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → 𝐾:(1...𝑀)⟶𝐴) |
115 | | fvco3 5424 |
. . . . . . . 8
⊢ ((𝐾:(1...𝑀)⟶𝐴 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖))) |
116 | 114, 115 | sylan 279 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖))) |
117 | 116 | fveq2d 5357 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) = (𝑓‘(◡𝑓‘(𝐾‘𝑖)))) |
118 | 11 | adantr 272 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑓:(1...𝑀)–1-1-onto→𝐴) |
119 | 114 | ffvelrnda 5487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) ∈ 𝐴) |
120 | | f1ocnvfv2 5611 |
. . . . . . 7
⊢ ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (𝐾‘𝑖) ∈ 𝐴) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖)) |
121 | 118, 119,
120 | syl2anc 406 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖)) |
122 | 117, 121 | eqtr2d 2133 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) = (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖))) |
123 | 122 | csbeq1d 2961 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ⦋(𝐾‘𝑖) / 𝑘⦌𝐵 = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵) |
124 | | elfznn 9675 |
. . . . . 6
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ) |
125 | | elfzle2 9649 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ≤ 𝑀) |
126 | 125 | adantl 273 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ≤ 𝑀) |
127 | 20 | breq2d 3887 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑖 ≤ 𝑀 ↔ 𝑖 ≤ 𝑁)) |
128 | 127 | adantr 272 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑖 ≤ 𝑀 ↔ 𝑖 ≤ 𝑁)) |
129 | 126, 128 | mpbid 146 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ≤ 𝑁) |
130 | 129 | iftrued 3428 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → if(𝑖 ≤ 𝑁, ⦋(𝐾‘𝑖) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵) |
131 | 38 | adantr 272 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
132 | | nfcsb1v 2985 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋(𝐾‘𝑖) / 𝑘⦌𝐵 |
133 | 132 | nfel1 2251 |
. . . . . . . . 9
⊢
Ⅎ𝑘⦋(𝐾‘𝑖) / 𝑘⦌𝐵 ∈ ℂ |
134 | | csbeq1a 2963 |
. . . . . . . . . 10
⊢ (𝑘 = (𝐾‘𝑖) → 𝐵 = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵) |
135 | 134 | eleq1d 2168 |
. . . . . . . . 9
⊢ (𝑘 = (𝐾‘𝑖) → (𝐵 ∈ ℂ ↔ ⦋(𝐾‘𝑖) / 𝑘⦌𝐵 ∈ ℂ)) |
136 | 133, 135 | rspc 2738 |
. . . . . . . 8
⊢ ((𝐾‘𝑖) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐾‘𝑖) / 𝑘⦌𝐵 ∈ ℂ)) |
137 | 119, 131,
136 | sylc 62 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ⦋(𝐾‘𝑖) / 𝑘⦌𝐵 ∈ ℂ) |
138 | 130, 137 | eqeltrd 2176 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → if(𝑖 ≤ 𝑁, ⦋(𝐾‘𝑖) / 𝑘⦌𝐵, 0) ∈ ℂ) |
139 | | breq1 3878 |
. . . . . . . 8
⊢ (𝑛 = 𝑖 → (𝑛 ≤ 𝑁 ↔ 𝑖 ≤ 𝑁)) |
140 | | fveq2 5353 |
. . . . . . . . 9
⊢ (𝑛 = 𝑖 → (𝐾‘𝑛) = (𝐾‘𝑖)) |
141 | 140 | csbeq1d 2961 |
. . . . . . . 8
⊢ (𝑛 = 𝑖 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵) |
142 | 139, 141 | ifbieq1d 3441 |
. . . . . . 7
⊢ (𝑛 = 𝑖 → if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑖 ≤ 𝑁, ⦋(𝐾‘𝑖) / 𝑘⦌𝐵, 0)) |
143 | 142, 76 | fvmptg 5429 |
. . . . . 6
⊢ ((𝑖 ∈ ℕ ∧ if(𝑖 ≤ 𝑁, ⦋(𝐾‘𝑖) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐻‘𝑖) = if(𝑖 ≤ 𝑁, ⦋(𝐾‘𝑖) / 𝑘⦌𝐵, 0)) |
144 | 124, 138,
143 | syl2an2 564 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = if(𝑖 ≤ 𝑁, ⦋(𝐾‘𝑖) / 𝑘⦌𝐵, 0)) |
145 | 144, 130 | eqtrd 2132 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵) |
146 | | breq1 3878 |
. . . . . . 7
⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → (𝑛 ≤ 𝑀 ↔ ((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀)) |
147 | | fveq2 5353 |
. . . . . . . 8
⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → (𝑓‘𝑛) = (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖))) |
148 | 147 | csbeq1d 2961 |
. . . . . . 7
⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵) |
149 | 146, 148 | ifbieq1d 3441 |
. . . . . 6
⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀, ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵, 0)) |
150 | | f1of 5301 |
. . . . . . . . 9
⊢ ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀)) |
151 | 24, 150 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀)) |
152 | 151 | ffvelrnda 5487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀)) |
153 | | elfznn 9675 |
. . . . . . 7
⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ) |
154 | 152, 153 | syl 14 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ) |
155 | | elfzle2 9649 |
. . . . . . . . . 10
⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀) → ((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀) |
156 | 152, 155 | syl 14 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀) |
157 | 156 | iftrued 3428 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → if(((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀, ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵, 0) = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵) |
158 | 157, 123 | eqtr4d 2135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → if(((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀, ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵) |
159 | 158, 137 | eqeltrd 2176 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → if(((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀, ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵, 0) ∈ ℂ) |
160 | 26, 149, 154, 159 | fvmptd3 5446 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = if(((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀, ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵, 0)) |
161 | 160, 157 | eqtrd 2132 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵) |
162 | 123, 145,
161 | 3eqtr4d 2142 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖))) |
163 | 2, 4, 6, 10, 24, 71, 109, 162 | seq3f1o 10118 |
. 2
⊢ (𝜑 → (seq1( + , 𝐻)‘𝑀) = (seq1( + , 𝐺)‘𝑀)) |
164 | 20 | fveq2d 5357 |
. 2
⊢ (𝜑 → (seq1( + , 𝐻)‘𝑀) = (seq1( + , 𝐻)‘𝑁)) |
165 | 163, 164 | eqtr3d 2134 |
1
⊢ (𝜑 → (seq1( + , 𝐺)‘𝑀) = (seq1( + , 𝐻)‘𝑁)) |