| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | addcl 11237 | . . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 + 𝑗) ∈ ℂ) | 
| 2 | 1 | adantl 481 | . . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 + 𝑗) ∈ ℂ) | 
| 3 |  | addcom 11447 | . . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 + 𝑗) = (𝑗 + 𝑚)) | 
| 4 | 3 | adantl 481 | . . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 + 𝑗) = (𝑗 + 𝑚)) | 
| 5 |  | addass 11242 | . . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑚 + 𝑗) + 𝑦) = (𝑚 + (𝑗 + 𝑦))) | 
| 6 | 5 | adantl 481 | . . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝑚 + 𝑗) + 𝑦) = (𝑚 + (𝑗 + 𝑦))) | 
| 7 |  | summolem3.5 | . . . . 5
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) | 
| 8 | 7 | simpld 494 | . . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 9 |  | nnuz 12921 | . . . 4
⊢ ℕ =
(ℤ≥‘1) | 
| 10 | 8, 9 | eleqtrdi 2851 | . . 3
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) | 
| 11 |  | ssidd 4007 | . . 3
⊢ (𝜑 → ℂ ⊆
ℂ) | 
| 12 |  | summolem3.6 | . . . . . 6
⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴) | 
| 13 |  | f1ocnv 6860 | . . . . . 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 6871 | . . . . 5
⊢ ((◡𝑓:𝐴–1-1-onto→(1...𝑀) ∧ 𝐾:(1...𝑁)–1-1-onto→𝐴) → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀)) | 
| 17 | 14, 15, 16 | syl2anc 584 | . . . 4
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀)) | 
| 18 |  | ovex 7464 | . . . . . . . . . 10
⊢
(1...𝑁) ∈
V | 
| 19 | 18 | f1oen 9013 | . . . . . . . . 9
⊢ ((◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀) → (1...𝑁) ≈ (1...𝑀)) | 
| 20 | 17, 19 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (1...𝑁) ≈ (1...𝑀)) | 
| 21 |  | fzfi 14013 | . . . . . . . . 9
⊢
(1...𝑁) ∈
Fin | 
| 22 |  | fzfi 14013 | . . . . . . . . 9
⊢
(1...𝑀) ∈
Fin | 
| 23 |  | hashen 14386 | . . . . . . . . 9
⊢
(((1...𝑁) ∈ Fin
∧ (1...𝑀) ∈ Fin)
→ ((♯‘(1...𝑁)) = (♯‘(1...𝑀)) ↔ (1...𝑁) ≈ (1...𝑀))) | 
| 24 | 21, 22, 23 | mp2an 692 | . . . . . . . 8
⊢
((♯‘(1...𝑁)) = (♯‘(1...𝑀)) ↔ (1...𝑁) ≈ (1...𝑀)) | 
| 25 | 20, 24 | sylibr 234 | . . . . . . 7
⊢ (𝜑 → (♯‘(1...𝑁)) = (♯‘(1...𝑀))) | 
| 26 | 7 | simprd 495 | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 27 |  | nnnn0 12533 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) | 
| 28 |  | hashfz1 14385 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (♯‘(1...𝑁)) = 𝑁) | 
| 29 | 26, 27, 28 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁) | 
| 30 |  | nnnn0 12533 | . . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) | 
| 31 |  | hashfz1 14385 | . . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ (♯‘(1...𝑀)) = 𝑀) | 
| 32 | 8, 30, 31 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀) | 
| 33 | 25, 29, 32 | 3eqtr3rd 2786 | . . . . . 6
⊢ (𝜑 → 𝑀 = 𝑁) | 
| 34 | 33 | oveq2d 7447 | . . . . 5
⊢ (𝜑 → (1...𝑀) = (1...𝑁)) | 
| 35 | 34 | f1oeq2d 6844 | . . . 4
⊢ (𝜑 → ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) ↔ (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀))) | 
| 36 | 17, 35 | mpbird 257 | . . 3
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀)) | 
| 37 |  | summo.3 | . . . . 5
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) | 
| 38 |  | fveq2 6906 | . . . . . 6
⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚)) | 
| 39 | 38 | csbeq1d 3903 | . . . . 5
⊢ (𝑛 = 𝑚 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) | 
| 40 |  | elfznn 13593 | . . . . . 6
⊢ (𝑚 ∈ (1...𝑀) → 𝑚 ∈ ℕ) | 
| 41 | 40 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → 𝑚 ∈ ℕ) | 
| 42 |  | f1of 6848 | . . . . . . . 8
⊢ (𝑓:(1...𝑀)–1-1-onto→𝐴 → 𝑓:(1...𝑀)⟶𝐴) | 
| 43 | 12, 42 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑓:(1...𝑀)⟶𝐴) | 
| 44 | 43 | ffvelcdmda 7104 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝑓‘𝑚) ∈ 𝐴) | 
| 45 |  | summo.2 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) | 
| 46 | 45 | ralrimiva 3146 | . . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) | 
| 47 | 46 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) | 
| 48 |  | nfcsb1v 3923 | . . . . . . . 8
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 | 
| 49 | 48 | nfel1 2922 | . . . . . . 7
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ | 
| 50 |  | csbeq1a 3913 | . . . . . . . 8
⊢ (𝑘 = (𝑓‘𝑚) → 𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) | 
| 51 | 50 | eleq1d 2826 | . . . . . . 7
⊢ (𝑘 = (𝑓‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) | 
| 52 | 49, 51 | rspc 3610 | . . . . . 6
⊢ ((𝑓‘𝑚) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) | 
| 53 | 44, 47, 52 | sylc 65 | . . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) | 
| 54 | 37, 39, 41, 53 | fvmptd3 7039 | . . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝐺‘𝑚) = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) | 
| 55 | 54, 53 | eqeltrd 2841 | . . 3
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝐺‘𝑚) ∈ ℂ) | 
| 56 | 34 | f1oeq2d 6844 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐾:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐾:(1...𝑁)–1-1-onto→𝐴)) | 
| 57 | 15, 56 | mpbird 257 | . . . . . . . . . 10
⊢ (𝜑 → 𝐾:(1...𝑀)–1-1-onto→𝐴) | 
| 58 |  | f1of 6848 | . . . . . . . . . 10
⊢ (𝐾:(1...𝑀)–1-1-onto→𝐴 → 𝐾:(1...𝑀)⟶𝐴) | 
| 59 | 57, 58 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐾:(1...𝑀)⟶𝐴) | 
| 60 |  | fvco3 7008 | . . . . . . . . 9
⊢ ((𝐾:(1...𝑀)⟶𝐴 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖))) | 
| 61 | 59, 60 | sylan 580 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖))) | 
| 62 | 61 | fveq2d 6910 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) = (𝑓‘(◡𝑓‘(𝐾‘𝑖)))) | 
| 63 | 12 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑓:(1...𝑀)–1-1-onto→𝐴) | 
| 64 | 59 | ffvelcdmda 7104 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) ∈ 𝐴) | 
| 65 |  | f1ocnvfv2 7297 | . . . . . . . 8
⊢ ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (𝐾‘𝑖) ∈ 𝐴) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖)) | 
| 66 | 63, 64, 65 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖)) | 
| 67 | 62, 66 | eqtr2d 2778 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) = (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖))) | 
| 68 | 67 | csbeq1d 3903 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ⦋(𝐾‘𝑖) / 𝑘⦌𝐵 = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵) | 
| 69 | 68 | fveq2d 6910 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵) = ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)) | 
| 70 |  | elfznn 13593 | . . . . . 6
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ) | 
| 71 | 70 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ ℕ) | 
| 72 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑛 = 𝑖 → (𝐾‘𝑛) = (𝐾‘𝑖)) | 
| 73 | 72 | csbeq1d 3903 | . . . . . 6
⊢ (𝑛 = 𝑖 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵) | 
| 74 |  | summolem3.4 | . . . . . 6
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⦋(𝐾‘𝑛) / 𝑘⦌𝐵) | 
| 75 | 73, 74 | fvmpti 7015 | . . . . 5
⊢ (𝑖 ∈ ℕ → (𝐻‘𝑖) = ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵)) | 
| 76 | 71, 75 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵)) | 
| 77 |  | f1of 6848 | . . . . . . 7
⊢ ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀)) | 
| 78 | 36, 77 | syl 17 | . . . . . 6
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀)) | 
| 79 | 78 | ffvelcdmda 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀)) | 
| 80 |  | elfznn 13593 | . . . . 5
⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ) | 
| 81 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → (𝑓‘𝑛) = (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖))) | 
| 82 | 81 | csbeq1d 3903 | . . . . . 6
⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵) | 
| 83 | 82, 37 | fvmpti 7015 | . . . . 5
⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)) | 
| 84 | 79, 80, 83 | 3syl 18 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)) | 
| 85 | 69, 76, 84 | 3eqtr4d 2787 | . . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖))) | 
| 86 | 2, 4, 6, 10, 11, 36, 55, 85 | seqf1o 14084 | . 2
⊢ (𝜑 → (seq1( + , 𝐻)‘𝑀) = (seq1( + , 𝐺)‘𝑀)) | 
| 87 | 33 | fveq2d 6910 | . 2
⊢ (𝜑 → (seq1( + , 𝐻)‘𝑀) = (seq1( + , 𝐻)‘𝑁)) | 
| 88 | 86, 87 | eqtr3d 2779 | 1
⊢ (𝜑 → (seq1( + , 𝐺)‘𝑀) = (seq1( + , 𝐻)‘𝑁)) |