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	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 mod 𝑁 ) = 1 ↔ 𝑁 ∥ ( 𝐴 − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eluzelre	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℝ )
2		eluz2gt1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑁 )
3	2	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ) → 1 < 𝑁 )
4		1mod	⊢ ( ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) → ( 1 mod 𝑁 ) = 1 )
5	4	eqcomd	⊢ ( ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) → 1 = ( 1 mod 𝑁 ) )
6	1 3 5	syl2an2r	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ) → 1 = ( 1 mod 𝑁 ) )
7	6	eqeq2d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 mod 𝑁 ) = 1 ↔ ( 𝐴 mod 𝑁 ) = ( 1 mod 𝑁 ) ) )
8		eluz2nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ )
9	8	adantr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ) → 𝑁 ∈ ℕ )
10		simpr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ) → 𝐴 ∈ ℤ )
11		1zzd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ) → 1 ∈ ℤ )
12		moddvds	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( 𝐴 mod 𝑁 ) = ( 1 mod 𝑁 ) ↔ 𝑁 ∥ ( 𝐴 − 1 ) ) )
13	9 10 11 12	syl3anc	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 mod 𝑁 ) = ( 1 mod 𝑁 ) ↔ 𝑁 ∥ ( 𝐴 − 1 ) ) )
14	7 13	bitrd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 mod 𝑁 ) = 1 ↔ 𝑁 ∥ ( 𝐴 − 1 ) ) )