Metamath Proof Explorer

Theorem modm1div

Description: An integer greater than one divides another integer minus one iff the second integer modulo the first integer is one. (Contributed by AV, 30-May-2023)

		Ref	Expression
	Assertion	modm1div	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ) \to (A \mod N = 1 \leftrightarrow N ∥ (A - 1))$

Proof

Step	Hyp	Ref	Expression
1		eluzelre	$⊢ N \in ℤ_{\geq 2} \to N \in ℝ$
2		eluz2gt1	$⊢ N \in ℤ_{\geq 2} \to 1 < N$
3	2	adantr	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ) \to 1 < N$
4		1mod	$⊢ (N \in ℝ \land 1 < N) \to 1 \mod N = 1$
5	4	eqcomd	$⊢ (N \in ℝ \land 1 < N) \to 1 = 1 \mod N$
6	1 3 5	syl2an2r	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ) \to 1 = 1 \mod N$
7	6	eqeq2d	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ) \to (A \mod N = 1 \leftrightarrow A \mod N = 1 \mod N)$
8		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
9	8	adantr	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ) \to N \in ℕ$
10		simpr	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ) \to A \in ℤ$
11		1zzd	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ) \to 1 \in ℤ$
12		moddvds	$⊢ (N \in ℕ \land A \in ℤ \land 1 \in ℤ) \to (A \mod N = 1 \mod N \leftrightarrow N ∥ (A - 1))$
13	9 10 11 12	syl3anc	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ) \to (A \mod N = 1 \mod N \leftrightarrow N ∥ (A - 1))$
14	7 13	bitrd	$⊢ (N \in ℤ_{\geq 2} \land A \in ℤ) \to (A \mod N = 1 \leftrightarrow N ∥ (A - 1))$