| Step | Hyp | Ref
| Expression |
| 1 | | breq1 5146 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ∥ 𝑁 ↔ 𝑦 ∥ 𝑁)) |
| 2 | 1 | elrab 3692 |
. . . . 5
⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↔ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁)) |
| 3 | | hashgcdeq 16827 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℕ) →
(♯‘{𝑧 ∈
(0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = if(𝑦 ∥ 𝑁, (ϕ‘(𝑁 / 𝑦)), 0)) |
| 4 | 3 | adantrr 717 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁)) → (♯‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = if(𝑦 ∥ 𝑁, (ϕ‘(𝑁 / 𝑦)), 0)) |
| 5 | | iftrue 4531 |
. . . . . . 7
⊢ (𝑦 ∥ 𝑁 → if(𝑦 ∥ 𝑁, (ϕ‘(𝑁 / 𝑦)), 0) = (ϕ‘(𝑁 / 𝑦))) |
| 6 | 5 | ad2antll 729 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁)) → if(𝑦 ∥ 𝑁, (ϕ‘(𝑁 / 𝑦)), 0) = (ϕ‘(𝑁 / 𝑦))) |
| 7 | 4, 6 | eqtrd 2777 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁)) → (♯‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = (ϕ‘(𝑁 / 𝑦))) |
| 8 | 2, 7 | sylan2b 594 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (♯‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = (ϕ‘(𝑁 / 𝑦))) |
| 9 | 8 | sumeq2dv 15738 |
. . 3
⊢ (𝑁 ∈ ℕ →
Σ𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (♯‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = Σ𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘(𝑁 / 𝑦))) |
| 10 | | dvdsfi 16826 |
. . . 4
⊢ (𝑁 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∈ Fin) |
| 11 | | fzofi 14015 |
. . . . . 6
⊢
(0..^𝑁) ∈
Fin |
| 12 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ⊆ (0..^𝑁) |
| 13 | | ssfi 9213 |
. . . . . 6
⊢
(((0..^𝑁) ∈ Fin
∧ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ⊆ (0..^𝑁)) → {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ∈ Fin) |
| 14 | 11, 12, 13 | mp2an 692 |
. . . . 5
⊢ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ∈ Fin |
| 15 | 14 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ∈ Fin) |
| 16 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑤 → (𝑧 gcd 𝑁) = (𝑤 gcd 𝑁)) |
| 17 | 16 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → ((𝑧 gcd 𝑁) = 𝑦 ↔ (𝑤 gcd 𝑁) = 𝑦)) |
| 18 | 17 | elrab 3692 |
. . . . . . . 8
⊢ (𝑤 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ↔ (𝑤 ∈ (0..^𝑁) ∧ (𝑤 gcd 𝑁) = 𝑦)) |
| 19 | 18 | simprbi 496 |
. . . . . . 7
⊢ (𝑤 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} → (𝑤 gcd 𝑁) = 𝑦) |
| 20 | 19 | rgen 3063 |
. . . . . 6
⊢
∀𝑤 ∈
{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} (𝑤 gcd 𝑁) = 𝑦 |
| 21 | 20 | rgenw 3065 |
. . . . 5
⊢
∀𝑦 ∈
{𝑥 ∈ ℕ ∣
𝑥 ∥ 𝑁}∀𝑤 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} (𝑤 gcd 𝑁) = 𝑦 |
| 22 | | invdisj 5129 |
. . . . 5
⊢
(∀𝑦 ∈
{𝑥 ∈ ℕ ∣
𝑥 ∥ 𝑁}∀𝑤 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} (𝑤 gcd 𝑁) = 𝑦 → Disj 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) |
| 23 | 21, 22 | mp1i 13 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Disj 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) |
| 24 | 10, 15, 23 | hashiun 15858 |
. . 3
⊢ (𝑁 ∈ ℕ →
(♯‘∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = Σ𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (♯‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦})) |
| 25 | | fveq2 6906 |
. . . 4
⊢ (𝑑 = (𝑁 / 𝑦) → (ϕ‘𝑑) = (ϕ‘(𝑁 / 𝑦))) |
| 26 | | eqid 2737 |
. . . . 5
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} |
| 27 | | eqid 2737 |
. . . . 5
⊢ (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)) = (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)) |
| 28 | 26, 27 | dvdsflip 16354 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
| 29 | | oveq2 7439 |
. . . . . 6
⊢ (𝑧 = 𝑦 → (𝑁 / 𝑧) = (𝑁 / 𝑦)) |
| 30 | | ovex 7464 |
. . . . . 6
⊢ (𝑁 / 𝑦) ∈ V |
| 31 | 29, 27, 30 | fvmpt 7016 |
. . . . 5
⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))‘𝑦) = (𝑁 / 𝑦)) |
| 32 | 31 | adantl 481 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))‘𝑦) = (𝑁 / 𝑦)) |
| 33 | | elrabi 3687 |
. . . . . . 7
⊢ (𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → 𝑑 ∈ ℕ) |
| 34 | 33 | adantl 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑑 ∈ ℕ) |
| 35 | 34 | phicld 16809 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (ϕ‘𝑑) ∈ ℕ) |
| 36 | 35 | nncnd 12282 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (ϕ‘𝑑) ∈ ℂ) |
| 37 | 25, 10, 28, 32, 36 | fsumf1o 15759 |
. . 3
⊢ (𝑁 ∈ ℕ →
Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘𝑑) = Σ𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘(𝑁 / 𝑦))) |
| 38 | 9, 24, 37 | 3eqtr4rd 2788 |
. 2
⊢ (𝑁 ∈ ℕ →
Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘𝑑) = (♯‘∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦})) |
| 39 | | iunrab 5052 |
. . . . 5
⊢ ∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} = {𝑧 ∈ (0..^𝑁) ∣ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦} |
| 40 | | breq1 5146 |
. . . . . . . . 9
⊢ (𝑥 = (𝑧 gcd 𝑁) → (𝑥 ∥ 𝑁 ↔ (𝑧 gcd 𝑁) ∥ 𝑁)) |
| 41 | | elfzoelz 13699 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (0..^𝑁) → 𝑧 ∈ ℤ) |
| 42 | 41 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → 𝑧 ∈ ℤ) |
| 43 | | nnz 12634 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
| 44 | 43 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → 𝑁 ∈ ℤ) |
| 45 | | nnne0 12300 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
| 46 | 45 | neneqd 2945 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ¬
𝑁 = 0) |
| 47 | 46 | intnand 488 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ¬
(𝑧 = 0 ∧ 𝑁 = 0)) |
| 48 | 47 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → ¬ (𝑧 = 0 ∧ 𝑁 = 0)) |
| 49 | | gcdn0cl 16539 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑧 = 0 ∧ 𝑁 = 0)) → (𝑧 gcd 𝑁) ∈ ℕ) |
| 50 | 42, 44, 48, 49 | syl21anc 838 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → (𝑧 gcd 𝑁) ∈ ℕ) |
| 51 | | gcddvds 16540 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑧 gcd 𝑁) ∥ 𝑧 ∧ (𝑧 gcd 𝑁) ∥ 𝑁)) |
| 52 | 42, 44, 51 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → ((𝑧 gcd 𝑁) ∥ 𝑧 ∧ (𝑧 gcd 𝑁) ∥ 𝑁)) |
| 53 | 52 | simprd 495 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → (𝑧 gcd 𝑁) ∥ 𝑁) |
| 54 | 40, 50, 53 | elrabd 3694 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → (𝑧 gcd 𝑁) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) |
| 55 | | clel5 3665 |
. . . . . . . 8
⊢ ((𝑧 gcd 𝑁) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↔ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦) |
| 56 | 54, 55 | sylib 218 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦) |
| 57 | 56 | ralrimiva 3146 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
∀𝑧 ∈ (0..^𝑁)∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦) |
| 58 | | rabid2 3470 |
. . . . . 6
⊢
((0..^𝑁) = {𝑧 ∈ (0..^𝑁) ∣ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦} ↔ ∀𝑧 ∈ (0..^𝑁)∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦) |
| 59 | 57, 58 | sylibr 234 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(0..^𝑁) = {𝑧 ∈ (0..^𝑁) ∣ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦}) |
| 60 | 39, 59 | eqtr4id 2796 |
. . . 4
⊢ (𝑁 ∈ ℕ → ∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} = (0..^𝑁)) |
| 61 | 60 | fveq2d 6910 |
. . 3
⊢ (𝑁 ∈ ℕ →
(♯‘∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = (♯‘(0..^𝑁))) |
| 62 | | nnnn0 12533 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
| 63 | | hashfzo0 14469 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (♯‘(0..^𝑁)) = 𝑁) |
| 64 | 62, 63 | syl 17 |
. . 3
⊢ (𝑁 ∈ ℕ →
(♯‘(0..^𝑁)) =
𝑁) |
| 65 | 61, 64 | eqtrd 2777 |
. 2
⊢ (𝑁 ∈ ℕ →
(♯‘∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = 𝑁) |
| 66 | 38, 65 | eqtrd 2777 |
1
⊢ (𝑁 ∈ ℕ →
Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘𝑑) = 𝑁) |