Step | Hyp | Ref
| Expression |
1 | | nfcv 2902 |
. . 3
⊢
Ⅎ𝑢Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 |
2 | | nfcv 2902 |
. . . 4
⊢
Ⅎ𝑗{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} |
3 | | nfcsb1v 3690 |
. . . 4
⊢
Ⅎ𝑗⦋𝑢 / 𝑗⦌𝐴 |
4 | 2, 3 | nfsum 14620 |
. . 3
⊢
Ⅎ𝑗Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 |
5 | | breq2 4808 |
. . . . 5
⊢ (𝑗 = 𝑢 → (𝑥 ∥ 𝑗 ↔ 𝑥 ∥ 𝑢)) |
6 | 5 | rabbidv 3329 |
. . . 4
⊢ (𝑗 = 𝑢 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}) |
7 | | csbeq1a 3683 |
. . . . 5
⊢ (𝑗 = 𝑢 → 𝐴 = ⦋𝑢 / 𝑗⦌𝐴) |
8 | 7 | adantr 472 |
. . . 4
⊢ ((𝑗 = 𝑢 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}) → 𝐴 = ⦋𝑢 / 𝑗⦌𝐴) |
9 | 6, 8 | sumeq12dv 14636 |
. . 3
⊢ (𝑗 = 𝑢 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴) |
10 | 1, 4, 9 | cbvsumi 14626 |
. 2
⊢
Σ𝑗 ∈
{𝑥 ∈ ℕ ∣
𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 |
11 | | breq2 4808 |
. . . . . 6
⊢ (𝑢 = (𝑁 / 𝑣) → (𝑥 ∥ 𝑢 ↔ 𝑥 ∥ (𝑁 / 𝑣))) |
12 | 11 | rabbidv 3329 |
. . . . 5
⊢ (𝑢 = (𝑁 / 𝑣) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}) |
13 | | csbeq1 3677 |
. . . . . 6
⊢ (𝑢 = (𝑁 / 𝑣) → ⦋𝑢 / 𝑗⦌𝐴 = ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴) |
14 | 13 | adantr 472 |
. . . . 5
⊢ ((𝑢 = (𝑁 / 𝑣) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}) → ⦋𝑢 / 𝑗⦌𝐴 = ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴) |
15 | 12, 14 | sumeq12dv 14636 |
. . . 4
⊢ (𝑢 = (𝑁 / 𝑣) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴) |
16 | | fzfid 12966 |
. . . . 5
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
17 | | fsumdvdscom.1 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
18 | | dvdsssfz1 15242 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ (1...𝑁)) |
19 | 17, 18 | syl 17 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ (1...𝑁)) |
20 | | ssfi 8345 |
. . . . 5
⊢
(((1...𝑁) ∈ Fin
∧ {𝑥 ∈ ℕ
∣ 𝑥 ∥ 𝑁} ⊆ (1...𝑁)) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∈ Fin) |
21 | 16, 19, 20 | syl2anc 696 |
. . . 4
⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∈ Fin) |
22 | | eqid 2760 |
. . . . . 6
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} |
23 | | eqid 2760 |
. . . . . 6
⊢ (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)) = (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)) |
24 | 22, 23 | dvdsflip 15241 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
25 | 17, 24 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
26 | | oveq2 6821 |
. . . . . 6
⊢ (𝑧 = 𝑣 → (𝑁 / 𝑧) = (𝑁 / 𝑣)) |
27 | | ovex 6841 |
. . . . . 6
⊢ (𝑁 / 𝑧) ∈ V |
28 | 26, 23, 27 | fvmpt3i 6449 |
. . . . 5
⊢ (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))‘𝑣) = (𝑁 / 𝑣)) |
29 | 28 | adantl 473 |
. . . 4
⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))‘𝑣) = (𝑁 / 𝑣)) |
30 | | fzfid 12966 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (1...𝑢) ∈ Fin) |
31 | | ssrab2 3828 |
. . . . . . . 8
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ ℕ |
32 | | simpr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
33 | 31, 32 | sseldi 3742 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑢 ∈ ℕ) |
34 | | dvdsssfz1 15242 |
. . . . . . 7
⊢ (𝑢 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} ⊆ (1...𝑢)) |
35 | 33, 34 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} ⊆ (1...𝑢)) |
36 | | ssfi 8345 |
. . . . . 6
⊢
(((1...𝑢) ∈ Fin
∧ {𝑥 ∈ ℕ
∣ 𝑥 ∥ 𝑢} ⊆ (1...𝑢)) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} ∈ Fin) |
37 | 30, 35, 36 | syl2anc 696 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} ∈ Fin) |
38 | | fsumdvdscom.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗})) → 𝐴 ∈ ℂ) |
39 | 38 | ralrimivva 3109 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ) |
40 | | nfv 1992 |
. . . . . . . . 9
⊢
Ⅎ𝑢∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ |
41 | 3 | nfel1 2917 |
. . . . . . . . . 10
⊢
Ⅎ𝑗⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ |
42 | 2, 41 | nfral 3083 |
. . . . . . . . 9
⊢
Ⅎ𝑗∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ |
43 | 7 | eleq1d 2824 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑢 → (𝐴 ∈ ℂ ↔ ⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)) |
44 | 6, 43 | raleqbidv 3291 |
. . . . . . . . 9
⊢ (𝑗 = 𝑢 → (∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ ↔ ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)) |
45 | 40, 42, 44 | cbvral 3306 |
. . . . . . . 8
⊢
(∀𝑗 ∈
{𝑥 ∈ ℕ ∣
𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ ↔ ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ) |
46 | 39, 45 | sylib 208 |
. . . . . . 7
⊢ (𝜑 → ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ) |
47 | 46 | r19.21bi 3070 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ) |
48 | 47 | r19.21bi 3070 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}) → ⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ) |
49 | 37, 48 | fsumcl 14663 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ) |
50 | 15, 21, 25, 29, 49 | fsumf1o 14653 |
. . 3
⊢ (𝜑 → Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 = Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴) |
51 | 13 | eleq1d 2824 |
. . . . . . . 8
⊢ (𝑢 = (𝑁 / 𝑣) → (⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ ↔ ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)) |
52 | 12, 51 | raleqbidv 3291 |
. . . . . . 7
⊢ (𝑢 = (𝑁 / 𝑣) → (∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ ↔ ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)) |
53 | 46 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ) |
54 | | dvdsdivcl 15240 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑣) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
55 | 17, 54 | sylan 489 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑣) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
56 | 52, 53, 55 | rspcdva 3455 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ) |
57 | 56 | r19.21bi 3070 |
. . . . 5
⊢ (((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ) |
58 | 57 | anasss 682 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)})) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ) |
59 | 17, 58 | fsumdvdsdiag 25109 |
. . 3
⊢ (𝜑 → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴) |
60 | | oveq2 6821 |
. . . . . . 7
⊢ (𝑣 = ((𝑁 / 𝑘) / 𝑚) → (𝑁 / 𝑣) = (𝑁 / ((𝑁 / 𝑘) / 𝑚))) |
61 | 60 | csbeq1d 3681 |
. . . . . 6
⊢ (𝑣 = ((𝑁 / 𝑘) / 𝑚) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = ⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴) |
62 | | fzfid 12966 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (1...(𝑁 / 𝑘)) ∈ Fin) |
63 | | dvdsdivcl 15240 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
64 | 31, 63 | sseldi 3742 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑘) ∈ ℕ) |
65 | 17, 64 | sylan 489 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑘) ∈ ℕ) |
66 | | dvdsssfz1 15242 |
. . . . . . . 8
⊢ ((𝑁 / 𝑘) ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ⊆ (1...(𝑁 / 𝑘))) |
67 | 65, 66 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ⊆ (1...(𝑁 / 𝑘))) |
68 | | ssfi 8345 |
. . . . . . 7
⊢
(((1...(𝑁 / 𝑘)) ∈ Fin ∧ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ⊆ (1...(𝑁 / 𝑘))) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ∈ Fin) |
69 | 62, 67, 68 | syl2anc 696 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ∈ Fin) |
70 | | eqid 2760 |
. . . . . . . 8
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} |
71 | | eqid 2760 |
. . . . . . . 8
⊢ (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)) = (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)) |
72 | 70, 71 | dvdsflip 15241 |
. . . . . . 7
⊢ ((𝑁 / 𝑘) ∈ ℕ → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) |
73 | 65, 72 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) |
74 | | oveq2 6821 |
. . . . . . . 8
⊢ (𝑧 = 𝑚 → ((𝑁 / 𝑘) / 𝑧) = ((𝑁 / 𝑘) / 𝑚)) |
75 | | ovex 6841 |
. . . . . . . 8
⊢ ((𝑁 / 𝑘) / 𝑧) ∈ V |
76 | 74, 71, 75 | fvmpt3i 6449 |
. . . . . . 7
⊢ (𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧))‘𝑚) = ((𝑁 / 𝑘) / 𝑚)) |
77 | 76 | adantl 473 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧))‘𝑚) = ((𝑁 / 𝑘) / 𝑚)) |
78 | 17 | fsumdvdsdiaglem 25108 |
. . . . . . . 8
⊢ (𝜑 → ((𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}))) |
79 | 58 | ex 449 |
. . . . . . . 8
⊢ (𝜑 → ((𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)) |
80 | 78, 79 | syld 47 |
. . . . . . 7
⊢ (𝜑 → ((𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)) |
81 | 80 | impl 651 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ) |
82 | 61, 69, 73, 77, 81 | fsumf1o 14653 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴) |
83 | | ovexd 6843 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) ∈ V) |
84 | | nncn 11220 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
85 | | nnne0 11245 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
86 | 84, 85 | jca 555 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
87 | 17, 86 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
88 | 87 | ad2antrr 764 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
89 | 88 | simpld 477 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑁 ∈ ℂ) |
90 | | elrabi 3499 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → 𝑘 ∈ ℕ) |
91 | 90 | adantl 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑘 ∈ ℕ) |
92 | 91 | adantr 472 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑘 ∈ ℕ) |
93 | | nncn 11220 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
94 | | nnne0 11245 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0) |
95 | 93, 94 | jca 555 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0)) |
96 | 92, 95 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0)) |
97 | | elrabi 3499 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} → 𝑚 ∈ ℕ) |
98 | 97 | adantl 473 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑚 ∈ ℕ) |
99 | | nncn 11220 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
100 | | nnne0 11245 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ → 𝑚 ≠ 0) |
101 | 99, 100 | jca 555 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) |
102 | 98, 101 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) |
103 | | divdiv1 10928 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℂ ∧ (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → ((𝑁 / 𝑘) / 𝑚) = (𝑁 / (𝑘 · 𝑚))) |
104 | 89, 96, 102, 103 | syl3anc 1477 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑁 / 𝑘) / 𝑚) = (𝑁 / (𝑘 · 𝑚))) |
105 | 104 | oveq2d 6829 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) = (𝑁 / (𝑁 / (𝑘 · 𝑚)))) |
106 | | nnmulcl 11235 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑘 · 𝑚) ∈ ℕ) |
107 | 91, 97, 106 | syl2an 495 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑘 · 𝑚) ∈ ℕ) |
108 | | nncn 11220 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 · 𝑚) ∈ ℕ → (𝑘 · 𝑚) ∈ ℂ) |
109 | | nnne0 11245 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 · 𝑚) ∈ ℕ → (𝑘 · 𝑚) ≠ 0) |
110 | 108, 109 | jca 555 |
. . . . . . . . . . . . 13
⊢ ((𝑘 · 𝑚) ∈ ℕ → ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0)) |
111 | 107, 110 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0)) |
112 | | ddcan 10931 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0)) → (𝑁 / (𝑁 / (𝑘 · 𝑚))) = (𝑘 · 𝑚)) |
113 | 88, 111, 112 | syl2anc 696 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / (𝑁 / (𝑘 · 𝑚))) = (𝑘 · 𝑚)) |
114 | 105, 113 | eqtrd 2794 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) = (𝑘 · 𝑚)) |
115 | 114 | eqeq2d 2770 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚)) ↔ 𝑗 = (𝑘 · 𝑚))) |
116 | 115 | biimpa 502 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) ∧ 𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚))) → 𝑗 = (𝑘 · 𝑚)) |
117 | | fsumdvdscom.2 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 · 𝑚) → 𝐴 = 𝐵) |
118 | 116, 117 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) ∧ 𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚))) → 𝐴 = 𝐵) |
119 | 83, 118 | csbied 3701 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴 = 𝐵) |
120 | 119 | sumeq2dv 14632 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵) |
121 | 82, 120 | eqtrd 2794 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵) |
122 | 121 | sumeq2dv 14632 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵) |
123 | 50, 59, 122 | 3eqtrd 2798 |
. 2
⊢ (𝜑 → Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵) |
124 | 10, 123 | syl5eq 2806 |
1
⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵) |