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 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 ) ) )