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 
|- ( N e. NN -> ( phi ` N ) = ( # ` { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } ) )

Proof

Step Hyp Ref Expression
1 elnn1uz2 
 |-  ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
2 phi1 
 |-  ( phi ` 1 ) = 1
3 0z 
 |-  0 e. ZZ
4 hashsng 
 |-  ( 0 e. ZZ -> ( # ` { 0 } ) = 1 )
5 3 4 ax-mp 
 |-  ( # ` { 0 } ) = 1
6 rabid2 
 |-  ( { 0 } = { x e. { 0 } | ( x gcd 1 ) = 1 } <-> A. x e. { 0 } ( x gcd 1 ) = 1 )
7 elsni 
 |-  ( x e. { 0 } -> x = 0 )
8 7 oveq1d 
 |-  ( x e. { 0 } -> ( x gcd 1 ) = ( 0 gcd 1 ) )
9 gcd1 
 |-  ( 0 e. ZZ -> ( 0 gcd 1 ) = 1 )
10 3 9 ax-mp 
 |-  ( 0 gcd 1 ) = 1
11 8 10 eqtrdi 
 |-  ( x e. { 0 } -> ( x gcd 1 ) = 1 )
12 6 11 mprgbir 
 |-  { 0 } = { x e. { 0 } | ( x gcd 1 ) = 1 }
13 12 fveq2i 
 |-  ( # ` { 0 } ) = ( # ` { x e. { 0 } | ( x gcd 1 ) = 1 } )
14 2 5 13 3eqtr2i 
 |-  ( phi ` 1 ) = ( # ` { x e. { 0 } | ( x gcd 1 ) = 1 } )
15 fveq2 
 |-  ( N = 1 -> ( phi ` N ) = ( phi ` 1 ) )
16 oveq2 
 |-  ( N = 1 -> ( 0 ..^ N ) = ( 0 ..^ 1 ) )
17 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
18 16 17 eqtrdi 
 |-  ( N = 1 -> ( 0 ..^ N ) = { 0 } )
19 oveq2 
 |-  ( N = 1 -> ( x gcd N ) = ( x gcd 1 ) )
20 19 eqeq1d 
 |-  ( N = 1 -> ( ( x gcd N ) = 1 <-> ( x gcd 1 ) = 1 ) )
21 18 20 rabeqbidv 
 |-  ( N = 1 -> { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } = { x e. { 0 } | ( x gcd 1 ) = 1 } )
22 21 fveq2d 
 |-  ( N = 1 -> ( # ` { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } ) = ( # ` { x e. { 0 } | ( x gcd 1 ) = 1 } ) )
23 14 15 22 3eqtr4a 
 |-  ( N = 1 -> ( phi ` N ) = ( # ` { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } ) )
24 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
25 phival 
 |-  ( N e. NN -> ( phi ` N ) = ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) )
26 24 25 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( phi ` N ) = ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) )
27 fzossfz 
 |-  ( 1 ..^ N ) C_ ( 1 ... N )
28 27 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 ..^ N ) C_ ( 1 ... N ) )
29 sseqin2 
 |-  ( ( 1 ..^ N ) C_ ( 1 ... N ) <-> ( ( 1 ... N ) i^i ( 1 ..^ N ) ) = ( 1 ..^ N ) )
30 28 29 sylib 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 1 ... N ) i^i ( 1 ..^ N ) ) = ( 1 ..^ N ) )
31 fzo0ss1 
 |-  ( 1 ..^ N ) C_ ( 0 ..^ N )
32 sseqin2 
 |-  ( ( 1 ..^ N ) C_ ( 0 ..^ N ) <-> ( ( 0 ..^ N ) i^i ( 1 ..^ N ) ) = ( 1 ..^ N ) )
33 31 32 mpbi 
 |-  ( ( 0 ..^ N ) i^i ( 1 ..^ N ) ) = ( 1 ..^ N )
34 30 33 eqtr4di 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 1 ... N ) i^i ( 1 ..^ N ) ) = ( ( 0 ..^ N ) i^i ( 1 ..^ N ) ) )
35 34 rabeqdv 
 |-  ( N e. ( ZZ>= ` 2 ) -> { x e. ( ( 1 ... N ) i^i ( 1 ..^ N ) ) | ( x gcd N ) = 1 } = { x e. ( ( 0 ..^ N ) i^i ( 1 ..^ N ) ) | ( x gcd N ) = 1 } )
36 inrab2 
 |-  ( { x e. ( 1 ... N ) | ( x gcd N ) = 1 } i^i ( 1 ..^ N ) ) = { x e. ( ( 1 ... N ) i^i ( 1 ..^ N ) ) | ( x gcd N ) = 1 }
37 inrab2 
 |-  ( { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } i^i ( 1 ..^ N ) ) = { x e. ( ( 0 ..^ N ) i^i ( 1 ..^ N ) ) | ( x gcd N ) = 1 }
38 35 36 37 3eqtr4g 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( { x e. ( 1 ... N ) | ( x gcd N ) = 1 } i^i ( 1 ..^ N ) ) = ( { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } i^i ( 1 ..^ N ) ) )
39 phibndlem 
 |-  ( N e. ( ZZ>= ` 2 ) -> { x e. ( 1 ... N ) | ( x gcd N ) = 1 } C_ ( 1 ... ( N - 1 ) ) )
