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

Metamath Proof Explorer

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