| Step | Hyp | Ref
| Expression |
| 1 | | fzfid 14014 |
. . . . . 6
⊢ (𝜑 → (𝑀...𝑚) ∈ Fin) |
| 2 | | simpl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑚)) → 𝜑) |
| 3 | | elfzuz 13560 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝑀...𝑚) → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 4 | | fsumsermpt.z |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 5 | 3, 4 | eleqtrrdi 2852 |
. . . . . . . 8
⊢ (𝑘 ∈ (𝑀...𝑚) → 𝑘 ∈ 𝑍) |
| 6 | 5 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑚)) → 𝑘 ∈ 𝑍) |
| 7 | | fsumsermpt.a |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) |
| 8 | 2, 6, 7 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑚)) → 𝐴 ∈ ℂ) |
| 9 | 1, 8 | fsumcl 15769 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...𝑚)𝐴 ∈ ℂ) |
| 10 | 9 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → Σ𝑘 ∈ (𝑀...𝑚)𝐴 ∈ ℂ) |
| 11 | 10 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑚 ∈ 𝑍 Σ𝑘 ∈ (𝑀...𝑚)𝐴 ∈ ℂ) |
| 12 | | fsumsermpt.f |
. . . . 5
⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐴) |
| 13 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝑀...𝑛) = (𝑀...𝑚)) |
| 14 | 13 | sumeq1d 15736 |
. . . . . 6
⊢ (𝑛 = 𝑚 → Σ𝑘 ∈ (𝑀...𝑛)𝐴 = Σ𝑘 ∈ (𝑀...𝑚)𝐴) |
| 15 | 14 | cbvmptv 5255 |
. . . . 5
⊢ (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐴) = (𝑚 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑚)𝐴) |
| 16 | 12, 15 | eqtri 2765 |
. . . 4
⊢ 𝐹 = (𝑚 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑚)𝐴) |
| 17 | 16 | fnmpt 6708 |
. . 3
⊢
(∀𝑚 ∈
𝑍 Σ𝑘 ∈ (𝑀...𝑚)𝐴 ∈ ℂ → 𝐹 Fn 𝑍) |
| 18 | 11, 17 | syl 17 |
. 2
⊢ (𝜑 → 𝐹 Fn 𝑍) |
| 19 | | fsumsermpt.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 20 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝑍) |
| 21 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝑍) |
| 22 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘𝑗 |
| 23 | 22 | nfcsb1 3922 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐴 |
| 24 | 23 | nfel1 2922 |
. . . . . . . . 9
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐴 ∈ ℂ |
| 25 | 21, 24 | nfim 1896 |
. . . . . . . 8
⊢
Ⅎ𝑘((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐴 ∈ ℂ) |
| 26 | | eleq1w 2824 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍)) |
| 27 | 26 | anbi2d 630 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑘 ∈ 𝑍) ↔ (𝜑 ∧ 𝑗 ∈ 𝑍))) |
| 28 | | csbeq1a 3913 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → 𝐴 = ⦋𝑗 / 𝑘⦌𝐴) |
| 29 | 28 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → (𝐴 ∈ ℂ ↔ ⦋𝑗 / 𝑘⦌𝐴 ∈ ℂ)) |
| 30 | 27, 29 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) ↔ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐴 ∈ ℂ))) |
| 31 | 25, 30, 7 | chvarfv 2240 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ⦋𝑗 / 𝑘⦌𝐴 ∈ ℂ) |
| 32 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝑍 ↦ 𝐴) = (𝑘 ∈ 𝑍 ↦ 𝐴) |
| 33 | 22, 23, 28, 32 | fvmptf 7037 |
. . . . . . 7
⊢ ((𝑗 ∈ 𝑍 ∧ ⦋𝑗 / 𝑘⦌𝐴 ∈ ℂ) → ((𝑘 ∈ 𝑍 ↦ 𝐴)‘𝑗) = ⦋𝑗 / 𝑘⦌𝐴) |
| 34 | 20, 31, 33 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ 𝐴)‘𝑗) = ⦋𝑗 / 𝑘⦌𝐴) |
| 35 | 34, 31 | eqeltrd 2841 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ 𝐴)‘𝑗) ∈ ℂ) |
| 36 | | addcl 11237 |
. . . . . 6
⊢ ((𝑗 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑗 + 𝑥) ∈ ℂ) |
| 37 | 36 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑗 + 𝑥) ∈ ℂ) |
| 38 | 4, 19, 35, 37 | seqf 14064 |
. . . 4
⊢ (𝜑 → seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐴)):𝑍⟶ℂ) |
| 39 | 38 | ffnd 6737 |
. . 3
⊢ (𝜑 → seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐴)) Fn 𝑍) |
| 40 | | fsumsermpt.g |
. . . . 5
⊢ 𝐺 = seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐴)) |
| 41 | 40 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐺 = seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐴))) |
| 42 | 41 | fneq1d 6661 |
. . 3
⊢ (𝜑 → (𝐺 Fn 𝑍 ↔ seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐴)) Fn 𝑍)) |
| 43 | 39, 42 | mpbird 257 |
. 2
⊢ (𝜑 → 𝐺 Fn 𝑍) |
| 44 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ 𝑍) |
| 45 | 16 | fvmpt2 7027 |
. . . . 5
⊢ ((𝑚 ∈ 𝑍 ∧ Σ𝑘 ∈ (𝑀...𝑚)𝐴 ∈ ℂ) → (𝐹‘𝑚) = Σ𝑘 ∈ (𝑀...𝑚)𝐴) |
| 46 | 44, 10, 45 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) = Σ𝑘 ∈ (𝑀...𝑚)𝐴) |
| 47 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑗𝐴 |
| 48 | 28, 47, 23 | cbvsum 15731 |
. . . . 5
⊢
Σ𝑘 ∈
(𝑀...𝑚)𝐴 = Σ𝑗 ∈ (𝑀...𝑚)⦋𝑗 / 𝑘⦌𝐴 |
| 49 | 48 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → Σ𝑘 ∈ (𝑀...𝑚)𝐴 = Σ𝑗 ∈ (𝑀...𝑚)⦋𝑗 / 𝑘⦌𝐴) |
| 50 | 46, 49 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) = Σ𝑗 ∈ (𝑀...𝑚)⦋𝑗 / 𝑘⦌𝐴) |
| 51 | | simpl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑚)) → 𝜑) |
| 52 | | elfzuz 13560 |
. . . . . . . 8
⊢ (𝑗 ∈ (𝑀...𝑚) → 𝑗 ∈ (ℤ≥‘𝑀)) |
| 53 | 52, 4 | eleqtrrdi 2852 |
. . . . . . 7
⊢ (𝑗 ∈ (𝑀...𝑚) → 𝑗 ∈ 𝑍) |
| 54 | 53 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑚)) → 𝑗 ∈ 𝑍) |
| 55 | 51, 54, 34 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑚)) → ((𝑘 ∈ 𝑍 ↦ 𝐴)‘𝑗) = ⦋𝑗 / 𝑘⦌𝐴) |
| 56 | 55 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ 𝑍) ∧ 𝑗 ∈ (𝑀...𝑚)) → ((𝑘 ∈ 𝑍 ↦ 𝐴)‘𝑗) = ⦋𝑗 / 𝑘⦌𝐴) |
| 57 | | id 22 |
. . . . . 6
⊢ (𝑚 ∈ 𝑍 → 𝑚 ∈ 𝑍) |
| 58 | 57, 4 | eleqtrdi 2851 |
. . . . 5
⊢ (𝑚 ∈ 𝑍 → 𝑚 ∈ (ℤ≥‘𝑀)) |
| 59 | 58 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ (ℤ≥‘𝑀)) |
| 60 | 51, 54, 31 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑚)) → ⦋𝑗 / 𝑘⦌𝐴 ∈ ℂ) |
| 61 | 60 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ 𝑍) ∧ 𝑗 ∈ (𝑀...𝑚)) → ⦋𝑗 / 𝑘⦌𝐴 ∈ ℂ) |
| 62 | 56, 59, 61 | fsumser 15766 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → Σ𝑗 ∈ (𝑀...𝑚)⦋𝑗 / 𝑘⦌𝐴 = (seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐴))‘𝑚)) |
| 63 | 40 | fveq1i 6907 |
. . . . 5
⊢ (𝐺‘𝑚) = (seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐴))‘𝑚) |
| 64 | 63 | eqcomi 2746 |
. . . 4
⊢ (seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐴))‘𝑚) = (𝐺‘𝑚) |
| 65 | 64 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐴))‘𝑚) = (𝐺‘𝑚)) |
| 66 | 50, 62, 65 | 3eqtrd 2781 |
. 2
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) = (𝐺‘𝑚)) |
| 67 | 18, 43, 66 | eqfnfvd 7054 |
1
⊢ (𝜑 → 𝐹 = 𝐺) |