odzcllem

Description: - Lemma for odzcl , showing existence of a recurrent point for the exponential. (Contributed by Mario Carneiro, 28-Feb-2014) (Proof shortened by AV, 26-Sep-2020)

		Ref	Expression
	Assertion	odzcllem	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to ({od}_{ℤ} (N) (A) \in ℕ \land N ∥ (A^{{od}_{ℤ} (N) (A)} - 1))$

Proof

Step	Hyp	Ref	Expression
1		odzval	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to {od}_{ℤ} (N) (A) = inf (\{n \in ℕ \| N ∥ (A^{n} - 1)\} ℝ <)$
2		ssrab2	$⊢ \{n \in ℕ \| N ∥ (A^{n} - 1)\} \subseteq ℕ$
3		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
4	2 3	sseqtri	$⊢ \{n \in ℕ \| N ∥ (A^{n} - 1)\} \subseteq ℤ_{\geq 1}$
5		phicl	$⊢ N \in ℕ \to ϕ (N) \in ℕ$
6	5	3ad2ant1	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to ϕ (N) \in ℕ$
7		eulerth	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to A^{ϕ (N)} \mod N = 1 \mod N$
8		simp1	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to N \in ℕ$
9		simp2	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to A \in ℤ$
10	6	nnnn0d	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to ϕ (N) \in ℕ_{0}$
11		zexpcl	$⊢ (A \in ℤ \land ϕ (N) \in ℕ_{0}) \to A^{ϕ (N)} \in ℤ$
12	9 10 11	syl2anc	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to A^{ϕ (N)} \in ℤ$
13		1z	$⊢ 1 \in ℤ$
14		moddvds	$⊢ (N \in ℕ \land A^{ϕ (N)} \in ℤ \land 1 \in ℤ) \to (A^{ϕ (N)} \mod N = 1 \mod N \leftrightarrow N ∥ (A^{ϕ (N)} - 1))$
15	13 14	mp3an3	$⊢ (N \in ℕ \land A^{ϕ (N)} \in ℤ) \to (A^{ϕ (N)} \mod N = 1 \mod N \leftrightarrow N ∥ (A^{ϕ (N)} - 1))$
16	8 12 15	syl2anc	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to (A^{ϕ (N)} \mod N = 1 \mod N \leftrightarrow N ∥ (A^{ϕ (N)} - 1))$
17	7 16	mpbid	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to N ∥ (A^{ϕ (N)} - 1)$
18		oveq2	$⊢ n = ϕ (N) \to A^{n} = A^{ϕ (N)}$
19	18	oveq1d	$⊢ n = ϕ (N) \to A^{n} - 1 = A^{ϕ (N)} - 1$
20	19	breq2d	$⊢ n = ϕ (N) \to (N ∥ (A^{n} - 1) \leftrightarrow N ∥ (A^{ϕ (N)} - 1))$
21	20	rspcev	$⊢ (ϕ (N) \in ℕ \land N ∥ (A^{ϕ (N)} - 1)) \to \exists n \in ℕ N ∥ (A^{n} - 1)$
22	6 17 21	syl2anc	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to \exists n \in ℕ N ∥ (A^{n} - 1)$
23		rabn0	$⊢ \{n \in ℕ \| N ∥ (A^{n} - 1)\} \neq \emptyset \leftrightarrow \exists n \in ℕ N ∥ (A^{n} - 1)$
24	22 23	sylibr	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to \{n \in ℕ \| N ∥ (A^{n} - 1)\} \neq \emptyset$
25		infssuzcl	$⊢ (\{n \in ℕ \| N ∥ (A^{n} - 1)\} \subseteq ℤ_{\geq 1} \land \{n \in ℕ \| N ∥ (A^{n} - 1)\} \neq \emptyset) \to inf (\{n \in ℕ \| N ∥ (A^{n} - 1)\} ℝ <) \in \{n \in ℕ \| N ∥ (A^{n} - 1)\}$
26	4 24 25	sylancr	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to inf (\{n \in ℕ \| N ∥ (A^{n} - 1)\} ℝ <) \in \{n \in ℕ \| N ∥ (A^{n} - 1)\}$
27	1 26	eqeltrd	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to {od}_{ℤ} (N) (A) \in \{n \in ℕ \| N ∥ (A^{n} - 1)\}$
28		oveq2	$⊢ n = {od}_{ℤ} (N) (A) \to A^{n} = A^{{od}_{ℤ} (N) (A)}$
29	28	oveq1d	$⊢ n = {od}_{ℤ} (N) (A) \to A^{n} - 1 = A^{{od}_{ℤ} (N) (A)} - 1$
30	29	breq2d	$⊢ n = {od}_{ℤ} (N) (A) \to (N ∥ (A^{n} - 1) \leftrightarrow N ∥ (A^{{od}_{ℤ} (N) (A)} - 1))$
31	30	elrab	$⊢ {od}_{ℤ} (N) (A) \in \{n \in ℕ \| N ∥ (A^{n} - 1)\} \leftrightarrow ({od}_{ℤ} (N) (A) \in ℕ \land N ∥ (A^{{od}_{ℤ} (N) (A)} - 1))$
32	27 31	sylib	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to ({od}_{ℤ} (N) (A) \in ℕ \land N ∥ (A^{{od}_{ℤ} (N) (A)} - 1))$

Metamath Proof Explorer

Theorem odzcllem

Proof