This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℤ ≥ 2 ∧ A ∈ ℤ → A mod N = 1 ↔ N ∥ A − 1

Proof

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