This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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