Metamath Proof Explorer

Theorem eulerthlem1

Description: Lemma for eulerth . (Contributed by Mario Carneiro, 8-May-2015)

Ref Expression
Hypotheses eulerth.1 
|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )
eulerth.2 
|- S = { y e. ( 0 ..^ N ) | ( y gcd N ) = 1 }
eulerth.3 
|- T = ( 1 ... ( phi ` N ) )
eulerth.4 
|- ( ph -> F : T -1-1-onto-> S )
eulerth.5 
|- G = ( x e. T |-> ( ( A x. ( F ` x ) ) mod N ) )
Assertion eulerthlem1 
|- ( ph -> G : T --> S )

Proof

Step Hyp Ref Expression
1 eulerth.1 
 |-  ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )
2 eulerth.2 
 |-  S = { y e. ( 0 ..^ N ) | ( y gcd N ) = 1 }
3 eulerth.3 
 |-  T = ( 1 ... ( phi ` N ) )
4 eulerth.4 
 |-  ( ph -> F : T -1-1-onto-> S )
5 eulerth.5 
 |-  G = ( x e. T |-> ( ( A x. ( F ` x ) ) mod N ) )
6 1 simp2d 
 |-  ( ph -> A e. ZZ )
7 6 adantr 
 |-  ( ( ph /\ x e. T ) -> A e. ZZ )
8 f1of 
 |-  ( F : T -1-1-onto-> S -> F : T --> S )
9 4 8 syl 
 |-  ( ph -> F : T --> S )
10 9 ffvelcdmda 
 |-  ( ( ph /\ x e. T ) -> ( F ` x ) e. S )
11 oveq1 
 |-  ( y = ( F ` x ) -> ( y gcd N ) = ( ( F ` x ) gcd N ) )
12 11 eqeq1d 
 |-  ( y = ( F ` x ) -> ( ( y gcd N ) = 1 <-> ( ( F ` x ) gcd N ) = 1 ) )
13 12 2 elrab2 
 |-  ( ( F ` x ) e. S <-> ( ( F ` x ) e. ( 0 ..^ N ) /\ ( ( F ` x ) gcd N ) = 1 ) )
14 10 13 sylib 
 |-  ( ( ph /\ x e. T ) -> ( ( F ` x ) e. ( 0 ..^ N ) /\ ( ( F ` x ) gcd N ) = 1 ) )
15 14 simpld 
 |-  ( ( ph /\ x e. T ) -> ( F ` x ) e. ( 0 ..^ N ) )
16 elfzoelz 
 |-  ( ( F ` x ) e. ( 0 ..^ N ) -> ( F ` x ) e. ZZ )
17 15 16 syl 
 |-  ( ( ph /\ x e. T ) -> ( F ` x ) e. ZZ )
18 7 17 zmulcld 
 |-  ( ( ph /\ x e. T ) -> ( A x. ( F ` x ) ) e. ZZ )
19 1 simp1d 
 |-  ( ph -> N e. NN )
20 19 adantr 
 |-  ( ( ph /\ x e. T ) -> N e. NN )
21 zmodfzo 
 |-  ( ( ( A x. ( F ` x ) ) e. ZZ /\ N e. NN ) -> ( ( A x. ( F ` x ) ) mod N ) e. ( 0 ..^ N ) )
22 18 20 21 syl2anc 
 |-  ( ( ph /\ x e. T ) -> ( ( A x. ( F ` x ) ) mod N ) e. ( 0 ..^ N ) )
23 modgcd 
 |-  ( ( ( A x. ( F ` x ) ) e. ZZ /\ N e. NN ) -> ( ( ( A x. ( F ` x ) ) mod N ) gcd N ) = ( ( A x. ( F ` x ) ) gcd N ) )
24 18 20 23 syl2anc 
 |-  ( ( ph /\ x e. T ) -> ( ( ( A x. ( F ` x ) ) mod N ) gcd N ) = ( ( A x. ( F ` x ) ) gcd N ) )
25 19 nnzd 
 |-  ( ph -> N e. ZZ )
26 25 adantr 
 |-  ( ( ph /\ x e. T ) -> N e. ZZ )
27 18 26 gcdcomd 
 |-  ( ( ph /\ x e. T ) -> ( ( A x. ( F ` x ) ) gcd N ) = ( N gcd ( A x. ( F ` x ) ) ) )
28 25 6 gcdcomd 
 |-  ( ph -> ( N gcd A ) = ( A gcd N ) )
29 1 simp3d 
 |-  ( ph -> ( A gcd N ) = 1 )
30 28 29 eqtrd 
 |-  ( ph -> ( N gcd A ) = 1 )
31 30 adantr 
 |-  ( ( ph /\ x e. T ) -> ( N gcd A ) = 1 )
32 26 17 gcdcomd 
 |-  ( ( ph /\ x e. T ) -> ( N gcd ( F ` x ) ) = ( ( F ` x ) gcd N ) )
33 14 simprd 
 |-  ( ( ph /\ x e. T ) -> ( ( F ` x ) gcd N ) = 1 )
34 32 33 eqtrd 
 |-  ( ( ph /\ x e. T ) -> ( N gcd ( F ` x ) ) = 1 )
35 rpmul 
 |-  ( ( N e. ZZ /\ A e. ZZ /\ ( F ` x ) e. ZZ ) -> ( ( ( N gcd A ) = 1 /\ ( N gcd ( F ` x ) ) = 1 ) -> ( N gcd ( A x. ( F ` x ) ) ) = 1 ) )
36 26 7 17 35 syl3anc 
 |-  ( ( ph /\ x e. T ) -> ( ( ( N gcd A ) = 1 /\ ( N gcd ( F ` x ) ) = 1 ) -> ( N gcd ( A x. ( F ` x ) ) ) = 1 ) )
37 31 34 36 mp2and 
 |-  ( ( ph /\ x e. T ) -> ( N gcd ( A x. ( F ` x ) ) ) = 1 )
38 24 27 37 3eqtrd 
 |-  ( ( ph /\ x e. T ) -> ( ( ( A x. ( F ` x ) ) mod N ) gcd N ) = 1 )
39 oveq1 
 |-  ( y = ( ( A x. ( F ` x ) ) mod N ) -> ( y gcd N ) = ( ( ( A x. ( F ` x ) ) mod N ) gcd N ) )
40 39 eqeq1d 
 |-  ( y = ( ( A x. ( F ` x ) ) mod N ) -> ( ( y gcd N ) = 1 <-> ( ( ( A x. ( F ` x ) ) mod N ) gcd N ) = 1 ) )
41 40 2 elrab2 
 |-  ( ( ( A x. ( F ` x ) ) mod N ) e. S <-> ( ( ( A x. ( F ` x ) ) mod N ) e. ( 0 ..^ N ) /\ ( ( ( A x. ( F ` x ) ) mod N ) gcd N ) = 1 ) )
42 22 38 41 sylanbrc 
 |-  ( ( ph /\ x e. T ) -> ( ( A x. ( F ` x ) ) mod N ) e. S )
43 42 5 fmptd 
 |-  ( ph -> G : T --> S )