Metamath Proof Explorer

Theorem odzdvds

Description: The only powers of A that are congruent to 1 are the multiples of the order of A . (Contributed by Mario Carneiro, 28-Feb-2014) (Proof shortened by AV, 26-Sep-2020)

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

Proof

Step Hyp Ref Expression
1 nn0re 
 |-  ( K e. NN0 -> K e. RR )
2 1 adantl 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> K e. RR )
3 odzcl 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( odZ ` N ) ` A ) e. NN )
4 3 adantr 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( odZ ` N ) ` A ) e. NN )
5 4 nnrpd 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( odZ ` N ) ` A ) e. RR+ )
6 modlt 
 |-  ( ( K e. RR /\ ( ( odZ ` N ) ` A ) e. RR+ ) -> ( K mod ( ( odZ ` N ) ` A ) ) < ( ( odZ ` N ) ` A ) )
7 2 5 6 syl2anc 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( K mod ( ( odZ ` N ) ` A ) ) < ( ( odZ ` N ) ` A ) )
8 nn0z 
 |-  ( K e. NN0 -> K e. ZZ )
9 8 adantl 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> K e. ZZ )
10 9 4 zmodcld 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( K mod ( ( odZ ` N ) ` A ) ) e. NN0 )
11 10 nn0red 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( K mod ( ( odZ ` N ) ` A ) ) e. RR )
12 4 nnred 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( odZ ` N ) ` A ) e. RR )
13 11 12 ltnled 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( K mod ( ( odZ ` N ) ` A ) ) < ( ( odZ ` N ) ` A ) <-> -. ( ( odZ ` N ) ` A ) <_ ( K mod ( ( odZ ` N ) ` A ) ) ) )
14 7 13 mpbid 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> -. ( ( odZ ` N ) ` A ) <_ ( K mod ( ( odZ ` N ) ` A ) ) )
15 oveq2 
 |-  ( n = ( K mod ( ( odZ ` N ) ` A ) ) -> ( A ^ n ) = ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) )
16 15 oveq1d 
 |-  ( n = ( K mod ( ( odZ ` N ) ` A ) ) -> ( ( A ^ n ) - 1 ) = ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) )
17 16 breq2d 
 |-  ( n = ( K mod ( ( odZ ` N ) ` A ) ) -> ( N || ( ( A ^ n ) - 1 ) <-> N || ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) ) )
18 17 elrab 
 |-  ( ( K mod ( ( odZ ` N ) ` A ) ) e. { n e. NN | N || ( ( A ^ n ) - 1 ) } <-> ( ( K mod ( ( odZ ` N ) ` A ) ) e. NN /\ N || ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) ) )
19 ssrab2 
 |-  { n e. NN | N || ( ( A ^ n ) - 1 ) } C_ NN
20 nnuz 
 |-  NN = ( ZZ>= ` 1 )
21 19 20 sseqtri 
 |-  { n e. NN | N || ( ( A ^ n ) - 1 ) } C_ ( ZZ>= ` 1 )
22 infssuzle 
 |-  ( ( { n e. NN | N || ( ( A ^ n ) - 1 ) } C_ ( ZZ>= ` 1 ) /\ ( K mod ( ( odZ ` N ) ` A ) ) e. { n e. NN | N || ( ( A ^ n ) - 1 ) } ) -> inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) <_ ( K mod ( ( odZ ` N ) ` A ) ) )
23 21 22 mpan 
 |-  ( ( K mod ( ( odZ ` N ) ` A ) ) e. { n e. NN | N || ( ( A ^ n ) - 1 ) } -> inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) <_ ( K mod ( ( odZ ` N ) ` A ) ) )
24 18 23 sylbir 
 |-  ( ( ( K mod ( ( odZ ` N ) ` A ) ) e. NN /\ N || ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) ) -> inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) <_ ( K mod ( ( odZ ` N ) ` A ) ) )
25 24 ancoms 
 |-  ( ( N || ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) /\ ( K mod ( ( odZ ` N ) ` A ) ) e. NN ) -> inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) <_ ( K mod ( ( odZ ` N ) ` A ) ) )
26 odzval 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( odZ ` N ) ` A ) = inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) )
27 26 adantr 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( odZ ` N ) ` A ) = inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) )
28 27 breq1d 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( ( odZ ` N ) ` A ) <_ ( K mod ( ( odZ ` N ) ` A ) ) <-> inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) <_ ( K mod ( ( odZ ` N ) ` A ) ) ) )
29 25 28 imbitrrid 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( N || ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) /\ ( K mod ( ( odZ ` N ) ` A ) ) e. NN ) -> ( ( odZ ` N ) ` A ) <_ ( K mod ( ( odZ ` N ) ` A ) ) ) )
30 14 29 mtod 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> -. ( N || ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) /\ ( K mod ( ( odZ ` N ) ` A ) ) e. NN ) )
31 imnan 
 |-  ( ( N || ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) -> -. ( K mod ( ( odZ ` N ) ` A ) ) e. NN ) <-> -. ( N || ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) /\ ( K mod ( ( odZ ` N ) ` A ) ) e. NN ) )
32 30 31 sylibr 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( N || ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) -> -. ( K mod ( ( odZ ` N ) ` A ) ) e. NN ) )
33 elnn0 
 |-  ( ( K mod ( ( odZ ` N ) ` A ) ) e. NN0 <-> ( ( K mod ( ( odZ ` N ) ` A ) ) e. NN \/ ( K mod ( ( odZ ` N ) ` A ) ) = 0 ) )
34 10 33 sylib 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( K mod ( ( odZ ` N ) ` A ) ) e. NN \/ ( K mod ( ( odZ ` N ) ` A ) ) = 0 ) )
35 34 ord 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( -. ( K mod ( ( odZ ` N ) ` A ) ) e. NN -> ( K mod ( ( odZ ` N ) ` A ) ) = 0 ) )
36 32 35 syld 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( N || ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) -> ( K mod ( ( odZ ` N ) ` A ) ) = 0 ) )
37 simpl1 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> N e. NN )
38 37 nnzd 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> N e. ZZ )
39 dvds0 
 |-  ( N e. ZZ -> N || 0 )
40 38 39 syl 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> N || 0 )
41 simpl2 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> A e. ZZ )
42 41 zcnd 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> A e. CC )
43 42 exp0d 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( A ^ 0 ) = 1 )
44 43 oveq1d 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( A ^ 0 ) - 1 ) = ( 1 - 1 ) )
45 1m1e0 
 |-  ( 1 - 1 ) = 0
46 44 45 eqtrdi 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( A ^ 0 ) - 1 ) = 0 )
47 40 46 breqtrrd 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> N || ( ( A ^ 0 ) - 1 ) )
48 oveq2 
 |-  ( ( K mod ( ( odZ ` N ) ` A ) ) = 0 -> ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) = ( A ^ 0 ) )
49 48 oveq1d 
 |-  ( ( K mod ( ( odZ ` N ) ` A ) ) = 0 -> ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) = ( ( A ^ 0 ) - 1 ) )
50 49 breq2d 
 |-  ( ( K mod ( ( odZ ` N ) ` A ) ) = 0 -> ( N || ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) <-> N || ( ( A ^ 0 ) - 1 ) ) )
51 47 50 syl5ibrcom 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( K mod ( ( odZ ` N ) ` A ) ) = 0 -> N || ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) ) )
52 36 51 impbid 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( N || ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) <-> ( K mod ( ( odZ ` N ) ` A ) ) = 0 ) )
53 4 nnnn0d 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( odZ ` N ) ` A ) e. NN0 )
54 2 4 nndivred 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( K / ( ( odZ ` N ) ` A ) ) e. RR )
55 nn0ge0 
 |-  ( K e. NN0 -> 0 <_ K )
56 55 adantl 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> 0 <_ K )
57 4 nngt0d 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> 0 < ( ( odZ ` N ) ` A ) )
58 ge0div 
 |-  ( ( K e. RR /\ ( ( odZ ` N ) ` A ) e. RR /\ 0 < ( ( odZ ` N ) ` A ) ) -> ( 0 <_ K <-> 0 <_ ( K / ( ( odZ ` N ) ` A ) ) ) )
59 2 12 57 58 syl3anc 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( 0 <_ K <-> 0 <_ ( K / ( ( odZ ` N ) ` A ) ) ) )
60 56 59 mpbid 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> 0 <_ ( K / ( ( odZ ` N ) ` A ) ) )
61 flge0nn0 
 |-  ( ( ( K / ( ( odZ ` N ) ` A ) ) e. RR /\ 0 <_ ( K / ( ( odZ ` N ) ` A ) ) ) -> ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) e. NN0 )
62 54 60 61 syl2anc 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) e. NN0 )
63 53 62 nn0mulcld 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) e. NN0 )
64 zexpcl 
 |-  ( ( A e. ZZ /\ ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) e. NN0 ) -> ( A ^ ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) ) e. ZZ )
65 41 63 64 syl2anc 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( A ^ ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) ) e. ZZ )
66 65 zred 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( A ^ ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) ) e. RR )
67 1red 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> 1 e. RR )
68 zexpcl 
 |-  ( ( A e. ZZ /\ ( K mod ( ( odZ ` N ) ` A ) ) e. NN0 ) -> ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) e. ZZ )
69 41 10 68 syl2anc 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) e. ZZ )
70 37 nnrpd 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> N e. RR+ )
71 42 62 53 expmuld 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( A ^ ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) ) = ( ( A ^ ( ( odZ ` N ) ` A ) ) ^ ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) )
72 71 oveq1d 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( A ^ ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) ) mod N ) = ( ( ( A ^ ( ( odZ ` N ) ` A ) ) ^ ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) mod N ) )
73 zexpcl 
 |-  ( ( A e. ZZ /\ ( ( odZ ` N ) ` A ) e. NN0 ) -> ( A ^ ( ( odZ ` N ) ` A ) ) e. ZZ )
74 41 53 73 syl2anc 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( A ^ ( ( odZ ` N ) ` A ) ) e. ZZ )
75 1zzd 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> 1 e. ZZ )
76 odzid 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> N || ( ( A ^ ( ( odZ ` N ) ` A ) ) - 1 ) )
77 76 adantr 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> N || ( ( A ^ ( ( odZ ` N ) ` A ) ) - 1 ) )
78 moddvds 
 |-  ( ( N e. NN /\ ( A ^ ( ( odZ ` N ) ` A ) ) e. ZZ /\ 1 e. ZZ ) -> ( ( ( A ^ ( ( odZ ` N ) ` A ) ) mod N ) = ( 1 mod N ) <-> N || ( ( A ^ ( ( odZ ` N ) ` A ) ) - 1 ) ) )
79 37 74 75 78 syl3anc 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( ( A ^ ( ( odZ ` N ) ` A ) ) mod N ) = ( 1 mod N ) <-> N || ( ( A ^ ( ( odZ ` N ) ` A ) ) - 1 ) ) )
80 77 79 mpbird 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( A ^ ( ( odZ ` N ) ` A ) ) mod N ) = ( 1 mod N ) )
81 modexp 
 |-  ( ( ( ( A ^ ( ( odZ ` N ) ` A ) ) e. ZZ /\ 1 e. ZZ ) /\ ( ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) e. NN0 /\ N e. RR+ ) /\ ( ( A ^ ( ( odZ ` N ) ` A ) ) mod N ) = ( 1 mod N ) ) -> ( ( ( A ^ ( ( odZ ` N ) ` A ) ) ^ ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) mod N ) = ( ( 1 ^ ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) mod N ) )
82 74 75 62 70 80 81 syl221anc 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( ( A ^ ( ( odZ ` N ) ` A ) ) ^ ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) mod N ) = ( ( 1 ^ ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) mod N ) )
83 54 flcld 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) e. ZZ )
84 1exp 
 |-  ( ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) e. ZZ -> ( 1 ^ ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) = 1 )
85 83 84 syl 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( 1 ^ ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) = 1 )
86 85 oveq1d 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( 1 ^ ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) mod N ) = ( 1 mod N ) )
87 72 82 86 3eqtrd 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( A ^ ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) ) mod N ) = ( 1 mod N ) )
88 modmul1 
 |-  ( ( ( ( A ^ ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) ) e. RR /\ 1 e. RR ) /\ ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) e. ZZ /\ N e. RR+ ) /\ ( ( A ^ ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) ) mod N ) = ( 1 mod N ) ) -> ( ( ( A ^ ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) ) x. ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) ) mod N ) = ( ( 1 x. ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) ) mod N ) )
89 66 67 69 70 87 88 syl221anc 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( ( A ^ ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) ) x. ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) ) mod N ) = ( ( 1 x. ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) ) mod N ) )
90 42 10 63 expaddd 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( A ^ ( ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) + ( K mod ( ( odZ ` N ) ` A ) ) ) ) = ( ( A ^ ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) ) x. ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) ) )
91 modval 
 |-  ( ( K e. RR /\ ( ( odZ ` N ) ` A ) e. RR+ ) -> ( K mod ( ( odZ ` N ) ` A ) ) = ( K - ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) ) )
92 2 5 91 syl2anc 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( K mod ( ( odZ ` N ) ` A ) ) = ( K - ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) ) )
93 92 oveq2d 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) + ( K mod ( ( odZ ` N ) ` A ) ) ) = ( ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) + ( K - ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) ) ) )
94 63 nn0cnd 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) e. CC )
95 2 recnd 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> K e. CC )
96 94 95 pncan3d 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) + ( K - ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) ) ) = K )
97 93 96 eqtrd 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) + ( K mod ( ( odZ ` N ) ` A ) ) ) = K )
98 97 oveq2d 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( A ^ ( ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) + ( K mod ( ( odZ ` N ) ` A ) ) ) ) = ( A ^ K ) )
99 90 98 eqtr3d 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( A ^ ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) ) x. ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) ) = ( A ^ K ) )
100 99 oveq1d 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( ( A ^ ( ( ( odZ ` N ) ` A ) x. ( |_ ` ( K / ( ( odZ ` N ) ` A ) ) ) ) ) x. ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) ) mod N ) = ( ( A ^ K ) mod N ) )
101 69 zcnd 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) e. CC )
102 101 mullidd 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( 1 x. ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) ) = ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) )
103 102 oveq1d 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( 1 x. ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) ) mod N ) = ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) mod N ) )
104 89 100 103 3eqtr3d 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( A ^ K ) mod N ) = ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) mod N ) )
105 104 eqeq1d 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( ( A ^ K ) mod N ) = ( 1 mod N ) <-> ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) mod N ) = ( 1 mod N ) ) )
106 zexpcl 
 |-  ( ( A e. ZZ /\ K e. NN0 ) -> ( A ^ K ) e. ZZ )
107 41 106 sylancom 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( A ^ K ) e. ZZ )
108 moddvds 
 |-  ( ( N e. NN /\ ( A ^ K ) e. ZZ /\ 1 e. ZZ ) -> ( ( ( A ^ K ) mod N ) = ( 1 mod N ) <-> N || ( ( A ^ K ) - 1 ) ) )
109 37 107 75 108 syl3anc 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( ( A ^ K ) mod N ) = ( 1 mod N ) <-> N || ( ( A ^ K ) - 1 ) ) )
110 moddvds 
 |-  ( ( N e. NN /\ ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) e. ZZ /\ 1 e. ZZ ) -> ( ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) mod N ) = ( 1 mod N ) <-> N || ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) ) )
111 37 69 75 110 syl3anc 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) mod N ) = ( 1 mod N ) <-> N || ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) ) )
112 105 109 111 3bitr3d 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( N || ( ( A ^ K ) - 1 ) <-> N || ( ( A ^ ( K mod ( ( odZ ` N ) ` A ) ) ) - 1 ) ) )
113 dvdsval3 
 |-  ( ( ( ( odZ ` N ) ` A ) e. NN /\ K e. ZZ ) -> ( ( ( odZ ` N ) ` A ) || K <-> ( K mod ( ( odZ ` N ) ` A ) ) = 0 ) )
114 4 9 113 syl2anc 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( ( ( odZ ` N ) ` A ) || K <-> ( K mod ( ( odZ ` N ) ` A ) ) = 0 ) )
115 52 112 114 3bitr4d 
 |-  ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 ) -> ( N || ( ( A ^ K ) - 1 ) <-> ( ( odZ ` N ) ` A ) || K ) )