Metamath Proof Explorer

Theorem hashgcdeq

Description: Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Assertion hashgcdeq 
|- ( ( M e. NN /\ N e. NN ) -> ( # ` { x e. ( 0 ..^ M ) | ( x gcd M ) = N } ) = if ( N || M , ( phi ` ( M / N ) ) , 0 ) )

Proof

Step Hyp Ref Expression
1 eqeq2 
 |-  ( ( phi ` ( M / N ) ) = if ( N || M , ( phi ` ( M / N ) ) , 0 ) -> ( ( # ` { x e. ( 0 ..^ M ) | ( x gcd M ) = N } ) = ( phi ` ( M / N ) ) <-> ( # ` { x e. ( 0 ..^ M ) | ( x gcd M ) = N } ) = if ( N || M , ( phi ` ( M / N ) ) , 0 ) ) )
2 eqeq2 
 |-  ( 0 = if ( N || M , ( phi ` ( M / N ) ) , 0 ) -> ( ( # ` { x e. ( 0 ..^ M ) | ( x gcd M ) = N } ) = 0 <-> ( # ` { x e. ( 0 ..^ M ) | ( x gcd M ) = N } ) = if ( N || M , ( phi ` ( M / N ) ) , 0 ) ) )
3 nndivdvds 
 |-  ( ( M e. NN /\ N e. NN ) -> ( N || M <-> ( M / N ) e. NN ) )
4 3 biimpa 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ N || M ) -> ( M / N ) e. NN )
5 dfphi2 
 |-  ( ( M / N ) e. NN -> ( phi ` ( M / N ) ) = ( # ` { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 } ) )
6 4 5 syl 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ N || M ) -> ( phi ` ( M / N ) ) = ( # ` { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 } ) )
7 eqid 
 |-  { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 } = { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 }
8 eqid 
 |-  { x e. ( 0 ..^ M ) | ( x gcd M ) = N } = { x e. ( 0 ..^ M ) | ( x gcd M ) = N }
9 eqid 
 |-  ( z e. { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 } |-> ( z x. N ) ) = ( z e. { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 } |-> ( z x. N ) )
10 7 8 9 hashgcdlem 
 |-  ( ( M e. NN /\ N e. NN /\ N || M ) -> ( z e. { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 } |-> ( z x. N ) ) : { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 } -1-1-onto-> { x e. ( 0 ..^ M ) | ( x gcd M ) = N } )
11 10 3expa 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ N || M ) -> ( z e. { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 } |-> ( z x. N ) ) : { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 } -1-1-onto-> { x e. ( 0 ..^ M ) | ( x gcd M ) = N } )
12 ovex 
 |-  ( 0 ..^ ( M / N ) ) e. _V
13 12 rabex 
 |-  { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 } e. _V
14 13 f1oen 
 |-  ( ( z e. { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 } |-> ( z x. N ) ) : { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 } -1-1-onto-> { x e. ( 0 ..^ M ) | ( x gcd M ) = N } -> { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 } ~~ { x e. ( 0 ..^ M ) | ( x gcd M ) = N } )
15 hasheni 
 |-  ( { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 } ~~ { x e. ( 0 ..^ M ) | ( x gcd M ) = N } -> ( # ` { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 } ) = ( # ` { x e. ( 0 ..^ M ) | ( x gcd M ) = N } ) )
16 11 14 15 3syl 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ N || M ) -> ( # ` { y e. ( 0 ..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 } ) = ( # ` { x e. ( 0 ..^ M ) | ( x gcd M ) = N } ) )
17 6 16 eqtr2d 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ N || M ) -> ( # ` { x e. ( 0 ..^ M ) | ( x gcd M ) = N } ) = ( phi ` ( M / N ) ) )
18 simprr 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ ( x e. ( 0 ..^ M ) /\ ( x gcd M ) = N ) ) -> ( x gcd M ) = N )
19 elfzoelz 
 |-  ( x e. ( 0 ..^ M ) -> x e. ZZ )
20 19 ad2antrl 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ ( x e. ( 0 ..^ M ) /\ ( x gcd M ) = N ) ) -> x e. ZZ )
21 nnz 
 |-  ( M e. NN -> M e. ZZ )
22 21 ad2antrr 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ ( x e. ( 0 ..^ M ) /\ ( x gcd M ) = N ) ) -> M e. ZZ )
23 gcddvds 
 |-  ( ( x e. ZZ /\ M e. ZZ ) -> ( ( x gcd M ) || x /\ ( x gcd M ) || M ) )
24 20 22 23 syl2anc 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ ( x e. ( 0 ..^ M ) /\ ( x gcd M ) = N ) ) -> ( ( x gcd M ) || x /\ ( x gcd M ) || M ) )
25 24 simprd 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ ( x e. ( 0 ..^ M ) /\ ( x gcd M ) = N ) ) -> ( x gcd M ) || M )
26 18 25 eqbrtrrd 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ ( x e. ( 0 ..^ M ) /\ ( x gcd M ) = N ) ) -> N || M )
27 26 expr 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ x e. ( 0 ..^ M ) ) -> ( ( x gcd M ) = N -> N || M ) )
28 27 con3d 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ x e. ( 0 ..^ M ) ) -> ( -. N || M -> -. ( x gcd M ) = N ) )
29 28 impancom 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ -. N || M ) -> ( x e. ( 0 ..^ M ) -> -. ( x gcd M ) = N ) )
30 29 ralrimiv 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ -. N || M ) -> A. x e. ( 0 ..^ M ) -. ( x gcd M ) = N )
31 rabeq0 
 |-  ( { x e. ( 0 ..^ M ) | ( x gcd M ) = N } = (/) <-> A. x e. ( 0 ..^ M ) -. ( x gcd M ) = N )
32 30 31 sylibr 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ -. N || M ) -> { x e. ( 0 ..^ M ) | ( x gcd M ) = N } = (/) )
33 32 fveq2d 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ -. N || M ) -> ( # ` { x e. ( 0 ..^ M ) | ( x gcd M ) = N } ) = ( # ` (/) ) )
34 hash0 
 |-  ( # ` (/) ) = 0
35 33 34 eqtrdi 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ -. N || M ) -> ( # ` { x e. ( 0 ..^ M ) | ( x gcd M ) = N } ) = 0 )
36 1 2 17 35 ifbothda 
 |-  ( ( M e. NN /\ N e. NN ) -> ( # ` { x e. ( 0 ..^ M ) | ( x gcd M ) = N } ) = if ( N || M , ( phi ` ( M / N ) ) , 0 ) )