Step | Hyp | Ref
| Expression |
1 | | addcl 9897 |
. . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 + 𝑗) ∈ ℂ) |
2 | 1 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 + 𝑗) ∈ ℂ) |
3 | | addcom 10101 |
. . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 + 𝑗) = (𝑗 + 𝑚)) |
4 | 3 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 + 𝑗) = (𝑗 + 𝑚)) |
5 | | addass 9902 |
. . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑚 + 𝑗) + 𝑦) = (𝑚 + (𝑗 + 𝑦))) |
6 | 5 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝑚 + 𝑗) + 𝑦) = (𝑚 + (𝑗 + 𝑦))) |
7 | | summolem3.5 |
. . . . 5
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) |
8 | 7 | simpld 474 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) |
9 | | nnuz 11599 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
10 | 8, 9 | syl6eleq 2698 |
. . 3
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
11 | | ssid 3587 |
. . . 4
⊢ ℂ
⊆ ℂ |
12 | 11 | a1i 11 |
. . 3
⊢ (𝜑 → ℂ ⊆
ℂ) |
13 | | summolem3.6 |
. . . . . 6
⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴) |
14 | | f1ocnv 6062 |
. . . . . 6
⊢ (𝑓:(1...𝑀)–1-1-onto→𝐴 → ◡𝑓:𝐴–1-1-onto→(1...𝑀)) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ (𝜑 → ◡𝑓:𝐴–1-1-onto→(1...𝑀)) |
16 | | summolem3.7 |
. . . . 5
⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴) |
17 | | f1oco 6072 |
. . . . 5
⊢ ((◡𝑓:𝐴–1-1-onto→(1...𝑀) ∧ 𝐾:(1...𝑁)–1-1-onto→𝐴) → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀)) |
18 | 15, 16, 17 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀)) |
19 | | ovex 6577 |
. . . . . . . . . 10
⊢
(1...𝑁) ∈
V |
20 | 19 | f1oen 7862 |
. . . . . . . . 9
⊢ ((◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀) → (1...𝑁) ≈ (1...𝑀)) |
21 | 18, 20 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (1...𝑁) ≈ (1...𝑀)) |
22 | | fzfi 12633 |
. . . . . . . . 9
⊢
(1...𝑁) ∈
Fin |
23 | | fzfi 12633 |
. . . . . . . . 9
⊢
(1...𝑀) ∈
Fin |
24 | | hashen 12997 |
. . . . . . . . 9
⊢
(((1...𝑁) ∈ Fin
∧ (1...𝑀) ∈ Fin)
→ ((#‘(1...𝑁)) =
(#‘(1...𝑀)) ↔
(1...𝑁) ≈ (1...𝑀))) |
25 | 22, 23, 24 | mp2an 704 |
. . . . . . . 8
⊢
((#‘(1...𝑁)) =
(#‘(1...𝑀)) ↔
(1...𝑁) ≈ (1...𝑀)) |
26 | 21, 25 | sylibr 223 |
. . . . . . 7
⊢ (𝜑 → (#‘(1...𝑁)) = (#‘(1...𝑀))) |
27 | 7 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
28 | | nnnn0 11176 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
29 | | hashfz1 12996 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (#‘(1...𝑁)) =
𝑁) |
30 | 27, 28, 29 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (#‘(1...𝑁)) = 𝑁) |
31 | | nnnn0 11176 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
32 | | hashfz1 12996 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ (#‘(1...𝑀)) =
𝑀) |
33 | 8, 31, 32 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (#‘(1...𝑀)) = 𝑀) |
34 | 26, 30, 33 | 3eqtr3rd 2653 |
. . . . . 6
⊢ (𝜑 → 𝑀 = 𝑁) |
35 | 34 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (1...𝑀) = (1...𝑁)) |
36 | | f1oeq2 6041 |
. . . . 5
⊢
((1...𝑀) =
(1...𝑁) → ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) ↔ (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀))) |
37 | 35, 36 | syl 17 |
. . . 4
⊢ (𝜑 → ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) ↔ (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀))) |
38 | 18, 37 | mpbird 246 |
. . 3
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀)) |
39 | | elfznn 12241 |
. . . . . 6
⊢ (𝑚 ∈ (1...𝑀) → 𝑚 ∈ ℕ) |
40 | 39 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → 𝑚 ∈ ℕ) |
41 | | f1of 6050 |
. . . . . . . 8
⊢ (𝑓:(1...𝑀)–1-1-onto→𝐴 → 𝑓:(1...𝑀)⟶𝐴) |
42 | 13, 41 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑓:(1...𝑀)⟶𝐴) |
43 | 42 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝑓‘𝑚) ∈ 𝐴) |
44 | | summo.2 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
45 | 44 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
46 | 45 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
47 | | nfcsb1v 3515 |
. . . . . . . 8
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 |
48 | 47 | nfel1 2765 |
. . . . . . 7
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ |
49 | | csbeq1a 3508 |
. . . . . . . 8
⊢ (𝑘 = (𝑓‘𝑚) → 𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
50 | 49 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑘 = (𝑓‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
51 | 48, 50 | rspc 3276 |
. . . . . 6
⊢ ((𝑓‘𝑚) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
52 | 43, 46, 51 | sylc 63 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) |
53 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚)) |
54 | 53 | csbeq1d 3506 |
. . . . . 6
⊢ (𝑛 = 𝑚 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
55 | | summo.3 |
. . . . . 6
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) |
56 | 54, 55 | fvmptg 6189 |
. . . . 5
⊢ ((𝑚 ∈ ℕ ∧
⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) → (𝐺‘𝑚) = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
57 | 40, 52, 56 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝐺‘𝑚) = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
58 | 57, 52 | eqeltrd 2688 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝐺‘𝑚) ∈ ℂ) |
59 | | f1oeq2 6041 |
. . . . . . . . . . . 12
⊢
((1...𝑀) =
(1...𝑁) → (𝐾:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐾:(1...𝑁)–1-1-onto→𝐴)) |
60 | 35, 59 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐾:(1...𝑁)–1-1-onto→𝐴)) |
61 | 16, 60 | mpbird 246 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾:(1...𝑀)–1-1-onto→𝐴) |
62 | | f1of 6050 |
. . . . . . . . . 10
⊢ (𝐾:(1...𝑀)–1-1-onto→𝐴 → 𝐾:(1...𝑀)⟶𝐴) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾:(1...𝑀)⟶𝐴) |
64 | | fvco3 6185 |
. . . . . . . . 9
⊢ ((𝐾:(1...𝑀)⟶𝐴 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖))) |
65 | 63, 64 | sylan 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖))) |
66 | 65 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) = (𝑓‘(◡𝑓‘(𝐾‘𝑖)))) |
67 | 13 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑓:(1...𝑀)–1-1-onto→𝐴) |
68 | 63 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) ∈ 𝐴) |
69 | | f1ocnvfv2 6433 |
. . . . . . . 8
⊢ ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (𝐾‘𝑖) ∈ 𝐴) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖)) |
70 | 67, 68, 69 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖)) |
71 | 66, 70 | eqtr2d 2645 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) = (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖))) |
72 | 71 | csbeq1d 3506 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ⦋(𝐾‘𝑖) / 𝑘⦌𝐵 = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵) |
73 | 72 | fveq2d 6107 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵) = ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)) |
74 | | elfznn 12241 |
. . . . . 6
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ) |
75 | 74 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ ℕ) |
76 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑛 = 𝑖 → (𝐾‘𝑛) = (𝐾‘𝑖)) |
77 | 76 | csbeq1d 3506 |
. . . . . 6
⊢ (𝑛 = 𝑖 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵) |
78 | | summolem3.4 |
. . . . . 6
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⦋(𝐾‘𝑛) / 𝑘⦌𝐵) |
79 | 77, 78 | fvmpti 6190 |
. . . . 5
⊢ (𝑖 ∈ ℕ → (𝐻‘𝑖) = ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵)) |
80 | 75, 79 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵)) |
81 | | f1of 6050 |
. . . . . . 7
⊢ ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀)) |
82 | 38, 81 | syl 17 |
. . . . . 6
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀)) |
83 | 82 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀)) |
84 | | elfznn 12241 |
. . . . 5
⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ) |
85 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → (𝑓‘𝑛) = (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖))) |
86 | 85 | csbeq1d 3506 |
. . . . . 6
⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵) |
87 | 86, 55 | fvmpti 6190 |
. . . . 5
⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)) |
88 | 83, 84, 87 | 3syl 18 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)) |
89 | 73, 80, 88 | 3eqtr4d 2654 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖))) |
90 | 2, 4, 6, 10, 12, 38, 58, 89 | seqf1o 12704 |
. 2
⊢ (𝜑 → (seq1( + , 𝐻)‘𝑀) = (seq1( + , 𝐺)‘𝑀)) |
91 | 34 | fveq2d 6107 |
. 2
⊢ (𝜑 → (seq1( + , 𝐻)‘𝑀) = (seq1( + , 𝐻)‘𝑁)) |
92 | 90, 91 | eqtr3d 2646 |
1
⊢ (𝜑 → (seq1( + , 𝐺)‘𝑀) = (seq1( + , 𝐻)‘𝑁)) |