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