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 ⊢ φ → P ∈ ℙ
aks4d1p8d1.2 ⊢ φ → M ∈ ℕ
aks4d1p8d1.3 ⊢ φ → N ∈ ℕ
aks4d1p8d1.4 ⊢ φ → P ∥ M
aks4d1p8d1.5 ⊢ φ → ¬ P ∥ N
Assertion aks4d1p8d1 ⊢ φ → P ∥ M M gcd N

Proof

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