Metamath Proof Explorer

Theorem phisum

Description: The divisor sum identity of the totient function. Theorem 2.2 in ApostolNT p. 26. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Assertion phisum ( 𝑁 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ϕ ‘ 𝑑 ) = 𝑁 )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∥ 𝑁 ↔ 𝑦 ∥ 𝑁 ) )
2 1 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁 ) )
3 hashgcdeq ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( ♯ ‘ { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ) = if ( 𝑦 ∥ 𝑁 , ( ϕ ‘ ( 𝑁 / 𝑦 ) ) , 0 ) )
4 3 adantrr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁 ) ) → ( ♯ ‘ { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ) = if ( 𝑦 ∥ 𝑁 , ( ϕ ‘ ( 𝑁 / 𝑦 ) ) , 0 ) )
5 iftrue ⊢ ( 𝑦 ∥ 𝑁 → if ( 𝑦 ∥ 𝑁 , ( ϕ ‘ ( 𝑁 / 𝑦 ) ) , 0 ) = ( ϕ ‘ ( 𝑁 / 𝑦 ) ) )
6 5 ad2antll ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁 ) ) → if ( 𝑦 ∥ 𝑁 , ( ϕ ‘ ( 𝑁 / 𝑦 ) ) , 0 ) = ( ϕ ‘ ( 𝑁 / 𝑦 ) ) )
7 4 6 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁 ) ) → ( ♯ ‘ { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ) = ( ϕ ‘ ( 𝑁 / 𝑦 ) ) )
8 2 7 sylan2b ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ♯ ‘ { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ) = ( ϕ ‘ ( 𝑁 / 𝑦 ) ) )
9 8 sumeq2dv ⊢ ( 𝑁 ∈ ℕ → Σ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ♯ ‘ { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ) = Σ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ϕ ‘ ( 𝑁 / 𝑦 ) ) )
10 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
11 dvdsssfz1 ⊢ ( 𝑁 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) )
12 ssfi ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∈ Fin )
13 10 11 12 sylancr ⊢ ( 𝑁 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∈ Fin )
14 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
15 ssrab2 ⊢ { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ⊆ ( 0 ..^ 𝑁 )
16 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ⊆ ( 0 ..^ 𝑁 ) ) → { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ∈ Fin )
17 14 15 16 mp2an ⊢ { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ∈ Fin
18 17 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ∈ Fin )
19 oveq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 gcd 𝑁 ) = ( 𝑤 gcd 𝑁 ) )
20 19 eqeq1d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑧 gcd 𝑁 ) = 𝑦 ↔ ( 𝑤 gcd 𝑁 ) = 𝑦 ) )
21 20 elrab ⊢ ( 𝑤 ∈ { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ↔ ( 𝑤 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝑤 gcd 𝑁 ) = 𝑦 ) )
22 21 simprbi ⊢ ( 𝑤 ∈ { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } → ( 𝑤 gcd 𝑁 ) = 𝑦 )
23 22 rgen ⊢ ∀ 𝑤 ∈ { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ( 𝑤 gcd 𝑁 ) = 𝑦
24 23 rgenw ⊢ ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∀ 𝑤 ∈ { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ( 𝑤 gcd 𝑁 ) = 𝑦
25 invdisj ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∀ 𝑤 ∈ { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ( 𝑤 gcd 𝑁 ) = 𝑦 → Disj 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } )
26 24 25 mp1i ⊢ ( 𝑁 ∈ ℕ → Disj 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } )
27 13 18 26 hashiun ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ ∪ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ) = Σ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ♯ ‘ { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ) )
28 fveq2 ⊢ ( 𝑑 = ( 𝑁 / 𝑦 ) → ( ϕ ‘ 𝑑 ) = ( ϕ ‘ ( 𝑁 / 𝑦 ) ) )
29 eqid ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 }
30 eqid ⊢ ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↦ ( 𝑁 / 𝑧 ) ) = ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↦ ( 𝑁 / 𝑧 ) )
31 29 30 dvdsflip ⊢ ( 𝑁 ∈ ℕ → ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↦ ( 𝑁 / 𝑧 ) ) : { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } –1-1-onto→ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
32 oveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑁 / 𝑧 ) = ( 𝑁 / 𝑦 ) )
33 ovex ⊢ ( 𝑁 / 𝑦 ) ∈ V
34 32 30 33 fvmpt ⊢ ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } → ( ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↦ ( 𝑁 / 𝑧 ) ) ‘ 𝑦 ) = ( 𝑁 / 𝑦 ) )
35 34 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↦ ( 𝑁 / 𝑧 ) ) ‘ 𝑦 ) = ( 𝑁 / 𝑦 ) )
36 elrabi ⊢ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } → 𝑑 ∈ ℕ )
37 36 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑑 ∈ ℕ )
38 37 phicld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ϕ ‘ 𝑑 ) ∈ ℕ )
39 38 nncnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ϕ ‘ 𝑑 ) ∈ ℂ )
40 28 13 31 35 39 fsumf1o ⊢ ( 𝑁 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ϕ ‘ 𝑑 ) = Σ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ϕ ‘ ( 𝑁 / 𝑦 ) ) )
41 9 27 40 3eqtr4rd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ϕ ‘ 𝑑 ) = ( ♯ ‘ ∪ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ) )
42 iunrab ⊢ ∪ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } = { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ∃ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( 𝑧 gcd 𝑁 ) = 𝑦 }
43 breq1 ⊢ ( 𝑥 = ( 𝑧 gcd 𝑁 ) → ( 𝑥 ∥ 𝑁 ↔ ( 𝑧 gcd 𝑁 ) ∥ 𝑁 ) )
44 elfzoelz ⊢ ( 𝑧 ∈ ( 0 ..^ 𝑁 ) → 𝑧 ∈ ℤ )
45 44 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ..^ 𝑁 ) ) → 𝑧 ∈ ℤ )
46 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
47 46 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℤ )
48 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
49 48 neneqd ⊢ ( 𝑁 ∈ ℕ → ¬ 𝑁 = 0 )
50 49 intnand ⊢ ( 𝑁 ∈ ℕ → ¬ ( 𝑧 = 0 ∧ 𝑁 = 0 ) )
51 50 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ..^ 𝑁 ) ) → ¬ ( 𝑧 = 0 ∧ 𝑁 = 0 ) )
52 gcdn0cl ⊢ ( ( ( 𝑧 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑧 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑧 gcd 𝑁 ) ∈ ℕ )
53 45 47 51 52 syl21anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑧 gcd 𝑁 ) ∈ ℕ )
54 gcddvds ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑧 gcd 𝑁 ) ∥ 𝑧 ∧ ( 𝑧 gcd 𝑁 ) ∥ 𝑁 ) )
55 45 47 54 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑧 gcd 𝑁 ) ∥ 𝑧 ∧ ( 𝑧 gcd 𝑁 ) ∥ 𝑁 ) )
56 55 simprd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑧 gcd 𝑁 ) ∥ 𝑁 )
57 43 53 56 elrabd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑧 gcd 𝑁 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
58 clel5 ⊢ ( ( 𝑧 gcd 𝑁 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↔ ∃ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( 𝑧 gcd 𝑁 ) = 𝑦 )
59 57 58 sylib ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ( 0 ..^ 𝑁 ) ) → ∃ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( 𝑧 gcd 𝑁 ) = 𝑦 )
60 59 ralrimiva ⊢ ( 𝑁 ∈ ℕ → ∀ 𝑧 ∈ ( 0 ..^ 𝑁 ) ∃ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( 𝑧 gcd 𝑁 ) = 𝑦 )
61 rabid2 ⊢ ( ( 0 ..^ 𝑁 ) = { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ∃ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( 𝑧 gcd 𝑁 ) = 𝑦 } ↔ ∀ 𝑧 ∈ ( 0 ..^ 𝑁 ) ∃ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( 𝑧 gcd 𝑁 ) = 𝑦 )
62 60 61 sylibr ⊢ ( 𝑁 ∈ ℕ → ( 0 ..^ 𝑁 ) = { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ∃ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( 𝑧 gcd 𝑁 ) = 𝑦 } )
63 42 62 eqtr4id ⊢ ( 𝑁 ∈ ℕ → ∪ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } = ( 0 ..^ 𝑁 ) )
64 63 fveq2d ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ ∪ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ) = ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
65 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
66 hashfzo0 ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
67 65 66 syl ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
68 64 67 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ ∪ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } { 𝑧 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑧 gcd 𝑁 ) = 𝑦 } ) = 𝑁 )
69 41 68 eqtrd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ϕ ‘ 𝑑 ) = 𝑁 )