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