This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfphi2

Description: Alternate definition of the Euler phi function. (Contributed by Mario Carneiro, 23-Feb-2014) (Revised by Mario Carneiro, 2-May-2016)

Ref Expression
Assertion dfphi2 ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) = ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) )

Proof

Step Hyp Ref Expression
1 elnn1uz2 ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) )
2 phi1 ⊢ ( ϕ ‘ 1 ) = 1
3 0z ⊢ 0 ∈ ℤ
4 hashsng ⊢ ( 0 ∈ ℤ → ( ♯ ‘ { 0 } ) = 1 )
5 3 4 ax-mp ⊢ ( ♯ ‘ { 0 } ) = 1
6 rabid2 ⊢ ( { 0 } = { 𝑥 ∈ { 0 } ∣ ( 𝑥 gcd 1 ) = 1 } ↔ ∀ 𝑥 ∈ { 0 } ( 𝑥 gcd 1 ) = 1 )
7 elsni ⊢ ( 𝑥 ∈ { 0 } → 𝑥 = 0 )
8 7 oveq1d ⊢ ( 𝑥 ∈ { 0 } → ( 𝑥 gcd 1 ) = ( 0 gcd 1 ) )
9 gcd1 ⊢ ( 0 ∈ ℤ → ( 0 gcd 1 ) = 1 )
10 3 9 ax-mp ⊢ ( 0 gcd 1 ) = 1
11 8 10 eqtrdi ⊢ ( 𝑥 ∈ { 0 } → ( 𝑥 gcd 1 ) = 1 )
12 6 11 mprgbir ⊢ { 0 } = { 𝑥 ∈ { 0 } ∣ ( 𝑥 gcd 1 ) = 1 }
13 12 fveq2i ⊢ ( ♯ ‘ { 0 } ) = ( ♯ ‘ { 𝑥 ∈ { 0 } ∣ ( 𝑥 gcd 1 ) = 1 } )
14 2 5 13 3eqtr2i ⊢ ( ϕ ‘ 1 ) = ( ♯ ‘ { 𝑥 ∈ { 0 } ∣ ( 𝑥 gcd 1 ) = 1 } )
15 fveq2 ⊢ ( 𝑁 = 1 → ( ϕ ‘ 𝑁 ) = ( ϕ ‘ 1 ) )
16 oveq2 ⊢ ( 𝑁 = 1 → ( 0 ..^ 𝑁 ) = ( 0 ..^ 1 ) )
17 fzo01 ⊢ ( 0 ..^ 1 ) = { 0 }
18 16 17 eqtrdi ⊢ ( 𝑁 = 1 → ( 0 ..^ 𝑁 ) = { 0 } )
19 oveq2 ⊢ ( 𝑁 = 1 → ( 𝑥 gcd 𝑁 ) = ( 𝑥 gcd 1 ) )
20 19 eqeq1d ⊢ ( 𝑁 = 1 → ( ( 𝑥 gcd 𝑁 ) = 1 ↔ ( 𝑥 gcd 1 ) = 1 ) )
21 18 20 rabeqbidv ⊢ ( 𝑁 = 1 → { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } = { 𝑥 ∈ { 0 } ∣ ( 𝑥 gcd 1 ) = 1 } )
22 21 fveq2d ⊢ ( 𝑁 = 1 → ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) = ( ♯ ‘ { 𝑥 ∈ { 0 } ∣ ( 𝑥 gcd 1 ) = 1 } ) )
23 14 15 22 3eqtr4a ⊢ ( 𝑁 = 1 → ( ϕ ‘ 𝑁 ) = ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) )
24 eluz2nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ )
25 phival ⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) = ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) )
26 24 25 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ϕ ‘ 𝑁 ) = ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) )
27 fzossfz ⊢ ( 1 ..^ 𝑁 ) ⊆ ( 1 ... 𝑁 )
28 27 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 1 ..^ 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
29 sseqin2 ⊢ ( ( 1 ..^ 𝑁 ) ⊆ ( 1 ... 𝑁 ) ↔ ( ( 1 ... 𝑁 ) ∩ ( 1 ..^ 𝑁 ) ) = ( 1 ..^ 𝑁 ) )
30 28 29 sylib ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 1 ... 𝑁 ) ∩ ( 1 ..^ 𝑁 ) ) = ( 1 ..^ 𝑁 ) )
31 fzo0ss1 ⊢ ( 1 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 )
32 sseqin2 ⊢ ( ( 1 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 ) ↔ ( ( 0 ..^ 𝑁 ) ∩ ( 1 ..^ 𝑁 ) ) = ( 1 ..^ 𝑁 ) )
33 31 32 mpbi ⊢ ( ( 0 ..^ 𝑁 ) ∩ ( 1 ..^ 𝑁 ) ) = ( 1 ..^ 𝑁 )
34 30 33 eqtr4di ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 1 ... 𝑁 ) ∩ ( 1 ..^ 𝑁 ) ) = ( ( 0 ..^ 𝑁 ) ∩ ( 1 ..^ 𝑁 ) ) )
35 34 rabeqdv ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → { 𝑥 ∈ ( ( 1 ... 𝑁 ) ∩ ( 1 ..^ 𝑁 ) ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } = { 𝑥 ∈ ( ( 0 ..^ 𝑁 ) ∩ ( 1 ..^ 𝑁 ) ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } )
36 inrab2 ⊢ ( { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ∩ ( 1 ..^ 𝑁 ) ) = { 𝑥 ∈ ( ( 1 ... 𝑁 ) ∩ ( 1 ..^ 𝑁 ) ) ∣ ( 𝑥 gcd 𝑁 ) = 1 }
37 inrab2 ⊢ ( { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ∩ ( 1 ..^ 𝑁 ) ) = { 𝑥 ∈ ( ( 0 ..^ 𝑁 ) ∩ ( 1 ..^ 𝑁 ) ) ∣ ( 𝑥 gcd 𝑁 ) = 1 }
38 35 36 37 3eqtr4g ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ∩ ( 1 ..^ 𝑁 ) ) = ( { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ∩ ( 1 ..^ 𝑁 ) ) )
39 phibndlem ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ⊆ ( 1 ... ( 𝑁 − 1 ) ) )
40 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℤ )
41 fzoval ⊢ ( 𝑁 ∈ ℤ → ( 1 ..^ 𝑁 ) = ( 1 ... ( 𝑁 − 1 ) ) )
42 40 41 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 1 ..^ 𝑁 ) = ( 1 ... ( 𝑁 − 1 ) ) )
43 39 42 sseqtrrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ⊆ ( 1 ..^ 𝑁 ) )
44 dfss2 ⊢ ( { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ⊆ ( 1 ..^ 𝑁 ) ↔ ( { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ∩ ( 1 ..^ 𝑁 ) ) = { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } )
45 43 44 sylib ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ∩ ( 1 ..^ 𝑁 ) ) = { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } )
46 gcd0id ⊢ ( 𝑁 ∈ ℤ → ( 0 gcd 𝑁 ) = ( abs ‘ 𝑁 ) )
47 40 46 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 0 gcd 𝑁 ) = ( abs ‘ 𝑁 ) )
48 eluzelre ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℝ )
49 eluzge2nn0 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ0 )
50 49 nn0ge0d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 0 ≤ 𝑁 )
51 48 50 absidd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( abs ‘ 𝑁 ) = 𝑁 )
52 47 51 eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 0 gcd 𝑁 ) = 𝑁 )
53 eluz2b3 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) )
54 53 simprbi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ≠ 1 )
55 52 54 eqnetrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 0 gcd 𝑁 ) ≠ 1 )
56 55 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( 0 gcd 𝑁 ) ≠ 1 )
57 7 oveq1d ⊢ ( 𝑥 ∈ { 0 } → ( 𝑥 gcd 𝑁 ) = ( 0 gcd 𝑁 ) )
58 57 17 eleq2s ⊢ ( 𝑥 ∈ ( 0 ..^ 1 ) → ( 𝑥 gcd 𝑁 ) = ( 0 gcd 𝑁 ) )
59 58 neeq1d ⊢ ( 𝑥 ∈ ( 0 ..^ 1 ) → ( ( 𝑥 gcd 𝑁 ) ≠ 1 ↔ ( 0 gcd 𝑁 ) ≠ 1 ) )
60 56 59 syl5ibrcom ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 0 ..^ 1 ) → ( 𝑥 gcd 𝑁 ) ≠ 1 ) )
61 60 necon2bd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑥 gcd 𝑁 ) = 1 → ¬ 𝑥 ∈ ( 0 ..^ 1 ) ) )
62 simpr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → 𝑥 ∈ ( 0 ..^ 𝑁 ) )
63 1z ⊢ 1 ∈ ℤ
64 fzospliti ⊢ ( ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∧ 1 ∈ ℤ ) → ( 𝑥 ∈ ( 0 ..^ 1 ) ∨ 𝑥 ∈ ( 1 ..^ 𝑁 ) ) )
65 62 63 64 sylancl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 0 ..^ 1 ) ∨ 𝑥 ∈ ( 1 ..^ 𝑁 ) ) )
66 65 ord ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ¬ 𝑥 ∈ ( 0 ..^ 1 ) → 𝑥 ∈ ( 1 ..^ 𝑁 ) ) )
67 61 66 syld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑥 gcd 𝑁 ) = 1 → 𝑥 ∈ ( 1 ..^ 𝑁 ) ) )
68 67 ralrimiva ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 𝑥 gcd 𝑁 ) = 1 → 𝑥 ∈ ( 1 ..^ 𝑁 ) ) )
69 rabss ⊢ ( { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ⊆ ( 1 ..^ 𝑁 ) ↔ ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( ( 𝑥 gcd 𝑁 ) = 1 → 𝑥 ∈ ( 1 ..^ 𝑁 ) ) )
70 68 69 sylibr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ⊆ ( 1 ..^ 𝑁 ) )
71 dfss2 ⊢ ( { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ⊆ ( 1 ..^ 𝑁 ) ↔ ( { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ∩ ( 1 ..^ 𝑁 ) ) = { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } )
72 70 71 sylib ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ∩ ( 1 ..^ 𝑁 ) ) = { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } )
73 38 45 72 3eqtr3d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } = { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } )
74 73 fveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) = ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) )
75 26 74 eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ϕ ‘ 𝑁 ) = ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) )
76 23 75 jaoi ⊢ ( ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ϕ ‘ 𝑁 ) = ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) )
77 1 76 sylbi ⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) = ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) )