Step | Hyp | Ref
| Expression |
1 | | breq1 4586 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ∥ 𝑁 ↔ 𝑦 ∥ 𝑁)) |
2 | 1 | elrab 3331 |
. . . . 5
⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↔ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁)) |
3 | | hashgcdeq 15332 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℕ) →
(#‘{𝑧 ∈
(0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = if(𝑦 ∥ 𝑁, (ϕ‘(𝑁 / 𝑦)), 0)) |
4 | 3 | adantrr 749 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁)) → (#‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = if(𝑦 ∥ 𝑁, (ϕ‘(𝑁 / 𝑦)), 0)) |
5 | | iftrue 4042 |
. . . . . . 7
⊢ (𝑦 ∥ 𝑁 → if(𝑦 ∥ 𝑁, (ϕ‘(𝑁 / 𝑦)), 0) = (ϕ‘(𝑁 / 𝑦))) |
6 | 5 | ad2antll 761 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁)) → if(𝑦 ∥ 𝑁, (ϕ‘(𝑁 / 𝑦)), 0) = (ϕ‘(𝑁 / 𝑦))) |
7 | 4, 6 | eqtrd 2644 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁)) → (#‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = (ϕ‘(𝑁 / 𝑦))) |
8 | 2, 7 | sylan2b 491 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (#‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = (ϕ‘(𝑁 / 𝑦))) |
9 | 8 | sumeq2dv 14281 |
. . 3
⊢ (𝑁 ∈ ℕ →
Σ𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (#‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = Σ𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘(𝑁 / 𝑦))) |
10 | | fzfi 12633 |
. . . . 5
⊢
(1...𝑁) ∈
Fin |
11 | | dvdsssfz1 14878 |
. . . . 5
⊢ (𝑁 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ (1...𝑁)) |
12 | | ssfi 8065 |
. . . . 5
⊢
(((1...𝑁) ∈ Fin
∧ {𝑥 ∈ ℕ
∣ 𝑥 ∥ 𝑁} ⊆ (1...𝑁)) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∈ Fin) |
13 | 10, 11, 12 | sylancr 694 |
. . . 4
⊢ (𝑁 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∈ Fin) |
14 | | fzofi 12635 |
. . . . . 6
⊢
(0..^𝑁) ∈
Fin |
15 | | ssrab2 3650 |
. . . . . 6
⊢ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ⊆ (0..^𝑁) |
16 | | ssfi 8065 |
. . . . . 6
⊢
(((0..^𝑁) ∈ Fin
∧ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ⊆ (0..^𝑁)) → {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ∈ Fin) |
17 | 14, 15, 16 | mp2an 704 |
. . . . 5
⊢ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ∈ Fin |
18 | 17 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ∈ Fin) |
19 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑤 → (𝑧 gcd 𝑁) = (𝑤 gcd 𝑁)) |
20 | 19 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → ((𝑧 gcd 𝑁) = 𝑦 ↔ (𝑤 gcd 𝑁) = 𝑦)) |
21 | 20 | elrab 3331 |
. . . . . . . 8
⊢ (𝑤 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ↔ (𝑤 ∈ (0..^𝑁) ∧ (𝑤 gcd 𝑁) = 𝑦)) |
22 | 21 | simprbi 479 |
. . . . . . 7
⊢ (𝑤 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} → (𝑤 gcd 𝑁) = 𝑦) |
23 | 22 | rgen 2906 |
. . . . . 6
⊢
∀𝑤 ∈
{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} (𝑤 gcd 𝑁) = 𝑦 |
24 | 23 | rgenw 2908 |
. . . . 5
⊢
∀𝑦 ∈
{𝑥 ∈ ℕ ∣
𝑥 ∥ 𝑁}∀𝑤 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} (𝑤 gcd 𝑁) = 𝑦 |
25 | | invdisj 4571 |
. . . . 5
⊢
(∀𝑦 ∈
{𝑥 ∈ ℕ ∣
𝑥 ∥ 𝑁}∀𝑤 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} (𝑤 gcd 𝑁) = 𝑦 → Disj 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) |
26 | 24, 25 | mp1i 13 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Disj 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) |
27 | 13, 18, 26 | hashiun 14395 |
. . 3
⊢ (𝑁 ∈ ℕ →
(#‘∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = Σ𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (#‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦})) |
28 | | fveq2 6103 |
. . . 4
⊢ (𝑑 = (𝑁 / 𝑦) → (ϕ‘𝑑) = (ϕ‘(𝑁 / 𝑦))) |
29 | | eqid 2610 |
. . . . 5
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} |
30 | | eqid 2610 |
. . . . 5
⊢ (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)) = (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)) |
31 | 29, 30 | dvdsflip 14877 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
32 | | oveq2 6557 |
. . . . . 6
⊢ (𝑧 = 𝑦 → (𝑁 / 𝑧) = (𝑁 / 𝑦)) |
33 | | ovex 6577 |
. . . . . 6
⊢ (𝑁 / 𝑦) ∈ V |
34 | 32, 30, 33 | fvmpt 6191 |
. . . . 5
⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))‘𝑦) = (𝑁 / 𝑦)) |
35 | 34 | adantl 481 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))‘𝑦) = (𝑁 / 𝑦)) |
36 | | elrabi 3328 |
. . . . . . 7
⊢ (𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → 𝑑 ∈ ℕ) |
37 | 36 | adantl 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑑 ∈ ℕ) |
38 | 37 | phicld 15315 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (ϕ‘𝑑) ∈ ℕ) |
39 | 38 | nncnd 10913 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (ϕ‘𝑑) ∈ ℂ) |
40 | 28, 13, 31, 35, 39 | fsumf1o 14301 |
. . 3
⊢ (𝑁 ∈ ℕ →
Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘𝑑) = Σ𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘(𝑁 / 𝑦))) |
41 | 9, 27, 40 | 3eqtr4rd 2655 |
. 2
⊢ (𝑁 ∈ ℕ →
Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘𝑑) = (#‘∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦})) |
42 | | elfzoelz 12339 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (0..^𝑁) → 𝑧 ∈ ℤ) |
43 | 42 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → 𝑧 ∈ ℤ) |
44 | | nnz 11276 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
45 | 44 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → 𝑁 ∈ ℤ) |
46 | | nnne0 10930 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
47 | 46 | neneqd 2787 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ¬
𝑁 = 0) |
48 | 47 | intnand 953 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ¬
(𝑧 = 0 ∧ 𝑁 = 0)) |
49 | 48 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → ¬ (𝑧 = 0 ∧ 𝑁 = 0)) |
50 | | gcdn0cl 15062 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑧 = 0 ∧ 𝑁 = 0)) → (𝑧 gcd 𝑁) ∈ ℕ) |
51 | 43, 45, 49, 50 | syl21anc 1317 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → (𝑧 gcd 𝑁) ∈ ℕ) |
52 | | gcddvds 15063 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑧 gcd 𝑁) ∥ 𝑧 ∧ (𝑧 gcd 𝑁) ∥ 𝑁)) |
53 | 43, 45, 52 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → ((𝑧 gcd 𝑁) ∥ 𝑧 ∧ (𝑧 gcd 𝑁) ∥ 𝑁)) |
54 | 53 | simprd 478 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → (𝑧 gcd 𝑁) ∥ 𝑁) |
55 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑧 gcd 𝑁) → (𝑥 ∥ 𝑁 ↔ (𝑧 gcd 𝑁) ∥ 𝑁)) |
56 | 55 | elrab 3331 |
. . . . . . . . 9
⊢ ((𝑧 gcd 𝑁) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↔ ((𝑧 gcd 𝑁) ∈ ℕ ∧ (𝑧 gcd 𝑁) ∥ 𝑁)) |
57 | 51, 54, 56 | sylanbrc 695 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → (𝑧 gcd 𝑁) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
58 | | risset 3044 |
. . . . . . . . 9
⊢ ((𝑧 gcd 𝑁) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↔ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}𝑦 = (𝑧 gcd 𝑁)) |
59 | | eqcom 2617 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑧 gcd 𝑁) ↔ (𝑧 gcd 𝑁) = 𝑦) |
60 | 59 | rexbii 3023 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
{𝑥 ∈ ℕ ∣
𝑥 ∥ 𝑁}𝑦 = (𝑧 gcd 𝑁) ↔ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦) |
61 | 58, 60 | bitri 263 |
. . . . . . . 8
⊢ ((𝑧 gcd 𝑁) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↔ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦) |
62 | 57, 61 | sylib 207 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦) |
63 | 62 | ralrimiva 2949 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
∀𝑧 ∈ (0..^𝑁)∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦) |
64 | | rabid2 3096 |
. . . . . 6
⊢
((0..^𝑁) = {𝑧 ∈ (0..^𝑁) ∣ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦} ↔ ∀𝑧 ∈ (0..^𝑁)∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦) |
65 | 63, 64 | sylibr 223 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(0..^𝑁) = {𝑧 ∈ (0..^𝑁) ∣ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦}) |
66 | | iunrab 4503 |
. . . . 5
⊢ ∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} = {𝑧 ∈ (0..^𝑁) ∣ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦} |
67 | 65, 66 | syl6reqr 2663 |
. . . 4
⊢ (𝑁 ∈ ℕ → ∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} = (0..^𝑁)) |
68 | 67 | fveq2d 6107 |
. . 3
⊢ (𝑁 ∈ ℕ →
(#‘∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = (#‘(0..^𝑁))) |
69 | | nnnn0 11176 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
70 | | hashfzo0 13077 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (#‘(0..^𝑁)) =
𝑁) |
71 | 69, 70 | syl 17 |
. . 3
⊢ (𝑁 ∈ ℕ →
(#‘(0..^𝑁)) = 𝑁) |
72 | 68, 71 | eqtrd 2644 |
. 2
⊢ (𝑁 ∈ ℕ →
(#‘∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = 𝑁) |
73 | 41, 72 | eqtrd 2644 |
1
⊢ (𝑁 ∈ ℕ →
Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘𝑑) = 𝑁) |