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	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴 − 1 ) → ¬ 𝑃 ∥ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-1ne0	⊢ 1 ≠ 0
2	1	neii	⊢ ¬ 1 = 0
3		eqeq1	⊢ ( 1 = ( 𝐴 mod 𝑃 ) → ( 1 = 0 ↔ ( 𝐴 mod 𝑃 ) = 0 ) )
4	3	eqcoms	⊢ ( ( 𝐴 mod 𝑃 ) = 1 → ( 1 = 0 ↔ ( 𝐴 mod 𝑃 ) = 0 ) )
5	2 4	mtbii	⊢ ( ( 𝐴 mod 𝑃 ) = 1 → ¬ ( 𝐴 mod 𝑃 ) = 0 )
6	5	a1i	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 mod 𝑃 ) = 1 → ¬ ( 𝐴 mod 𝑃 ) = 0 ) )
7		modprm1div	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 mod 𝑃 ) = 1 ↔ 𝑃 ∥ ( 𝐴 − 1 ) ) )
8		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
9		dvdsval3	⊢ ( ( 𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ 𝐴 ↔ ( 𝐴 mod 𝑃 ) = 0 ) )
10	8 9	sylan	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ 𝐴 ↔ ( 𝐴 mod 𝑃 ) = 0 ) )
11	10	bicomd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 mod 𝑃 ) = 0 ↔ 𝑃 ∥ 𝐴 ) )
12	11	notbid	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ¬ ( 𝐴 mod 𝑃 ) = 0 ↔ ¬ 𝑃 ∥ 𝐴 ) )
13	6 7 12	3imtr3d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴 − 1 ) → ¬ 𝑃 ∥ 𝐴 ) )