Metamath Proof Explorer

Theorem odzphi

Description: The order of any group element is a divisor of the Euler phi function. (Contributed by Mario Carneiro, 28-Feb-2014)

Ref Expression
Assertion odzphi 
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( odZ ` N ) ` A ) || ( phi ` N ) )

Proof

Step Hyp Ref Expression
1 eulerth 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( A ^ ( phi ` N ) ) mod N ) = ( 1 mod N ) )
2 simp1 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> N e. NN )
3 simp2 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> A e. ZZ )
4 2 phicld 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( phi ` N ) e. NN )
5 4 nnnn0d 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( phi ` N ) e. NN0 )
6 zexpcl 
 |-  ( ( A e. ZZ /\ ( phi ` N ) e. NN0 ) -> ( A ^ ( phi ` N ) ) e. ZZ )
7 3 5 6 syl2anc 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( A ^ ( phi ` N ) ) e. ZZ )
8 1zzd 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> 1 e. ZZ )
9 moddvds 
 |-  ( ( N e. NN /\ ( A ^ ( phi ` N ) ) e. ZZ /\ 1 e. ZZ ) -> ( ( ( A ^ ( phi ` N ) ) mod N ) = ( 1 mod N ) <-> N || ( ( A ^ ( phi ` N ) ) - 1 ) ) )
10 2 7 8 9 syl3anc 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( ( A ^ ( phi ` N ) ) mod N ) = ( 1 mod N ) <-> N || ( ( A ^ ( phi ` N ) ) - 1 ) ) )
11 1 10 mpbid 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> N || ( ( A ^ ( phi ` N ) ) - 1 ) )
12 odzdvds 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ ( phi ` N ) e. NN0 ) -> ( N || ( ( A ^ ( phi ` N ) ) - 1 ) <-> ( ( odZ ` N ) ` A ) || ( phi ` N ) ) )
13 5 12 mpdan 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( N || ( ( A ^ ( phi ` N ) ) - 1 ) <-> ( ( odZ ` N ) ` A ) || ( phi ` N ) ) )
14 11 13 mpbid 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( odZ ` N ) ` A ) || ( phi ` N ) )