ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  odzdvds GIF version

Theorem odzdvds 12228
Description: The only powers of 𝐴 that are congruent to 1 are the multiples of the order of 𝐴. (Contributed by Mario Carneiro, 28-Feb-2014.) (Proof shortened by AV, 26-Sep-2020.)
Assertion
Ref Expression
odzdvds (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝑁 ∥ ((𝐴𝐾) − 1) ↔ ((od𝑁)‘𝐴) ∥ 𝐾))

Proof of Theorem odzdvds
Dummy variable 𝑛 is distinct from all other variables.
StepHypRef Expression
1 nn0z 9262 . . . . . . . . . 10 (𝐾 ∈ ℕ0𝐾 ∈ ℤ)
2 zq 9615 . . . . . . . . . 10 (𝐾 ∈ ℤ → 𝐾 ∈ ℚ)
31, 2syl 14 . . . . . . . . 9 (𝐾 ∈ ℕ0𝐾 ∈ ℚ)
43adantl 277 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈ ℚ)
5 odzcl 12226 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → ((od𝑁)‘𝐴) ∈ ℕ)
65adantr 276 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((od𝑁)‘𝐴) ∈ ℕ)
7 nnq 9622 . . . . . . . . 9 (((od𝑁)‘𝐴) ∈ ℕ → ((od𝑁)‘𝐴) ∈ ℚ)
86, 7syl 14 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((od𝑁)‘𝐴) ∈ ℚ)
96nngt0d 8952 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 0 < ((od𝑁)‘𝐴))
10 modqlt 10319 . . . . . . . 8 ((𝐾 ∈ ℚ ∧ ((od𝑁)‘𝐴) ∈ ℚ ∧ 0 < ((od𝑁)‘𝐴)) → (𝐾 mod ((od𝑁)‘𝐴)) < ((od𝑁)‘𝐴))
114, 8, 9, 10syl3anc 1238 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝐾 mod ((od𝑁)‘𝐴)) < ((od𝑁)‘𝐴))
121adantl 277 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈ ℤ)
1312, 6zmodcld 10331 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ0)
1413nn0zd 9362 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝐾 mod ((od𝑁)‘𝐴)) ∈ ℤ)
156nnzd 9363 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((od𝑁)‘𝐴) ∈ ℤ)
16 zltnle 9288 . . . . . . . 8 (((𝐾 mod ((od𝑁)‘𝐴)) ∈ ℤ ∧ ((od𝑁)‘𝐴) ∈ ℤ) → ((𝐾 mod ((od𝑁)‘𝐴)) < ((od𝑁)‘𝐴) ↔ ¬ ((od𝑁)‘𝐴) ≤ (𝐾 mod ((od𝑁)‘𝐴))))
1714, 15, 16syl2anc 411 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((𝐾 mod ((od𝑁)‘𝐴)) < ((od𝑁)‘𝐴) ↔ ¬ ((od𝑁)‘𝐴) ≤ (𝐾 mod ((od𝑁)‘𝐴))))
1811, 17mpbid 147 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ¬ ((od𝑁)‘𝐴) ≤ (𝐾 mod ((od𝑁)‘𝐴)))
19 1zzd 9269 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) ∧ ((𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ ∧ 𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1))) → 1 ∈ ℤ)
20 nnuz 9552 . . . . . . . . . . 11 ℕ = (ℤ‘1)
2120rabeqi 2730 . . . . . . . . . 10 {𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴𝑛) − 1)} = {𝑛 ∈ (ℤ‘1) ∣ 𝑁 ∥ ((𝐴𝑛) − 1)}
22 oveq2 5877 . . . . . . . . . . . . . . 15 (𝑛 = (𝐾 mod ((od𝑁)‘𝐴)) → (𝐴𝑛) = (𝐴↑(𝐾 mod ((od𝑁)‘𝐴))))
2322oveq1d 5884 . . . . . . . . . . . . . 14 (𝑛 = (𝐾 mod ((od𝑁)‘𝐴)) → ((𝐴𝑛) − 1) = ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1))
2423breq2d 4012 . . . . . . . . . . . . 13 (𝑛 = (𝐾 mod ((od𝑁)‘𝐴)) → (𝑁 ∥ ((𝐴𝑛) − 1) ↔ 𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1)))
2524elrab 2893 . . . . . . . . . . . 12 ((𝐾 mod ((od𝑁)‘𝐴)) ∈ {𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴𝑛) − 1)} ↔ ((𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ ∧ 𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1)))
2625biimpri 133 . . . . . . . . . . 11 (((𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ ∧ 𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1)) → (𝐾 mod ((od𝑁)‘𝐴)) ∈ {𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴𝑛) − 1)})
2726adantl 277 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) ∧ ((𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ ∧ 𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1))) → (𝐾 mod ((od𝑁)‘𝐴)) ∈ {𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴𝑛) − 1)})
28 simp1 997 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → 𝑁 ∈ ℕ)
2928ad3antrrr 492 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) ∧ ((𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ ∧ 𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1))) ∧ 𝑛 ∈ (1...(𝐾 mod ((od𝑁)‘𝐴)))) → 𝑁 ∈ ℕ)
30 simp2 998 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → 𝐴 ∈ ℤ)
3130ad3antrrr 492 . . . . . . . . . . . . 13 (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) ∧ ((𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ ∧ 𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1))) ∧ 𝑛 ∈ (1...(𝐾 mod ((od𝑁)‘𝐴)))) → 𝐴 ∈ ℤ)
32 elfznn 10040 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...(𝐾 mod ((od𝑁)‘𝐴))) → 𝑛 ∈ ℕ)
3332nnnn0d 9218 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...(𝐾 mod ((od𝑁)‘𝐴))) → 𝑛 ∈ ℕ0)
3433adantl 277 . . . . . . . . . . . . 13 (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) ∧ ((𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ ∧ 𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1))) ∧ 𝑛 ∈ (1...(𝐾 mod ((od𝑁)‘𝐴)))) → 𝑛 ∈ ℕ0)
35 zexpcl 10521 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℤ)
3631, 34, 35syl2anc 411 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) ∧ ((𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ ∧ 𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1))) ∧ 𝑛 ∈ (1...(𝐾 mod ((od𝑁)‘𝐴)))) → (𝐴𝑛) ∈ ℤ)
37 peano2zm 9280 . . . . . . . . . . . 12 ((𝐴𝑛) ∈ ℤ → ((𝐴𝑛) − 1) ∈ ℤ)
3836, 37syl 14 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) ∧ ((𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ ∧ 𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1))) ∧ 𝑛 ∈ (1...(𝐾 mod ((od𝑁)‘𝐴)))) → ((𝐴𝑛) − 1) ∈ ℤ)
39 dvdsdc 11789 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ ((𝐴𝑛) − 1) ∈ ℤ) → DECID 𝑁 ∥ ((𝐴𝑛) − 1))
4029, 38, 39syl2anc 411 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) ∧ ((𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ ∧ 𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1))) ∧ 𝑛 ∈ (1...(𝐾 mod ((od𝑁)‘𝐴)))) → DECID 𝑁 ∥ ((𝐴𝑛) − 1))
4119, 21, 27, 40infssuzledc 11934 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) ∧ ((𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ ∧ 𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1))) → inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴𝑛) − 1)}, ℝ, < ) ≤ (𝐾 mod ((od𝑁)‘𝐴)))
4241ex 115 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (((𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ ∧ 𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1)) → inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴𝑛) − 1)}, ℝ, < ) ≤ (𝐾 mod ((od𝑁)‘𝐴))))
4342ancomsd 269 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1) ∧ (𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ) → inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴𝑛) − 1)}, ℝ, < ) ≤ (𝐾 mod ((od𝑁)‘𝐴))))
44 odzval 12224 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → ((od𝑁)‘𝐴) = inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴𝑛) − 1)}, ℝ, < ))
4544adantr 276 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((od𝑁)‘𝐴) = inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴𝑛) − 1)}, ℝ, < ))
4645breq1d 4010 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (((od𝑁)‘𝐴) ≤ (𝐾 mod ((od𝑁)‘𝐴)) ↔ inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴𝑛) − 1)}, ℝ, < ) ≤ (𝐾 mod ((od𝑁)‘𝐴))))
4743, 46sylibrd 169 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1) ∧ (𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ) → ((od𝑁)‘𝐴) ≤ (𝐾 mod ((od𝑁)‘𝐴))))
4818, 47mtod 663 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ¬ (𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1) ∧ (𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ))
49 imnan 690 . . . . 5 ((𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1) → ¬ (𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ) ↔ ¬ (𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1) ∧ (𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ))
5048, 49sylibr 134 . . . 4 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1) → ¬ (𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ))
51 elnn0 9167 . . . . . 6 ((𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ0 ↔ ((𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ ∨ (𝐾 mod ((od𝑁)‘𝐴)) = 0))
5213, 51sylib 122 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ ∨ (𝐾 mod ((od𝑁)‘𝐴)) = 0))
5352ord 724 . . . 4 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (¬ (𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ → (𝐾 mod ((od𝑁)‘𝐴)) = 0))
5450, 53syld 45 . . 3 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1) → (𝐾 mod ((od𝑁)‘𝐴)) = 0))
55 simpl1 1000 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 𝑁 ∈ ℕ)
5655nnzd 9363 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 𝑁 ∈ ℤ)
57 dvds0 11797 . . . . . 6 (𝑁 ∈ ℤ → 𝑁 ∥ 0)
5856, 57syl 14 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 𝑁 ∥ 0)
59 simpl2 1001 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 𝐴 ∈ ℤ)
6059zcnd 9365 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 𝐴 ∈ ℂ)
6160exp0d 10633 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝐴↑0) = 1)
6261oveq1d 5884 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((𝐴↑0) − 1) = (1 − 1))
63 1m1e0 8977 . . . . . 6 (1 − 1) = 0
6462, 63eqtrdi 2226 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((𝐴↑0) − 1) = 0)
6558, 64breqtrrd 4028 . . . 4 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 𝑁 ∥ ((𝐴↑0) − 1))
66 oveq2 5877 . . . . . 6 ((𝐾 mod ((od𝑁)‘𝐴)) = 0 → (𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) = (𝐴↑0))
6766oveq1d 5884 . . . . 5 ((𝐾 mod ((od𝑁)‘𝐴)) = 0 → ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1) = ((𝐴↑0) − 1))
6867breq2d 4012 . . . 4 ((𝐾 mod ((od𝑁)‘𝐴)) = 0 → (𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1) ↔ 𝑁 ∥ ((𝐴↑0) − 1)))
6965, 68syl5ibrcom 157 . . 3 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((𝐾 mod ((od𝑁)‘𝐴)) = 0 → 𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1)))
7054, 69impbid 129 . 2 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1) ↔ (𝐾 mod ((od𝑁)‘𝐴)) = 0))
716nnnn0d 9218 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((od𝑁)‘𝐴) ∈ ℕ0)
72 znq 9613 . . . . . . . . . . 11 ((𝐾 ∈ ℤ ∧ ((od𝑁)‘𝐴) ∈ ℕ) → (𝐾 / ((od𝑁)‘𝐴)) ∈ ℚ)
7312, 6, 72syl2anc 411 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝐾 / ((od𝑁)‘𝐴)) ∈ ℚ)
74 nn0ge0 9190 . . . . . . . . . . . 12 (𝐾 ∈ ℕ0 → 0 ≤ 𝐾)
7574adantl 277 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 0 ≤ 𝐾)
76 nn0re 9174 . . . . . . . . . . . . 13 (𝐾 ∈ ℕ0𝐾 ∈ ℝ)
7776adantl 277 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈ ℝ)
786nnred 8921 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((od𝑁)‘𝐴) ∈ ℝ)
79 ge0div 8817 . . . . . . . . . . . 12 ((𝐾 ∈ ℝ ∧ ((od𝑁)‘𝐴) ∈ ℝ ∧ 0 < ((od𝑁)‘𝐴)) → (0 ≤ 𝐾 ↔ 0 ≤ (𝐾 / ((od𝑁)‘𝐴))))
8077, 78, 9, 79syl3anc 1238 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (0 ≤ 𝐾 ↔ 0 ≤ (𝐾 / ((od𝑁)‘𝐴))))
8175, 80mpbid 147 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 0 ≤ (𝐾 / ((od𝑁)‘𝐴)))
82 flqge0nn0 10279 . . . . . . . . . 10 (((𝐾 / ((od𝑁)‘𝐴)) ∈ ℚ ∧ 0 ≤ (𝐾 / ((od𝑁)‘𝐴))) → (⌊‘(𝐾 / ((od𝑁)‘𝐴))) ∈ ℕ0)
8373, 81, 82syl2anc 411 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (⌊‘(𝐾 / ((od𝑁)‘𝐴))) ∈ ℕ0)
8471, 83nn0mulcld 9223 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴)))) ∈ ℕ0)
85 zexpcl 10521 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴)))) ∈ ℕ0) → (𝐴↑(((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴))))) ∈ ℤ)
8659, 84, 85syl2anc 411 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝐴↑(((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴))))) ∈ ℤ)
87 zq 9615 . . . . . . 7 ((𝐴↑(((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴))))) ∈ ℤ → (𝐴↑(((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴))))) ∈ ℚ)
8886, 87syl 14 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝐴↑(((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴))))) ∈ ℚ)
89 1z 9268 . . . . . . 7 1 ∈ ℤ
90 zq 9615 . . . . . . 7 (1 ∈ ℤ → 1 ∈ ℚ)
9189, 90mp1i 10 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 1 ∈ ℚ)
92 zexpcl 10521 . . . . . . 7 ((𝐴 ∈ ℤ ∧ (𝐾 mod ((od𝑁)‘𝐴)) ∈ ℕ0) → (𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) ∈ ℤ)
9359, 13, 92syl2anc 411 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) ∈ ℤ)
94 nnq 9622 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ∈ ℚ)
9555, 94syl 14 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 𝑁 ∈ ℚ)
9655nngt0d 8952 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 0 < 𝑁)
9760, 83, 71expmuld 10642 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝐴↑(((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴))))) = ((𝐴↑((od𝑁)‘𝐴))↑(⌊‘(𝐾 / ((od𝑁)‘𝐴)))))
9897oveq1d 5884 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((𝐴↑(((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴))))) mod 𝑁) = (((𝐴↑((od𝑁)‘𝐴))↑(⌊‘(𝐾 / ((od𝑁)‘𝐴)))) mod 𝑁))
99 zexpcl 10521 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ ((od𝑁)‘𝐴) ∈ ℕ0) → (𝐴↑((od𝑁)‘𝐴)) ∈ ℤ)
10059, 71, 99syl2anc 411 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝐴↑((od𝑁)‘𝐴)) ∈ ℤ)
101 1zzd 9269 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 1 ∈ ℤ)
102 odzid 12227 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → 𝑁 ∥ ((𝐴↑((od𝑁)‘𝐴)) − 1))
103102adantr 276 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 𝑁 ∥ ((𝐴↑((od𝑁)‘𝐴)) − 1))
104 moddvds 11790 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝐴↑((od𝑁)‘𝐴)) ∈ ℤ ∧ 1 ∈ ℤ) → (((𝐴↑((od𝑁)‘𝐴)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑((od𝑁)‘𝐴)) − 1)))
10555, 100, 101, 104syl3anc 1238 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (((𝐴↑((od𝑁)‘𝐴)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑((od𝑁)‘𝐴)) − 1)))
106103, 105mpbird 167 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((𝐴↑((od𝑁)‘𝐴)) mod 𝑁) = (1 mod 𝑁))
107100, 101, 83, 95, 96, 106modqexp 10632 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (((𝐴↑((od𝑁)‘𝐴))↑(⌊‘(𝐾 / ((od𝑁)‘𝐴)))) mod 𝑁) = ((1↑(⌊‘(𝐾 / ((od𝑁)‘𝐴)))) mod 𝑁))
10873flqcld 10263 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (⌊‘(𝐾 / ((od𝑁)‘𝐴))) ∈ ℤ)
109 1exp 10535 . . . . . . . . 9 ((⌊‘(𝐾 / ((od𝑁)‘𝐴))) ∈ ℤ → (1↑(⌊‘(𝐾 / ((od𝑁)‘𝐴)))) = 1)
110108, 109syl 14 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (1↑(⌊‘(𝐾 / ((od𝑁)‘𝐴)))) = 1)
111110oveq1d 5884 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((1↑(⌊‘(𝐾 / ((od𝑁)‘𝐴)))) mod 𝑁) = (1 mod 𝑁))
11298, 107, 1113eqtrd 2214 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((𝐴↑(((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴))))) mod 𝑁) = (1 mod 𝑁))
11388, 91, 93, 95, 96, 112modqmul1 10363 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (((𝐴↑(((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴))))) · (𝐴↑(𝐾 mod ((od𝑁)‘𝐴)))) mod 𝑁) = ((1 · (𝐴↑(𝐾 mod ((od𝑁)‘𝐴)))) mod 𝑁))
11460, 13, 84expaddd 10641 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝐴↑((((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴)))) + (𝐾 mod ((od𝑁)‘𝐴)))) = ((𝐴↑(((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴))))) · (𝐴↑(𝐾 mod ((od𝑁)‘𝐴)))))
115 modqval 10310 . . . . . . . . . . 11 ((𝐾 ∈ ℚ ∧ ((od𝑁)‘𝐴) ∈ ℚ ∧ 0 < ((od𝑁)‘𝐴)) → (𝐾 mod ((od𝑁)‘𝐴)) = (𝐾 − (((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴))))))
1164, 8, 9, 115syl3anc 1238 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝐾 mod ((od𝑁)‘𝐴)) = (𝐾 − (((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴))))))
117116oveq2d 5885 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴)))) + (𝐾 mod ((od𝑁)‘𝐴))) = ((((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴)))) + (𝐾 − (((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴)))))))
11884nn0cnd 9220 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴)))) ∈ ℂ)
11977recnd 7976 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈ ℂ)
120118, 119pncan3d 8261 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴)))) + (𝐾 − (((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴)))))) = 𝐾)
121117, 120eqtrd 2210 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴)))) + (𝐾 mod ((od𝑁)‘𝐴))) = 𝐾)
122121oveq2d 5885 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝐴↑((((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴)))) + (𝐾 mod ((od𝑁)‘𝐴)))) = (𝐴𝐾))
123114, 122eqtr3d 2212 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((𝐴↑(((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴))))) · (𝐴↑(𝐾 mod ((od𝑁)‘𝐴)))) = (𝐴𝐾))
124123oveq1d 5884 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (((𝐴↑(((od𝑁)‘𝐴) · (⌊‘(𝐾 / ((od𝑁)‘𝐴))))) · (𝐴↑(𝐾 mod ((od𝑁)‘𝐴)))) mod 𝑁) = ((𝐴𝐾) mod 𝑁))
12593zcnd 9365 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) ∈ ℂ)
126125mulid2d 7966 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (1 · (𝐴↑(𝐾 mod ((od𝑁)‘𝐴)))) = (𝐴↑(𝐾 mod ((od𝑁)‘𝐴))))
127126oveq1d 5884 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((1 · (𝐴↑(𝐾 mod ((od𝑁)‘𝐴)))) mod 𝑁) = ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) mod 𝑁))
128113, 124, 1273eqtr3d 2218 . . . 4 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → ((𝐴𝐾) mod 𝑁) = ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) mod 𝑁))
129128eqeq1d 2186 . . 3 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (((𝐴𝐾) mod 𝑁) = (1 mod 𝑁) ↔ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) mod 𝑁) = (1 mod 𝑁)))
130 zexpcl 10521 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝐾 ∈ ℕ0) → (𝐴𝐾) ∈ ℤ)
13159, 130sylancom 420 . . . 4 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝐴𝐾) ∈ ℤ)
132 moddvds 11790 . . . 4 ((𝑁 ∈ ℕ ∧ (𝐴𝐾) ∈ ℤ ∧ 1 ∈ ℤ) → (((𝐴𝐾) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴𝐾) − 1)))
13355, 131, 101, 132syl3anc 1238 . . 3 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (((𝐴𝐾) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴𝐾) − 1)))
134 moddvds 11790 . . . 4 ((𝑁 ∈ ℕ ∧ (𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) ∈ ℤ ∧ 1 ∈ ℤ) → (((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1)))
13555, 93, 101, 134syl3anc 1238 . . 3 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1)))
136129, 133, 1353bitr3d 218 . 2 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝑁 ∥ ((𝐴𝐾) − 1) ↔ 𝑁 ∥ ((𝐴↑(𝐾 mod ((od𝑁)‘𝐴))) − 1)))
137 dvdsval3 11782 . . 3 ((((od𝑁)‘𝐴) ∈ ℕ ∧ 𝐾 ∈ ℤ) → (((od𝑁)‘𝐴) ∥ 𝐾 ↔ (𝐾 mod ((od𝑁)‘𝐴)) = 0))
1386, 12, 137syl2anc 411 . 2 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (((od𝑁)‘𝐴) ∥ 𝐾 ↔ (𝐾 mod ((od𝑁)‘𝐴)) = 0))
13970, 136, 1383bitr4d 220 1 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝑁 ∥ ((𝐴𝐾) − 1) ↔ ((od𝑁)‘𝐴) ∥ 𝐾))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  DECID wdc 834  w3a 978   = wceq 1353  wcel 2148  {crab 2459   class class class wbr 4000  cfv 5212  (class class class)co 5869  infcinf 6976  cr 7801  0cc0 7802  1c1 7803   + caddc 7805   · cmul 7807   < clt 7982  cle 7983  cmin 8118   / cdiv 8618  cn 8908  0cn0 9165  cz 9242  cuz 9517  cq 9608  ...cfz 9995  cfl 10254   mod cmo 10308  cexp 10505  cdvds 11778   gcd cgcd 11926  odcodz 12191
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584  ax-cnex 7893  ax-resscn 7894  ax-1cn 7895  ax-1re 7896  ax-icn 7897  ax-addcl 7898  ax-addrcl 7899  ax-mulcl 7900  ax-mulrcl 7901  ax-addcom 7902  ax-mulcom 7903  ax-addass 7904  ax-mulass 7905  ax-distr 7906  ax-i2m1 7907  ax-0lt1 7908  ax-1rid 7909  ax-0id 7910  ax-rnegex 7911  ax-precex 7912  ax-cnre 7913  ax-pre-ltirr 7914  ax-pre-ltwlin 7915  ax-pre-lttrn 7916  ax-pre-apti 7917  ax-pre-ltadd 7918  ax-pre-mulgt0 7919  ax-pre-mulext 7920  ax-arch 7921  ax-caucvg 7922
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4290  df-po 4293  df-iso 4294  df-iord 4363  df-on 4365  df-ilim 4366  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-isom 5221  df-riota 5825  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-recs 6300  df-irdg 6365  df-frec 6386  df-1o 6411  df-oadd 6415  df-er 6529  df-en 6735  df-dom 6736  df-fin 6737  df-sup 6977  df-inf 6978  df-pnf 7984  df-mnf 7985  df-xr 7986  df-ltxr 7987  df-le 7988  df-sub 8120  df-neg 8121  df-reap 8522  df-ap 8529  df-div 8619  df-inn 8909  df-2 8967  df-3 8968  df-4 8969  df-n0 9166  df-z 9243  df-uz 9518  df-q 9609  df-rp 9641  df-fz 9996  df-fzo 10129  df-fl 10256  df-mod 10309  df-seqfrec 10432  df-exp 10506  df-ihash 10740  df-cj 10835  df-re 10836  df-im 10837  df-rsqrt 10991  df-abs 10992  df-clim 11271  df-proddc 11543  df-dvds 11779  df-gcd 11927  df-odz 12193  df-phi 12194
This theorem is referenced by:  odzphi  12229  pockthlem  12337
  Copyright terms: Public domain W3C validator