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 ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 ∥ ( ( 𝐴 ↑ 𝐾 ) − 1 ) ↔ ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) ∥ 𝐾 ) )

Proof

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