Step | Hyp | Ref
| Expression |
1 | | nfcv 2764 |
. . 3
⊢
Ⅎ𝑢Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 |
2 | | nfcv 2764 |
. . . 4
⊢
Ⅎ𝑗{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} |
3 | | nfcsb1v 3549 |
. . . 4
⊢
Ⅎ𝑗⦋𝑢 / 𝑗⦌𝐴 |
4 | 2, 3 | nfsum 14421 |
. . 3
⊢
Ⅎ𝑗Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 |
5 | | breq2 4657 |
. . . . 5
⊢ (𝑗 = 𝑢 → (𝑥 ∥ 𝑗 ↔ 𝑥 ∥ 𝑢)) |
6 | 5 | rabbidv 3189 |
. . . 4
⊢ (𝑗 = 𝑢 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}) |
7 | | csbeq1a 3542 |
. . . . 5
⊢ (𝑗 = 𝑢 → 𝐴 = ⦋𝑢 / 𝑗⦌𝐴) |
8 | 7 | adantr 481 |
. . . 4
⊢ ((𝑗 = 𝑢 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}) → 𝐴 = ⦋𝑢 / 𝑗⦌𝐴) |
9 | 6, 8 | sumeq12dv 14437 |
. . 3
⊢ (𝑗 = 𝑢 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴) |
10 | 1, 4, 9 | cbvsumi 14427 |
. 2
⊢
Σ𝑗 ∈
{𝑥 ∈ ℕ ∣
𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 |
11 | | breq2 4657 |
. . . . . 6
⊢ (𝑢 = (𝑁 / 𝑣) → (𝑥 ∥ 𝑢 ↔ 𝑥 ∥ (𝑁 / 𝑣))) |
12 | 11 | rabbidv 3189 |
. . . . 5
⊢ (𝑢 = (𝑁 / 𝑣) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}) |
13 | | csbeq1 3536 |
. . . . . 6
⊢ (𝑢 = (𝑁 / 𝑣) → ⦋𝑢 / 𝑗⦌𝐴 = ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴) |
14 | 13 | adantr 481 |
. . . . 5
⊢ ((𝑢 = (𝑁 / 𝑣) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}) → ⦋𝑢 / 𝑗⦌𝐴 = ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴) |
15 | 12, 14 | sumeq12dv 14437 |
. . . 4
⊢ (𝑢 = (𝑁 / 𝑣) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴) |
16 | | fzfid 12772 |
. . . . 5
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
17 | | fsumdvdscom.1 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
18 | | dvdsssfz1 15040 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ (1...𝑁)) |
19 | 17, 18 | syl 17 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ (1...𝑁)) |
20 | | ssfi 8180 |
. . . . 5
⊢
(((1...𝑁) ∈ Fin
∧ {𝑥 ∈ ℕ
∣ 𝑥 ∥ 𝑁} ⊆ (1...𝑁)) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∈ Fin) |
21 | 16, 19, 20 | syl2anc 693 |
. . . 4
⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∈ Fin) |
22 | | eqid 2622 |
. . . . . 6
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} |
23 | | eqid 2622 |
. . . . . 6
⊢ (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)) = (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)) |
24 | 22, 23 | dvdsflip 15039 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
25 | 17, 24 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
26 | | oveq2 6658 |
. . . . . 6
⊢ (𝑧 = 𝑣 → (𝑁 / 𝑧) = (𝑁 / 𝑣)) |
27 | | ovex 6678 |
. . . . . 6
⊢ (𝑁 / 𝑧) ∈ V |
28 | 26, 23, 27 | fvmpt3i 6287 |
. . . . 5
⊢ (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))‘𝑣) = (𝑁 / 𝑣)) |
29 | 28 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))‘𝑣) = (𝑁 / 𝑣)) |
30 | | fzfid 12772 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (1...𝑢) ∈ Fin) |
31 | | ssrab2 3687 |
. . . . . . . 8
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ ℕ |
32 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
33 | 31, 32 | sseldi 3601 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑢 ∈ ℕ) |
34 | | dvdsssfz1 15040 |
. . . . . . 7
⊢ (𝑢 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} ⊆ (1...𝑢)) |
35 | 33, 34 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} ⊆ (1...𝑢)) |
36 | | ssfi 8180 |
. . . . . 6
⊢
(((1...𝑢) ∈ Fin
∧ {𝑥 ∈ ℕ
∣ 𝑥 ∥ 𝑢} ⊆ (1...𝑢)) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} ∈ Fin) |
37 | 30, 35, 36 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} ∈ Fin) |
38 | | fsumdvdscom.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗})) → 𝐴 ∈ ℂ) |
39 | 38 | ralrimivva 2971 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ) |
40 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑢∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ |
41 | 3 | nfel1 2779 |
. . . . . . . . . 10
⊢
Ⅎ𝑗⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ |
42 | 2, 41 | nfral 2945 |
. . . . . . . . 9
⊢
Ⅎ𝑗∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ |
43 | 7 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑢 → (𝐴 ∈ ℂ ↔ ⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)) |
44 | 6, 43 | raleqbidv 3152 |
. . . . . . . . 9
⊢ (𝑗 = 𝑢 → (∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ ↔ ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)) |
45 | 40, 42, 44 | cbvral 3167 |
. . . . . . . 8
⊢
(∀𝑗 ∈
{𝑥 ∈ ℕ ∣
𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ ↔ ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ) |
46 | 39, 45 | sylib 208 |
. . . . . . 7
⊢ (𝜑 → ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ) |
47 | 46 | r19.21bi 2932 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ) |
48 | 47 | r19.21bi 2932 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}) → ⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ) |
49 | 37, 48 | fsumcl 14464 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ) |
50 | 15, 21, 25, 29, 49 | fsumf1o 14454 |
. . 3
⊢ (𝜑 → Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 = Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴) |
51 | | dvdsdivcl 15038 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑣) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
52 | 17, 51 | sylan 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑣) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
53 | 46 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ) |
54 | 13 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑢 = (𝑁 / 𝑣) → (⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ ↔ ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)) |
55 | 12, 54 | raleqbidv 3152 |
. . . . . . . 8
⊢ (𝑢 = (𝑁 / 𝑣) → (∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ ↔ ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)) |
56 | 55 | rspcv 3305 |
. . . . . . 7
⊢ ((𝑁 / 𝑣) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → (∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ → ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)) |
57 | 52, 53, 56 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ) |
58 | 57 | r19.21bi 2932 |
. . . . 5
⊢ (((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ) |
59 | 58 | anasss 679 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)})) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ) |
60 | 17, 59 | fsumdvdsdiag 24910 |
. . 3
⊢ (𝜑 → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴) |
61 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑣 = ((𝑁 / 𝑘) / 𝑚) → (𝑁 / 𝑣) = (𝑁 / ((𝑁 / 𝑘) / 𝑚))) |
62 | 61 | csbeq1d 3540 |
. . . . . 6
⊢ (𝑣 = ((𝑁 / 𝑘) / 𝑚) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = ⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴) |
63 | | fzfid 12772 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (1...(𝑁 / 𝑘)) ∈ Fin) |
64 | | dvdsdivcl 15038 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
65 | 31, 64 | sseldi 3601 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑘) ∈ ℕ) |
66 | 17, 65 | sylan 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑘) ∈ ℕ) |
67 | | dvdsssfz1 15040 |
. . . . . . . 8
⊢ ((𝑁 / 𝑘) ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ⊆ (1...(𝑁 / 𝑘))) |
68 | 66, 67 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ⊆ (1...(𝑁 / 𝑘))) |
69 | | ssfi 8180 |
. . . . . . 7
⊢
(((1...(𝑁 / 𝑘)) ∈ Fin ∧ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ⊆ (1...(𝑁 / 𝑘))) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ∈ Fin) |
70 | 63, 68, 69 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ∈ Fin) |
71 | | eqid 2622 |
. . . . . . . 8
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} |
72 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)) = (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)) |
73 | 71, 72 | dvdsflip 15039 |
. . . . . . 7
⊢ ((𝑁 / 𝑘) ∈ ℕ → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) |
74 | 66, 73 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) |
75 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑧 = 𝑚 → ((𝑁 / 𝑘) / 𝑧) = ((𝑁 / 𝑘) / 𝑚)) |
76 | | ovex 6678 |
. . . . . . . 8
⊢ ((𝑁 / 𝑘) / 𝑧) ∈ V |
77 | 75, 72, 76 | fvmpt3i 6287 |
. . . . . . 7
⊢ (𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧))‘𝑚) = ((𝑁 / 𝑘) / 𝑚)) |
78 | 77 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧))‘𝑚) = ((𝑁 / 𝑘) / 𝑚)) |
79 | 17 | fsumdvdsdiaglem 24909 |
. . . . . . . 8
⊢ (𝜑 → ((𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}))) |
80 | 59 | ex 450 |
. . . . . . . 8
⊢ (𝜑 → ((𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)) |
81 | 79, 80 | syld 47 |
. . . . . . 7
⊢ (𝜑 → ((𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)) |
82 | 81 | impl 650 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ) |
83 | 62, 70, 74, 78, 82 | fsumf1o 14454 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴) |
84 | | ovexd 6680 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) ∈ V) |
85 | | nncn 11028 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
86 | | nnne0 11053 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
87 | 85, 86 | jca 554 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
88 | 17, 87 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
89 | 88 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
90 | 89 | simpld 475 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑁 ∈ ℂ) |
91 | | elrabi 3359 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → 𝑘 ∈ ℕ) |
92 | 91 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑘 ∈ ℕ) |
93 | 92 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑘 ∈ ℕ) |
94 | | nncn 11028 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
95 | | nnne0 11053 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0) |
96 | 94, 95 | jca 554 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0)) |
97 | 93, 96 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0)) |
98 | | elrabi 3359 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} → 𝑚 ∈ ℕ) |
99 | 98 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑚 ∈ ℕ) |
100 | | nncn 11028 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
101 | | nnne0 11053 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ → 𝑚 ≠ 0) |
102 | 100, 101 | jca 554 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) |
103 | 99, 102 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) |
104 | | divdiv1 10736 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℂ ∧ (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → ((𝑁 / 𝑘) / 𝑚) = (𝑁 / (𝑘 · 𝑚))) |
105 | 90, 97, 103, 104 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑁 / 𝑘) / 𝑚) = (𝑁 / (𝑘 · 𝑚))) |
106 | 105 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) = (𝑁 / (𝑁 / (𝑘 · 𝑚)))) |
107 | | nnmulcl 11043 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑘 · 𝑚) ∈ ℕ) |
108 | 92, 98, 107 | syl2an 494 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑘 · 𝑚) ∈ ℕ) |
109 | | nncn 11028 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 · 𝑚) ∈ ℕ → (𝑘 · 𝑚) ∈ ℂ) |
110 | | nnne0 11053 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 · 𝑚) ∈ ℕ → (𝑘 · 𝑚) ≠ 0) |
111 | 109, 110 | jca 554 |
. . . . . . . . . . . . 13
⊢ ((𝑘 · 𝑚) ∈ ℕ → ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0)) |
112 | 108, 111 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0)) |
113 | | ddcan 10739 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0)) → (𝑁 / (𝑁 / (𝑘 · 𝑚))) = (𝑘 · 𝑚)) |
114 | 89, 112, 113 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / (𝑁 / (𝑘 · 𝑚))) = (𝑘 · 𝑚)) |
115 | 106, 114 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) = (𝑘 · 𝑚)) |
116 | 115 | eqeq2d 2632 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚)) ↔ 𝑗 = (𝑘 · 𝑚))) |
117 | 116 | biimpa 501 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) ∧ 𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚))) → 𝑗 = (𝑘 · 𝑚)) |
118 | | fsumdvdscom.2 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 · 𝑚) → 𝐴 = 𝐵) |
119 | 117, 118 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) ∧ 𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚))) → 𝐴 = 𝐵) |
120 | 84, 119 | csbied 3560 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴 = 𝐵) |
121 | 120 | sumeq2dv 14433 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵) |
122 | 83, 121 | eqtrd 2656 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵) |
123 | 122 | sumeq2dv 14433 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵) |
124 | 50, 60, 123 | 3eqtrd 2660 |
. 2
⊢ (𝜑 → Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵) |
125 | 10, 124 | syl5eq 2668 |
1
⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵) |