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 A A gcd N = 1 K 0 N A K 1 od N A K

Proof

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