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 \in ℕ \land A \in ℤ \land A \gcd N = 1) \land K \in ℕ_{0}) \to (N ∥ (A^{K} - 1) \leftrightarrow {od}_{ℤ} (N) (A) ∥ K)$

Proof

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

Metamath Proof Explorer

Theorem odzdvds

Proof