Step | Hyp | Ref
| Expression |
1 | | addcl 10698 |
. . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 + 𝑗) ∈ ℂ) |
2 | 1 | adantl 485 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 + 𝑗) ∈ ℂ) |
3 | | addcom 10905 |
. . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 + 𝑗) = (𝑗 + 𝑚)) |
4 | 3 | adantl 485 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 + 𝑗) = (𝑗 + 𝑚)) |
5 | | addass 10703 |
. . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑚 + 𝑗) + 𝑦) = (𝑚 + (𝑗 + 𝑦))) |
6 | 5 | adantl 485 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝑚 + 𝑗) + 𝑦) = (𝑚 + (𝑗 + 𝑦))) |
7 | | summolem3.5 |
. . . . 5
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) |
8 | 7 | simpld 498 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) |
9 | | nnuz 12364 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
10 | 8, 9 | eleqtrdi 2843 |
. . 3
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
11 | | ssidd 3901 |
. . 3
⊢ (𝜑 → ℂ ⊆
ℂ) |
12 | | summolem3.6 |
. . . . . 6
⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴) |
13 | | f1ocnv 6631 |
. . . . . 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 6641 |
. . . . 5
⊢ ((◡𝑓:𝐴–1-1-onto→(1...𝑀) ∧ 𝐾:(1...𝑁)–1-1-onto→𝐴) → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀)) |
17 | 14, 15, 16 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀)) |
18 | | ovex 7204 |
. . . . . . . . . 10
⊢
(1...𝑁) ∈
V |
19 | 18 | f1oen 8577 |
. . . . . . . . 9
⊢ ((◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀) → (1...𝑁) ≈ (1...𝑀)) |
20 | 17, 19 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (1...𝑁) ≈ (1...𝑀)) |
21 | | fzfi 13432 |
. . . . . . . . 9
⊢
(1...𝑁) ∈
Fin |
22 | | fzfi 13432 |
. . . . . . . . 9
⊢
(1...𝑀) ∈
Fin |
23 | | hashen 13800 |
. . . . . . . . 9
⊢
(((1...𝑁) ∈ Fin
∧ (1...𝑀) ∈ Fin)
→ ((♯‘(1...𝑁)) = (♯‘(1...𝑀)) ↔ (1...𝑁) ≈ (1...𝑀))) |
24 | 21, 22, 23 | mp2an 692 |
. . . . . . . 8
⊢
((♯‘(1...𝑁)) = (♯‘(1...𝑀)) ↔ (1...𝑁) ≈ (1...𝑀)) |
25 | 20, 24 | sylibr 237 |
. . . . . . 7
⊢ (𝜑 → (♯‘(1...𝑁)) = (♯‘(1...𝑀))) |
26 | 7 | simprd 499 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
27 | | nnnn0 11984 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
28 | | hashfz1 13799 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (♯‘(1...𝑁)) = 𝑁) |
29 | 26, 27, 28 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁) |
30 | | nnnn0 11984 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
31 | | hashfz1 13799 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ (♯‘(1...𝑀)) = 𝑀) |
32 | 8, 30, 31 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀) |
33 | 25, 29, 32 | 3eqtr3rd 2782 |
. . . . . 6
⊢ (𝜑 → 𝑀 = 𝑁) |
34 | 33 | oveq2d 7187 |
. . . . 5
⊢ (𝜑 → (1...𝑀) = (1...𝑁)) |
35 | 34 | f1oeq2d 6615 |
. . . 4
⊢ (𝜑 → ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) ↔ (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀))) |
36 | 17, 35 | mpbird 260 |
. . 3
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀)) |
37 | | summo.3 |
. . . . 5
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) |
38 | | fveq2 6675 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚)) |
39 | 38 | csbeq1d 3795 |
. . . . 5
⊢ (𝑛 = 𝑚 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
40 | | elfznn 13028 |
. . . . . 6
⊢ (𝑚 ∈ (1...𝑀) → 𝑚 ∈ ℕ) |
41 | 40 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → 𝑚 ∈ ℕ) |
42 | | f1of 6619 |
. . . . . . . 8
⊢ (𝑓:(1...𝑀)–1-1-onto→𝐴 → 𝑓:(1...𝑀)⟶𝐴) |
43 | 12, 42 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑓:(1...𝑀)⟶𝐴) |
44 | 43 | ffvelrnda 6862 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝑓‘𝑚) ∈ 𝐴) |
45 | | summo.2 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
46 | 45 | ralrimiva 3096 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
47 | 46 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
48 | | nfcsb1v 3815 |
. . . . . . . 8
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 |
49 | 48 | nfel1 2915 |
. . . . . . 7
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ |
50 | | csbeq1a 3805 |
. . . . . . . 8
⊢ (𝑘 = (𝑓‘𝑚) → 𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
51 | 50 | eleq1d 2817 |
. . . . . . 7
⊢ (𝑘 = (𝑓‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
52 | 49, 51 | rspc 3515 |
. . . . . 6
⊢ ((𝑓‘𝑚) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) |
53 | 44, 47, 52 | sylc 65 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) |
54 | 37, 39, 41, 53 | fvmptd3 6799 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝐺‘𝑚) = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) |
55 | 54, 53 | eqeltrd 2833 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝐺‘𝑚) ∈ ℂ) |
56 | 34 | f1oeq2d 6615 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐾:(1...𝑁)–1-1-onto→𝐴)) |
57 | 15, 56 | mpbird 260 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾:(1...𝑀)–1-1-onto→𝐴) |
58 | | f1of 6619 |
. . . . . . . . . 10
⊢ (𝐾:(1...𝑀)–1-1-onto→𝐴 → 𝐾:(1...𝑀)⟶𝐴) |
59 | 57, 58 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾:(1...𝑀)⟶𝐴) |
60 | | fvco3 6768 |
. . . . . . . . 9
⊢ ((𝐾:(1...𝑀)⟶𝐴 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖))) |
61 | 59, 60 | sylan 583 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖))) |
62 | 61 | fveq2d 6679 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) = (𝑓‘(◡𝑓‘(𝐾‘𝑖)))) |
63 | 12 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑓:(1...𝑀)–1-1-onto→𝐴) |
64 | 59 | ffvelrnda 6862 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) ∈ 𝐴) |
65 | | f1ocnvfv2 7046 |
. . . . . . . 8
⊢ ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (𝐾‘𝑖) ∈ 𝐴) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖)) |
66 | 63, 64, 65 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖)) |
67 | 62, 66 | eqtr2d 2774 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) = (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖))) |
68 | 67 | csbeq1d 3795 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ⦋(𝐾‘𝑖) / 𝑘⦌𝐵 = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵) |
69 | 68 | fveq2d 6679 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵) = ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)) |
70 | | elfznn 13028 |
. . . . . 6
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ) |
71 | 70 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ ℕ) |
72 | | fveq2 6675 |
. . . . . . 7
⊢ (𝑛 = 𝑖 → (𝐾‘𝑛) = (𝐾‘𝑖)) |
73 | 72 | csbeq1d 3795 |
. . . . . 6
⊢ (𝑛 = 𝑖 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵) |
74 | | summolem3.4 |
. . . . . 6
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⦋(𝐾‘𝑛) / 𝑘⦌𝐵) |
75 | 73, 74 | fvmpti 6775 |
. . . . 5
⊢ (𝑖 ∈ ℕ → (𝐻‘𝑖) = ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵)) |
76 | 71, 75 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵)) |
77 | | f1of 6619 |
. . . . . . 7
⊢ ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀)) |
78 | 36, 77 | syl 17 |
. . . . . 6
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀)) |
79 | 78 | ffvelrnda 6862 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀)) |
80 | | elfznn 13028 |
. . . . 5
⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ) |
81 | | fveq2 6675 |
. . . . . . 7
⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → (𝑓‘𝑛) = (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖))) |
82 | 81 | csbeq1d 3795 |
. . . . . 6
⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵) |
83 | 82, 37 | fvmpti 6775 |
. . . . 5
⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)) |
84 | 79, 80, 83 | 3syl 18 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)) |
85 | 69, 76, 84 | 3eqtr4d 2783 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖))) |
86 | 2, 4, 6, 10, 11, 36, 55, 85 | seqf1o 13504 |
. 2
⊢ (𝜑 → (seq1( + , 𝐻)‘𝑀) = (seq1( + , 𝐺)‘𝑀)) |
87 | 33 | fveq2d 6679 |
. 2
⊢ (𝜑 → (seq1( + , 𝐻)‘𝑀) = (seq1( + , 𝐻)‘𝑁)) |
88 | 86, 87 | eqtr3d 2775 |
1
⊢ (𝜑 → (seq1( + , 𝐺)‘𝑀) = (seq1( + , 𝐻)‘𝑁)) |