Step | Hyp | Ref
| Expression |
1 | | breq1 3969 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ∥ 𝑁 ↔ 𝑦 ∥ 𝑁)) |
2 | 1 | elrab 2868 |
. . . . 5
⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↔ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁)) |
3 | | hashgcdeq 12118 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℕ) →
(♯‘{𝑧 ∈
(0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = if(𝑦 ∥ 𝑁, (ϕ‘(𝑁 / 𝑦)), 0)) |
4 | 3 | adantrr 471 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁)) → (♯‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = if(𝑦 ∥ 𝑁, (ϕ‘(𝑁 / 𝑦)), 0)) |
5 | | iftrue 3510 |
. . . . . . 7
⊢ (𝑦 ∥ 𝑁 → if(𝑦 ∥ 𝑁, (ϕ‘(𝑁 / 𝑦)), 0) = (ϕ‘(𝑁 / 𝑦))) |
6 | 5 | ad2antll 483 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁)) → if(𝑦 ∥ 𝑁, (ϕ‘(𝑁 / 𝑦)), 0) = (ϕ‘(𝑁 / 𝑦))) |
7 | 4, 6 | eqtrd 2190 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁)) → (♯‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = (ϕ‘(𝑁 / 𝑦))) |
8 | 2, 7 | sylan2b 285 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (♯‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = (ϕ‘(𝑁 / 𝑦))) |
9 | 8 | sumeq2dv 11269 |
. . 3
⊢ (𝑁 ∈ ℕ →
Σ𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (♯‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = Σ𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘(𝑁 / 𝑦))) |
10 | | 1zzd 9195 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 1 ∈
ℤ) |
11 | | nnz 9187 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
12 | 10, 11 | fzfigd 10334 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(1...𝑁) ∈
Fin) |
13 | | dvdsssfz1 11748 |
. . . . 5
⊢ (𝑁 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ (1...𝑁)) |
14 | | elfznn 9957 |
. . . . . . . 8
⊢ (𝑗 ∈ (1...𝑁) → 𝑗 ∈ ℕ) |
15 | | dvdsdc 11698 |
. . . . . . . 8
⊢ ((𝑗 ∈ ℕ ∧ 𝑁 ∈ ℤ) →
DECID 𝑗
∥ 𝑁) |
16 | 14, 11, 15 | syl2anr 288 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...𝑁)) → DECID 𝑗 ∥ 𝑁) |
17 | | ibar 299 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → (𝑗 ∥ 𝑁 ↔ (𝑗 ∈ ℕ ∧ 𝑗 ∥ 𝑁))) |
18 | 14, 17 | syl 14 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1...𝑁) → (𝑗 ∥ 𝑁 ↔ (𝑗 ∈ ℕ ∧ 𝑗 ∥ 𝑁))) |
19 | | breq1 3969 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑗 → (𝑥 ∥ 𝑁 ↔ 𝑗 ∥ 𝑁)) |
20 | 19 | elrab 2868 |
. . . . . . . . . 10
⊢ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↔ (𝑗 ∈ ℕ ∧ 𝑗 ∥ 𝑁)) |
21 | 18, 20 | bitr4di 197 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...𝑁) → (𝑗 ∥ 𝑁 ↔ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})) |
22 | 21 | dcbid 824 |
. . . . . . . 8
⊢ (𝑗 ∈ (1...𝑁) → (DECID 𝑗 ∥ 𝑁 ↔ DECID 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})) |
23 | 22 | adantl 275 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...𝑁)) → (DECID 𝑗 ∥ 𝑁 ↔ DECID 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})) |
24 | 16, 23 | mpbid 146 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...𝑁)) → DECID 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
25 | 24 | ralrimiva 2530 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
∀𝑗 ∈ (1...𝑁)DECID 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
26 | | ssfidc 6880 |
. . . . 5
⊢
(((1...𝑁) ∈ Fin
∧ {𝑥 ∈ ℕ
∣ 𝑥 ∥ 𝑁} ⊆ (1...𝑁) ∧ ∀𝑗 ∈ (1...𝑁)DECID 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∈ Fin) |
27 | 12, 13, 25, 26 | syl3anc 1220 |
. . . 4
⊢ (𝑁 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∈ Fin) |
28 | | 0z 9179 |
. . . . . . 7
⊢ 0 ∈
ℤ |
29 | | fzofig 10335 |
. . . . . . 7
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → (0..^𝑁) ∈ Fin) |
30 | 28, 11, 29 | sylancr 411 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(0..^𝑁) ∈
Fin) |
31 | 30 | adantr 274 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (0..^𝑁) ∈ Fin) |
32 | | ssrab2 3213 |
. . . . . 6
⊢ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ⊆ (0..^𝑁) |
33 | 32 | a1i 9 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ⊆ (0..^𝑁)) |
34 | | elfzoelz 10050 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ) |
35 | 34 | adantl 275 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℤ) |
36 | 11 | ad2antrr 480 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑁 ∈ ℤ) |
37 | 35, 36 | gcdcld 11856 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 gcd 𝑁) ∈
ℕ0) |
38 | 37 | nn0zd 9285 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 gcd 𝑁) ∈ ℤ) |
39 | | elrabi 2865 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → 𝑦 ∈ ℕ) |
40 | 39 | ad2antlr 481 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑦 ∈ ℕ) |
41 | 40 | nnzd 9286 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑦 ∈ ℤ) |
42 | | zdceq 9240 |
. . . . . . . 8
⊢ (((𝑗 gcd 𝑁) ∈ ℤ ∧ 𝑦 ∈ ℤ) → DECID
(𝑗 gcd 𝑁) = 𝑦) |
43 | 38, 41, 42 | syl2anc 409 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑗 ∈ (0..^𝑁)) → DECID (𝑗 gcd 𝑁) = 𝑦) |
44 | | ibar 299 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (0..^𝑁) → ((𝑗 gcd 𝑁) = 𝑦 ↔ (𝑗 ∈ (0..^𝑁) ∧ (𝑗 gcd 𝑁) = 𝑦))) |
45 | | oveq1 5832 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑗 → (𝑧 gcd 𝑁) = (𝑗 gcd 𝑁)) |
46 | 45 | eqeq1d 2166 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑗 → ((𝑧 gcd 𝑁) = 𝑦 ↔ (𝑗 gcd 𝑁) = 𝑦)) |
47 | 46 | elrab 2868 |
. . . . . . . . . 10
⊢ (𝑗 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ↔ (𝑗 ∈ (0..^𝑁) ∧ (𝑗 gcd 𝑁) = 𝑦)) |
48 | 44, 47 | bitr4di 197 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0..^𝑁) → ((𝑗 gcd 𝑁) = 𝑦 ↔ 𝑗 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦})) |
49 | 48 | dcbid 824 |
. . . . . . . 8
⊢ (𝑗 ∈ (0..^𝑁) → (DECID (𝑗 gcd 𝑁) = 𝑦 ↔ DECID 𝑗 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦})) |
50 | 49 | adantl 275 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑗 ∈ (0..^𝑁)) → (DECID (𝑗 gcd 𝑁) = 𝑦 ↔ DECID 𝑗 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦})) |
51 | 43, 50 | mpbid 146 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑗 ∈ (0..^𝑁)) → DECID 𝑗 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) |
52 | 51 | ralrimiva 2530 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ∀𝑗 ∈ (0..^𝑁)DECID 𝑗 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) |
53 | | ssfidc 6880 |
. . . . 5
⊢
(((0..^𝑁) ∈ Fin
∧ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ⊆ (0..^𝑁) ∧ ∀𝑗 ∈ (0..^𝑁)DECID 𝑗 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) → {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ∈ Fin) |
54 | 31, 33, 52, 53 | syl3anc 1220 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ∈ Fin) |
55 | | oveq1 5832 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑤 → (𝑧 gcd 𝑁) = (𝑤 gcd 𝑁)) |
56 | 55 | eqeq1d 2166 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → ((𝑧 gcd 𝑁) = 𝑦 ↔ (𝑤 gcd 𝑁) = 𝑦)) |
57 | 56 | elrab 2868 |
. . . . . . . 8
⊢ (𝑤 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ↔ (𝑤 ∈ (0..^𝑁) ∧ (𝑤 gcd 𝑁) = 𝑦)) |
58 | 57 | simprbi 273 |
. . . . . . 7
⊢ (𝑤 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} → (𝑤 gcd 𝑁) = 𝑦) |
59 | 58 | rgen 2510 |
. . . . . 6
⊢
∀𝑤 ∈
{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} (𝑤 gcd 𝑁) = 𝑦 |
60 | 59 | rgenw 2512 |
. . . . 5
⊢
∀𝑦 ∈
{𝑥 ∈ ℕ ∣
𝑥 ∥ 𝑁}∀𝑤 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} (𝑤 gcd 𝑁) = 𝑦 |
61 | | invdisj 3960 |
. . . . 5
⊢
(∀𝑦 ∈
{𝑥 ∈ ℕ ∣
𝑥 ∥ 𝑁}∀𝑤 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} (𝑤 gcd 𝑁) = 𝑦 → Disj 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) |
62 | 60, 61 | mp1i 10 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Disj 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) |
63 | 27, 54, 62 | hashiun 11379 |
. . 3
⊢ (𝑁 ∈ ℕ →
(♯‘∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = Σ𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (♯‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦})) |
64 | | fveq2 5469 |
. . . 4
⊢ (𝑑 = (𝑁 / 𝑦) → (ϕ‘𝑑) = (ϕ‘(𝑁 / 𝑦))) |
65 | | eqid 2157 |
. . . . 5
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} |
66 | | eqid 2157 |
. . . . 5
⊢ (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)) = (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)) |
67 | 65, 66 | dvdsflip 11747 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
68 | | oveq2 5833 |
. . . . 5
⊢ (𝑧 = 𝑦 → (𝑁 / 𝑧) = (𝑁 / 𝑦)) |
69 | | simpr 109 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
70 | 11 | adantr 274 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑁 ∈ ℤ) |
71 | 39 | adantl 275 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑦 ∈ ℕ) |
72 | | znq 9534 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑁 / 𝑦) ∈ ℚ) |
73 | 70, 71, 72 | syl2anc 409 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑦) ∈ ℚ) |
74 | 66, 68, 69, 73 | fvmptd3 5562 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))‘𝑦) = (𝑁 / 𝑦)) |
75 | | elrabi 2865 |
. . . . . . 7
⊢ (𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → 𝑑 ∈ ℕ) |
76 | 75 | adantl 275 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑑 ∈ ℕ) |
77 | 76 | phicld 12097 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (ϕ‘𝑑) ∈ ℕ) |
78 | 77 | nncnd 8848 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (ϕ‘𝑑) ∈ ℂ) |
79 | 64, 27, 67, 74, 78 | fsumf1o 11291 |
. . 3
⊢ (𝑁 ∈ ℕ →
Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘𝑑) = Σ𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘(𝑁 / 𝑦))) |
80 | 9, 63, 79 | 3eqtr4rd 2201 |
. 2
⊢ (𝑁 ∈ ℕ →
Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘𝑑) = (♯‘∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦})) |
81 | | iunrab 3897 |
. . . . 5
⊢ ∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} = {𝑧 ∈ (0..^𝑁) ∣ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦} |
82 | | breq1 3969 |
. . . . . . . . 9
⊢ (𝑥 = (𝑧 gcd 𝑁) → (𝑥 ∥ 𝑁 ↔ (𝑧 gcd 𝑁) ∥ 𝑁)) |
83 | | elfzoelz 10050 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (0..^𝑁) → 𝑧 ∈ ℤ) |
84 | 83 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → 𝑧 ∈ ℤ) |
85 | 11 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → 𝑁 ∈ ℤ) |
86 | | nnne0 8862 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
87 | 86 | neneqd 2348 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ¬
𝑁 = 0) |
88 | 87 | intnand 917 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ¬
(𝑧 = 0 ∧ 𝑁 = 0)) |
89 | 88 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → ¬ (𝑧 = 0 ∧ 𝑁 = 0)) |
90 | | gcdn0cl 11850 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑧 = 0 ∧ 𝑁 = 0)) → (𝑧 gcd 𝑁) ∈ ℕ) |
91 | 84, 85, 89, 90 | syl21anc 1219 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → (𝑧 gcd 𝑁) ∈ ℕ) |
92 | | gcddvds 11851 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑧 gcd 𝑁) ∥ 𝑧 ∧ (𝑧 gcd 𝑁) ∥ 𝑁)) |
93 | 84, 85, 92 | syl2anc 409 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → ((𝑧 gcd 𝑁) ∥ 𝑧 ∧ (𝑧 gcd 𝑁) ∥ 𝑁)) |
94 | 93 | simprd 113 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → (𝑧 gcd 𝑁) ∥ 𝑁) |
95 | 82, 91, 94 | elrabd 2870 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → (𝑧 gcd 𝑁) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
96 | | clel5 2849 |
. . . . . . . 8
⊢ ((𝑧 gcd 𝑁) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↔ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦) |
97 | 95, 96 | sylib 121 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦) |
98 | 97 | ralrimiva 2530 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
∀𝑧 ∈ (0..^𝑁)∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦) |
99 | | rabid2 2633 |
. . . . . 6
⊢
((0..^𝑁) = {𝑧 ∈ (0..^𝑁) ∣ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦} ↔ ∀𝑧 ∈ (0..^𝑁)∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦) |
100 | 98, 99 | sylibr 133 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(0..^𝑁) = {𝑧 ∈ (0..^𝑁) ∣ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦}) |
101 | 81, 100 | eqtr4id 2209 |
. . . 4
⊢ (𝑁 ∈ ℕ → ∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} = (0..^𝑁)) |
102 | 101 | fveq2d 5473 |
. . 3
⊢ (𝑁 ∈ ℕ →
(♯‘∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = (♯‘(0..^𝑁))) |
103 | | nnnn0 9098 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
104 | | hashfzo0 10701 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (♯‘(0..^𝑁)) = 𝑁) |
105 | 103, 104 | syl 14 |
. . 3
⊢ (𝑁 ∈ ℕ →
(♯‘(0..^𝑁)) =
𝑁) |
106 | 102, 105 | eqtrd 2190 |
. 2
⊢ (𝑁 ∈ ℕ →
(♯‘∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = 𝑁) |
107 | 80, 106 | eqtrd 2190 |
1
⊢ (𝑁 ∈ ℕ →
Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘𝑑) = 𝑁) |