40 eluzelz 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. ZZ )
41 fzoval 
 |-  ( N e. ZZ -> ( 1 ..^ N ) = ( 1 ... ( N - 1 ) ) )
42 40 41 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 ..^ N ) = ( 1 ... ( N - 1 ) ) )
43 39 42 sseqtrrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> { x e. ( 1 ... N ) | ( x gcd N ) = 1 } C_ ( 1 ..^ N ) )
44 dfss2 
 |-  ( { x e. ( 1 ... N ) | ( x gcd N ) = 1 } C_ ( 1 ..^ N ) <-> ( { x e. ( 1 ... N ) | ( x gcd N ) = 1 } i^i ( 1 ..^ N ) ) = { x e. ( 1 ... N ) | ( x gcd N ) = 1 } )
45 43 44 sylib 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( { x e. ( 1 ... N ) | ( x gcd N ) = 1 } i^i ( 1 ..^ N ) ) = { x e. ( 1 ... N ) | ( x gcd N ) = 1 } )
46 gcd0id 
 |-  ( N e. ZZ -> ( 0 gcd N ) = ( abs ` N ) )
47 40 46 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 0 gcd N ) = ( abs ` N ) )
48 eluzelre 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. RR )
49 eluzge2nn0 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN0 )
50 49 nn0ge0d 
 |-  ( N e. ( ZZ>= ` 2 ) -> 0 <_ N )
51 48 50 absidd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( abs ` N ) = N )
52 47 51 eqtrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 0 gcd N ) = N )
53 eluz2b3 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ N =/= 1 ) )
54 53 simprbi 
 |-  ( N e. ( ZZ>= ` 2 ) -> N =/= 1 )
55 52 54 eqnetrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 0 gcd N ) =/= 1 )
56 55 adantr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ x e. ( 0 ..^ N ) ) -> ( 0 gcd N ) =/= 1 )
57 7 oveq1d 
 |-  ( x e. { 0 } -> ( x gcd N ) = ( 0 gcd N ) )
58 57 17 eleq2s 
 |-  ( x e. ( 0 ..^ 1 ) -> ( x gcd N ) = ( 0 gcd N ) )
59 58 neeq1d 
 |-  ( x e. ( 0 ..^ 1 ) -> ( ( x gcd N ) =/= 1 <-> ( 0 gcd N ) =/= 1 ) )
60 56 59 syl5ibrcom 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ x e. ( 0 ..^ N ) ) -> ( x e. ( 0 ..^ 1 ) -> ( x gcd N ) =/= 1 ) )
61 60 necon2bd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ x e. ( 0 ..^ N ) ) -> ( ( x gcd N ) = 1 -> -. x e. ( 0 ..^ 1 ) ) )
62 simpr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ x e. ( 0 ..^ N ) ) -> x e. ( 0 ..^ N ) )
63 1z 
 |-  1 e. ZZ
64 fzospliti 
 |-  ( ( x e. ( 0 ..^ N ) /\ 1 e. ZZ ) -> ( x e. ( 0 ..^ 1 ) \/ x e. ( 1 ..^ N ) ) )
65 62 63 64 sylancl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ x e. ( 0 ..^ N ) ) -> ( x e. ( 0 ..^ 1 ) \/ x e. ( 1 ..^ N ) ) )
66 65 ord 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ x e. ( 0 ..^ N ) ) -> ( -. x e. ( 0 ..^ 1 ) -> x e. ( 1 ..^ N ) ) )
67 61 66 syld 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ x e. ( 0 ..^ N ) ) -> ( ( x gcd N ) = 1 -> x e. ( 1 ..^ N ) ) )
68 67 ralrimiva 
 |-  ( N e. ( ZZ>= ` 2 ) -> A. x e. ( 0 ..^ N ) ( ( x gcd N ) = 1 -> x e. ( 1 ..^ N ) ) )
69 rabss 
 |-  ( { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } C_ ( 1 ..^ N ) <-> A. x e. ( 0 ..^ N ) ( ( x gcd N ) = 1 -> x e. ( 1 ..^ N ) ) )
70 68 69 sylibr 
 |-  ( N e. ( ZZ>= ` 2 ) -> { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } C_ ( 1 ..^ N ) )
71 dfss2 
 |-  ( { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } C_ ( 1 ..^ N ) <-> ( { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } i^i ( 1 ..^ N ) ) = { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } )
72 70 71 sylib 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } i^i ( 1 ..^ N ) ) = { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } )
73 38 45 72 3eqtr3d 
 |-  ( N e. ( ZZ>= ` 2 ) -> { x e. ( 1 ... N ) | ( x gcd N ) = 1 } = { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } )
74 73 fveq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) = ( # ` { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } ) )
75 26 74 eqtrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( phi ` N ) = ( # ` { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } ) )
76 23 75 jaoi 
 |-  ( ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) -> ( phi ` N ) = ( # ` { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } ) )
77 1 76 sylbi 
 |-  ( N e. NN -> ( phi ` N ) = ( # ` { x e. ( 0 ..^ N ) | ( x gcd N ) = 1 } ) )