Theorem m1dvdsndvds

Description: If an integer minus 1 is divisible by a prime number, the integer itself is not divisible by this prime number. (Contributed by Alexander van der Vekens, 30-Aug-2018)

	Ref	Expression
Assertion	m1dvdsndvds	|- ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A - 1 ) -> -. P || A ) )

Proof

Step	Hyp	Ref	Expression
1		ax-1ne0	|- 1 =/= 0
2	1	neii	|- -. 1 = 0
3		eqeq1	|- ( 1 = ( A mod P ) -> ( 1 = 0 <-> ( A mod P ) = 0 ) )
4	3	eqcoms	|- ( ( A mod P ) = 1 -> ( 1 = 0 <-> ( A mod P ) = 0 ) )
5	2 4	mtbii	|- ( ( A mod P ) = 1 -> -. ( A mod P ) = 0 )
6	5	a1i	|- ( ( P e. Prime /\ A e. ZZ ) -> ( ( A mod P ) = 1 -> -. ( A mod P ) = 0 ) )
7		modprm1div	|- ( ( P e. Prime /\ A e. ZZ ) -> ( ( A mod P ) = 1 <-> P || ( A - 1 ) ) )
8		prmnn	|- ( P e. Prime -> P e. NN )
9		dvdsval3	|- ( ( P e. NN /\ A e. ZZ ) -> ( P || A <-> ( A mod P ) = 0 ) )
10	8 9	sylan	|- ( ( P e. Prime /\ A e. ZZ ) -> ( P || A <-> ( A mod P ) = 0 ) )
11	10	bicomd	|- ( ( P e. Prime /\ A e. ZZ ) -> ( ( A mod P ) = 0 <-> P || A ) )
12	11	notbid	|- ( ( P e. Prime /\ A e. ZZ ) -> ( -. ( A mod P ) = 0 <-> -. P || A ) )
13	6 7 12	3imtr3d	|- ( ( P e. Prime /\ A e. ZZ ) -> ( P || ( A - 1 ) -> -. P || A ) )