Metamath Proof Explorer

Theorem odzcllem

Description: - Lemma for odzcl , showing existence of a recurrent point for the exponential. (Contributed by Mario Carneiro, 28-Feb-2014) (Proof shortened by AV, 26-Sep-2020)

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

Proof

Step Hyp Ref Expression
1 odzval 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( odZ ` N ) ` A ) = inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) )
2 ssrab2 
 |-  { n e. NN | N || ( ( A ^ n ) - 1 ) } C_ NN
3 nnuz 
 |-  NN = ( ZZ>= ` 1 )
4 2 3 sseqtri 
 |-  { n e. NN | N || ( ( A ^ n ) - 1 ) } C_ ( ZZ>= ` 1 )
5 phicl 
 |-  ( N e. NN -> ( phi ` N ) e. NN )
6 5 3ad2ant1 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( phi ` N ) e. NN )
7 eulerth 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( A ^ ( phi ` N ) ) mod N ) = ( 1 mod N ) )
8 simp1 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> N e. NN )
9 simp2 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> A e. ZZ )
10 6 nnnn0d 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( phi ` N ) e. NN0 )
11 zexpcl 
 |-  ( ( A e. ZZ /\ ( phi ` N ) e. NN0 ) -> ( A ^ ( phi ` N ) ) e. ZZ )
12 9 10 11 syl2anc 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( A ^ ( phi ` N ) ) e. ZZ )
13 1z 
 |-  1 e. ZZ
14 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 ) ) )
15 13 14 mp3an3 
 |-  ( ( N e. NN /\ ( A ^ ( phi ` N ) ) e. ZZ ) -> ( ( ( A ^ ( phi ` N ) ) mod N ) = ( 1 mod N ) <-> N || ( ( A ^ ( phi ` N ) ) - 1 ) ) )
16 8 12 15 syl2anc 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( ( A ^ ( phi ` N ) ) mod N ) = ( 1 mod N ) <-> N || ( ( A ^ ( phi ` N ) ) - 1 ) ) )
17 7 16 mpbid 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> N || ( ( A ^ ( phi ` N ) ) - 1 ) )
18 oveq2 
 |-  ( n = ( phi ` N ) -> ( A ^ n ) = ( A ^ ( phi ` N ) ) )
19 18 oveq1d 
 |-  ( n = ( phi ` N ) -> ( ( A ^ n ) - 1 ) = ( ( A ^ ( phi ` N ) ) - 1 ) )
20 19 breq2d 
 |-  ( n = ( phi ` N ) -> ( N || ( ( A ^ n ) - 1 ) <-> N || ( ( A ^ ( phi ` N ) ) - 1 ) ) )
21 20 rspcev 
 |-  ( ( ( phi ` N ) e. NN /\ N || ( ( A ^ ( phi ` N ) ) - 1 ) ) -> E. n e. NN N || ( ( A ^ n ) - 1 ) )
22 6 17 21 syl2anc 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> E. n e. NN N || ( ( A ^ n ) - 1 ) )
23 rabn0 
 |-  ( { n e. NN | N || ( ( A ^ n ) - 1 ) } =/= (/) <-> E. n e. NN N || ( ( A ^ n ) - 1 ) )
24 22 23 sylibr 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> { n e. NN | N || ( ( A ^ n ) - 1 ) } =/= (/) )
25 infssuzcl 
 |-  ( ( { n e. NN | N || ( ( A ^ n ) - 1 ) } C_ ( ZZ>= ` 1 ) /\ { n e. NN | N || ( ( A ^ n ) - 1 ) } =/= (/) ) -> inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) e. { n e. NN | N || ( ( A ^ n ) - 1 ) } )
26 4 24 25 sylancr 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) e. { n e. NN | N || ( ( A ^ n ) - 1 ) } )
27 1 26 eqeltrd 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( odZ ` N ) ` A ) e. { n e. NN | N || ( ( A ^ n ) - 1 ) } )
28 oveq2 
 |-  ( n = ( ( odZ ` N ) ` A ) -> ( A ^ n ) = ( A ^ ( ( odZ ` N ) ` A ) ) )
29 28 oveq1d 
 |-  ( n = ( ( odZ ` N ) ` A ) -> ( ( A ^ n ) - 1 ) = ( ( A ^ ( ( odZ ` N ) ` A ) ) - 1 ) )
30 29 breq2d 
 |-  ( n = ( ( odZ ` N ) ` A ) -> ( N || ( ( A ^ n ) - 1 ) <-> N || ( ( A ^ ( ( odZ ` N ) ` A ) ) - 1 ) ) )
31 30 elrab 
 |-  ( ( ( odZ ` N ) ` A ) e. { n e. NN | N || ( ( A ^ n ) - 1 ) } <-> ( ( ( odZ ` N ) ` A ) e. NN /\ N || ( ( A ^ ( ( odZ ` N ) ` A ) ) - 1 ) ) )
32 27 31 sylib 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( ( odZ ` N ) ` A ) e. NN /\ N || ( ( A ^ ( ( odZ ` N ) ` A ) ) - 1 ) ) )