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 ( ( 𝑁 ∈ ( ℤ≥ ‘ 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 ) ) )