Metamath Proof Explorer

Theorem modm1div

Description: A number greater than 1 divides an integer minus 1 iff the integer modulo the number is 1. (Contributed by AV, 30-May-2023)

Ref Expression
Assertion modm1div 
|- ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ ) -> ( ( A mod N ) = 1 <-> N || ( A - 1 ) ) )

Proof

Step Hyp Ref Expression
1 eluzelre 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. RR )
2 eluz2gt1 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 < N )
3 2 adantr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ ) -> 1 < N )
4 1mod 
 |-  ( ( N e. RR /\ 1 < N ) -> ( 1 mod N ) = 1 )
5 4 eqcomd 
 |-  ( ( N e. RR /\ 1 < N ) -> 1 = ( 1 mod N ) )
6 1 3 5 syl2an2r 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ ) -> 1 = ( 1 mod N ) )
7 6 eqeq2d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ ) -> ( ( A mod N ) = 1 <-> ( A mod N ) = ( 1 mod N ) ) )
8 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
9 8 adantr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ ) -> N e. NN )
10 simpr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ ) -> A e. ZZ )
11 1zzd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ ) -> 1 e. ZZ )
12 moddvds 
 |-  ( ( N e. NN /\ A e. ZZ /\ 1 e. ZZ ) -> ( ( A mod N ) = ( 1 mod N ) <-> N || ( A - 1 ) ) )
13 9 10 11 12 syl3anc 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ ) -> ( ( A mod N ) = ( 1 mod N ) <-> N || ( A - 1 ) ) )
14 7 13 bitrd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ ) -> ( ( A mod N ) = 1 <-> N || ( A - 1 ) ) )