Step | Hyp | Ref
| Expression |
1 | | addcl 10306 |
. . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 + 𝑗) ∈ ℂ) |
2 | 1 | adantl 474 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 + 𝑗) ∈ ℂ) |
3 | | addcom 10512 |
. . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 + 𝑗) = (𝑗 + 𝑚)) |
4 | 3 | adantl 474 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 + 𝑗) = (𝑗 + 𝑚)) |
5 | | addass 10311 |
. . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑚 + 𝑗) + 𝑦) = (𝑚 + (𝑗 + 𝑦))) |
6 | 5 | adantl 474 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝑚 + 𝑗) + 𝑦) = (𝑚 + (𝑗 + 𝑦))) |
7 | | summolem3.5 |
. . . . 5
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) |
8 | 7 | simpld 489 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) |
9 | | nnuz 11967 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
10 | 8, 9 | syl6eleq 2888 |
. . 3
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
11 | | ssidd 3820 |
. . 3
⊢ (𝜑 → ℂ ⊆
ℂ) |
12 | | summolem3.6 |
. . . . . 6
⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴) |
13 | | f1ocnv 6368 |
. . . . . 6
⊢ (𝑓:(1...𝑀)–1-1-onto→𝐴 → ◡𝑓:𝐴–1-1-onto→(1...𝑀)) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ (𝜑 → ◡𝑓:𝐴–1-1-onto→(1...𝑀)) |
15 | | summolem3.7 |
. . . . 5
⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴) |
16 | | f1oco 6378 |
. . . . 5
⊢ ((◡𝑓:𝐴–1-1-onto→(1...𝑀) ∧ 𝐾:(1...𝑁)–1-1-onto→𝐴) → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀)) |
17 | 14, 15, 16 | syl2anc 580 |
. . . 4
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀)) |
18 | | ovex 6910 |
. . . . . . . . . 10
⊢
(1...𝑁) ∈
V |
19 | 18 | f1oen 8216 |
. . . . . . . . 9
⊢ ((◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀) → (1...𝑁) ≈ (1...𝑀)) |
20 | 17, 19 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (1...𝑁) ≈ (1...𝑀)) |
21 | | fzfi 13026 |
. . . . . . . . 9
⊢
(1...𝑁) ∈
Fin |
22 | | fzfi 13026 |
. . . . . . . . 9
⊢
(1...𝑀) ∈
Fin |
23 | | hashen 13387 |
. . . . . . . . 9
⊢
(((1...𝑁) ∈ Fin
∧ (1...𝑀) ∈ Fin)
→ ((♯‘(1...𝑁)) = (♯‘(1...𝑀)) ↔ (1...𝑁) ≈ (1...𝑀))) |
24 | 21, 22, 23 | mp2an 684 |
. . . . . . . 8
⊢
((♯‘(1...𝑁)) = (♯‘(1...𝑀)) ↔ (1...𝑁) ≈ (1...𝑀)) |
25 | 20, 24 | sylibr 226 |
. . . . . . 7
⊢ (𝜑 → (♯‘(1...𝑁)) = (♯‘(1...𝑀))) |
26 | 7 | simprd 490 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
27 | | nnnn0 11588 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
28 | | hashfz1 13386 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (♯‘(1...𝑁)) = 𝑁) |
29 | 26, 27, 28 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁) |
30 | | nnnn0 11588 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
31 | | hashfz1 13386 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ (♯‘(1...𝑀)) = 𝑀) |
32 | 8, 30, 31 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀) |
33 | 25, 29, 32 | 3eqtr3rd 2842 |
. . . . . 6
⊢ (𝜑 → 𝑀 = 𝑁) |
34 | 33 | oveq2d 6894 |
. . . . 5
⊢ (𝜑 → (1...𝑀) = (1...𝑁)) |
35 | 34 | f1oeq2d 6352 |
. . . 4
⊢ (𝜑 → ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) ↔ (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀))) |
36 | 17, 35 | mpbird 249 |
. . 3
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀)) |
37 | | elfznn 12624 |
. . . . . 6
⊢ (𝑚 ∈ (1...𝑀) → 𝑚 ∈ ℕ) |
38 | 37 | adantl 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → 𝑚 ∈ ℕ) |
39 | | f1of 6356 |
. . . . . . . 8
⊢ (𝑓:(1...𝑀)–1-1-onto→𝐴 → 𝑓:(1...𝑀)⟶𝐴) |
40 | 12, 39 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑓:(1...𝑀)⟶𝐴) |
41 | 40 | ffvelrnda 6585 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝑓‘𝑚) ∈ 𝐴) |
42 | | summo.2 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
43 | 42 | ralrimiva 3147 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
44 | 43 | adantr 473 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
45 | | nfcsb1v 3744 |
. . . . . . . 8
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 |
46 | 45 | nfel1 2956 |
. . . . . . 7
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ |
47 | | csbeq1a 3737 |
. . . . . . . 8
⊢ (𝑘 = (𝑓‘𝑚) → 𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
48 | 47 | eleq1d 2863 |
. . . . . . 7
⊢ (𝑘 = (𝑓‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
49 | 46, 48 | rspc 3491 |
. . . . . 6
⊢ ((𝑓‘𝑚) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
50 | 41, 44, 49 | sylc 65 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) |
51 | | fveq2 6411 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚)) |
52 | 51 | csbeq1d 3735 |
. . . . . 6
⊢ (𝑛 = 𝑚 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
53 | | summo.3 |
. . . . . 6
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) |
54 | 52, 53 | fvmptg 6505 |
. . . . 5
⊢ ((𝑚 ∈ ℕ ∧
⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) → (𝐺‘𝑚) = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
55 | 38, 50, 54 | syl2anc 580 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝐺‘𝑚) = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
56 | 55, 50 | eqeltrd 2878 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝐺‘𝑚) ∈ ℂ) |
57 | 34 | f1oeq2d 6352 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐾:(1...𝑁)–1-1-onto→𝐴)) |
58 | 15, 57 | mpbird 249 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾:(1...𝑀)–1-1-onto→𝐴) |
59 | | f1of 6356 |
. . . . . . . . . 10
⊢ (𝐾:(1...𝑀)–1-1-onto→𝐴 → 𝐾:(1...𝑀)⟶𝐴) |
60 | 58, 59 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾:(1...𝑀)⟶𝐴) |
61 | | fvco3 6500 |
. . . . . . . . 9
⊢ ((𝐾:(1...𝑀)⟶𝐴 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖))) |
62 | 60, 61 | sylan 576 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖))) |
63 | 62 | fveq2d 6415 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) = (𝑓‘(◡𝑓‘(𝐾‘𝑖)))) |
64 | 12 | adantr 473 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑓:(1...𝑀)–1-1-onto→𝐴) |
65 | 60 | ffvelrnda 6585 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) ∈ 𝐴) |
66 | | f1ocnvfv2 6761 |
. . . . . . . 8
⊢ ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (𝐾‘𝑖) ∈ 𝐴) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖)) |
67 | 64, 65, 66 | syl2anc 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖)) |
68 | 63, 67 | eqtr2d 2834 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) = (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖))) |
69 | 68 | csbeq1d 3735 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ⦋(𝐾‘𝑖) / 𝑘⦌𝐵 = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵) |
70 | 69 | fveq2d 6415 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵) = ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)) |
71 | | elfznn 12624 |
. . . . . 6
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ) |
72 | 71 | adantl 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ ℕ) |
73 | | fveq2 6411 |
. . . . . . 7
⊢ (𝑛 = 𝑖 → (𝐾‘𝑛) = (𝐾‘𝑖)) |
74 | 73 | csbeq1d 3735 |
. . . . . 6
⊢ (𝑛 = 𝑖 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵) |
75 | | summolem3.4 |
. . . . . 6
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⦋(𝐾‘𝑛) / 𝑘⦌𝐵) |
76 | 74, 75 | fvmpti 6506 |
. . . . 5
⊢ (𝑖 ∈ ℕ → (𝐻‘𝑖) = ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵)) |
77 | 72, 76 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵)) |
78 | | f1of 6356 |
. . . . . . 7
⊢ ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀)) |
79 | 36, 78 | syl 17 |
. . . . . 6
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀)) |
80 | 79 | ffvelrnda 6585 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀)) |
81 | | elfznn 12624 |
. . . . 5
⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ) |
82 | | fveq2 6411 |
. . . . . . 7
⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → (𝑓‘𝑛) = (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖))) |
83 | 82 | csbeq1d 3735 |
. . . . . 6
⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵) |
84 | 83, 53 | fvmpti 6506 |
. . . . 5
⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)) |
85 | 80, 81, 84 | 3syl 18 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)) |
86 | 70, 77, 85 | 3eqtr4d 2843 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖))) |
87 | 2, 4, 6, 10, 11, 36, 56, 86 | seqf1o 13096 |
. 2
⊢ (𝜑 → (seq1( + , 𝐻)‘𝑀) = (seq1( + , 𝐺)‘𝑀)) |
88 | 33 | fveq2d 6415 |
. 2
⊢ (𝜑 → (seq1( + , 𝐻)‘𝑀) = (seq1( + , 𝐻)‘𝑁)) |
89 | 87, 88 | eqtr3d 2835 |
1
⊢ (𝜑 → (seq1( + , 𝐺)‘𝑀) = (seq1( + , 𝐻)‘𝑁)) |