Metamath Proof Explorer

Theorem aks4d1p8d1

Description: If a prime divides one number M , but not another number N , then it divides the quotient of M and the gcd of M and N . (Contributed by Thierry Arnoux, 10-Nov-2024)

Ref Expression
Hypotheses aks4d1p8d1.1 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks4d1p8d1.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
aks4d1p8d1.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
aks4d1p8d1.4 ⊢ ( 𝜑 → 𝑃 ∥ 𝑀 )
aks4d1p8d1.5 ⊢ ( 𝜑 → ¬ 𝑃 ∥ 𝑁 )
Assertion aks4d1p8d1 ( 𝜑 → 𝑃 ∥ ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 aks4d1p8d1.1 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
2 aks4d1p8d1.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3 aks4d1p8d1.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 aks4d1p8d1.4 ⊢ ( 𝜑 → 𝑃 ∥ 𝑀 )
5 aks4d1p8d1.5 ⊢ ( 𝜑 → ¬ 𝑃 ∥ 𝑁 )
6 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
7 1 6 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
8 7 nnzd ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
9 gcdnncl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 gcd 𝑁 ) ∈ ℕ )
10 2 3 9 syl2anc ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) ∈ ℕ )
11 10 nnzd ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) ∈ ℤ )
12 2 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
13 5 intnand ⊢ ( 𝜑 → ¬ ( 𝑃 ∥ 𝑀 ∧ 𝑃 ∥ 𝑁 ) )
14 3 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
15 dvdsgcdb ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 ∥ 𝑀 ∧ 𝑃 ∥ 𝑁 ) ↔ 𝑃 ∥ ( 𝑀 gcd 𝑁 ) ) )
16 8 12 14 15 syl3anc ⊢ ( 𝜑 → ( ( 𝑃 ∥ 𝑀 ∧ 𝑃 ∥ 𝑁 ) ↔ 𝑃 ∥ ( 𝑀 gcd 𝑁 ) ) )
17 13 16 mtbid ⊢ ( 𝜑 → ¬ 𝑃 ∥ ( 𝑀 gcd 𝑁 ) )
18 coprm ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 gcd 𝑁 ) ∈ ℤ ) → ( ¬ 𝑃 ∥ ( 𝑀 gcd 𝑁 ) ↔ ( 𝑃 gcd ( 𝑀 gcd 𝑁 ) ) = 1 ) )
19 18 biimpa ⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑀 gcd 𝑁 ) ∈ ℤ ) ∧ ¬ 𝑃 ∥ ( 𝑀 gcd 𝑁 ) ) → ( 𝑃 gcd ( 𝑀 gcd 𝑁 ) ) = 1 )
20 1 11 17 19 syl21anc ⊢ ( 𝜑 → ( 𝑃 gcd ( 𝑀 gcd 𝑁 ) ) = 1 )
21 gcddvds ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) )
22 12 14 21 syl2anc ⊢ ( 𝜑 → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) )
23 22 simpld ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) ∥ 𝑀 )
24 8 11 12 20 4 23 coprmdvds2d ⊢ ( 𝜑 → ( 𝑃 · ( 𝑀 gcd 𝑁 ) ) ∥ 𝑀 )
25 7 10 2 nnproddivdvdsd ⊢ ( 𝜑 → ( ( 𝑃 · ( 𝑀 gcd 𝑁 ) ) ∥ 𝑀 ↔ 𝑃 ∥ ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) ) )
26 24 25 mpbid ⊢ ( 𝜑 → 𝑃 ∥ ( 𝑀 / ( 𝑀 gcd 𝑁 ) ) )