Metamath Proof Explorer

Theorem rpdvds

Description: If K is relatively prime to N then it is also relatively prime to any divisor M of N . (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Assertion rpdvds ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( 𝐾 gcd 𝑀 ) = 1 )

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → 𝐾 ∈ ℤ )
2 simpl2 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → 𝑀 ∈ ℤ )
3 gcddvds ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝐾 gcd 𝑀 ) ∥ 𝐾 ∧ ( 𝐾 gcd 𝑀 ) ∥ 𝑀 ) )
4 1 2 3 syl2anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( ( 𝐾 gcd 𝑀 ) ∥ 𝐾 ∧ ( 𝐾 gcd 𝑀 ) ∥ 𝑀 ) )
5 4 simpld ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( 𝐾 gcd 𝑀 ) ∥ 𝐾 )
6 4 simprd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( 𝐾 gcd 𝑀 ) ∥ 𝑀 )
7 simprr ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → 𝑀 ∥ 𝑁 )
8 ax-1ne0 ⊢ 1 ≠ 0
9 simprl ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( 𝐾 gcd 𝑁 ) = 1 )
10 9 neeq1d ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( ( 𝐾 gcd 𝑁 ) ≠ 0 ↔ 1 ≠ 0 ) )
11 8 10 mpbiri ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( 𝐾 gcd 𝑁 ) ≠ 0 )
12 11 neneqd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ¬ ( 𝐾 gcd 𝑁 ) = 0 )
13 simprl ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) ∧ ( 𝐾 = 0 ∧ 𝑀 = 0 ) ) → 𝐾 = 0 )
14 simprr ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) ∧ ( 𝐾 = 0 ∧ 𝑀 = 0 ) ) → 𝑀 = 0 )
15 simplrr ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) ∧ ( 𝐾 = 0 ∧ 𝑀 = 0 ) ) → 𝑀 ∥ 𝑁 )
16 14 15 eqbrtrrd ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) ∧ ( 𝐾 = 0 ∧ 𝑀 = 0 ) ) → 0 ∥ 𝑁 )
17 simpll3 ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) ∧ ( 𝐾 = 0 ∧ 𝑀 = 0 ) ) → 𝑁 ∈ ℤ )
18 0dvds ⊢ ( 𝑁 ∈ ℤ → ( 0 ∥ 𝑁 ↔ 𝑁 = 0 ) )
19 17 18 syl ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) ∧ ( 𝐾 = 0 ∧ 𝑀 = 0 ) ) → ( 0 ∥ 𝑁 ↔ 𝑁 = 0 ) )
20 16 19 mpbid ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) ∧ ( 𝐾 = 0 ∧ 𝑀 = 0 ) ) → 𝑁 = 0 )
21 13 20 jca ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) ∧ ( 𝐾 = 0 ∧ 𝑀 = 0 ) ) → ( 𝐾 = 0 ∧ 𝑁 = 0 ) )
22 21 ex ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( ( 𝐾 = 0 ∧ 𝑀 = 0 ) → ( 𝐾 = 0 ∧ 𝑁 = 0 ) ) )
23 simpl3 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → 𝑁 ∈ ℤ )
24 gcdeq0 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 gcd 𝑁 ) = 0 ↔ ( 𝐾 = 0 ∧ 𝑁 = 0 ) ) )
25 1 23 24 syl2anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( ( 𝐾 gcd 𝑁 ) = 0 ↔ ( 𝐾 = 0 ∧ 𝑁 = 0 ) ) )
26 22 25 sylibrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( ( 𝐾 = 0 ∧ 𝑀 = 0 ) → ( 𝐾 gcd 𝑁 ) = 0 ) )
27 12 26 mtod ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ¬ ( 𝐾 = 0 ∧ 𝑀 = 0 ) )
28 gcdn0cl ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ¬ ( 𝐾 = 0 ∧ 𝑀 = 0 ) ) → ( 𝐾 gcd 𝑀 ) ∈ ℕ )
29 1 2 27 28 syl21anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( 𝐾 gcd 𝑀 ) ∈ ℕ )
30 29 nnzd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( 𝐾 gcd 𝑀 ) ∈ ℤ )
31 dvdstr ⊢ ( ( ( 𝐾 gcd 𝑀 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐾 gcd 𝑀 ) ∥ 𝑀 ∧ 𝑀 ∥ 𝑁 ) → ( 𝐾 gcd 𝑀 ) ∥ 𝑁 ) )
32 30 2 23 31 syl3anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( ( ( 𝐾 gcd 𝑀 ) ∥ 𝑀 ∧ 𝑀 ∥ 𝑁 ) → ( 𝐾 gcd 𝑀 ) ∥ 𝑁 ) )
33 6 7 32 mp2and ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( 𝐾 gcd 𝑀 ) ∥ 𝑁 )
34 12 25 mtbid ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ¬ ( 𝐾 = 0 ∧ 𝑁 = 0 ) )
35 dvdslegcd ⊢ ( ( ( ( 𝐾 gcd 𝑀 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝐾 = 0 ∧ 𝑁 = 0 ) ) → ( ( ( 𝐾 gcd 𝑀 ) ∥ 𝐾 ∧ ( 𝐾 gcd 𝑀 ) ∥ 𝑁 ) → ( 𝐾 gcd 𝑀 ) ≤ ( 𝐾 gcd 𝑁 ) ) )
36 30 1 23 34 35 syl31anc ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( ( ( 𝐾 gcd 𝑀 ) ∥ 𝐾 ∧ ( 𝐾 gcd 𝑀 ) ∥ 𝑁 ) → ( 𝐾 gcd 𝑀 ) ≤ ( 𝐾 gcd 𝑁 ) ) )
37 5 33 36 mp2and ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( 𝐾 gcd 𝑀 ) ≤ ( 𝐾 gcd 𝑁 ) )
38 37 9 breqtrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( 𝐾 gcd 𝑀 ) ≤ 1 )
39 nnle1eq1 ⊢ ( ( 𝐾 gcd 𝑀 ) ∈ ℕ → ( ( 𝐾 gcd 𝑀 ) ≤ 1 ↔ ( 𝐾 gcd 𝑀 ) = 1 ) )
40 29 39 syl ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( ( 𝐾 gcd 𝑀 ) ≤ 1 ↔ ( 𝐾 gcd 𝑀 ) = 1 ) )
41 38 40 mpbid ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐾 gcd 𝑁 ) = 1 ∧ 𝑀 ∥ 𝑁 ) ) → ( 𝐾 gcd 𝑀 ) = 1 )