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

Metamath Proof Explorer

Theorem dvdsn1add

Description: If K divides N but K does not divide M , then K does not divide ( M + N ) . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Assertion dvdsn1add ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ¬ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → ¬ 𝐾 ∥ ( 𝑀 + 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ℤ )
2 zaddcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
3 2 3adant1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
4 simp3 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
5 1 3 4 3jca ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
6 5 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∥ 𝑁 ) ∧ 𝐾 ∥ ( 𝑀 + 𝑁 ) ) → ( 𝐾 ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
7 pm3.22 ⊢ ( ( 𝐾 ∥ 𝑁 ∧ 𝐾 ∥ ( 𝑀 + 𝑁 ) ) → ( 𝐾 ∥ ( 𝑀 + 𝑁 ) ∧ 𝐾 ∥ 𝑁 ) )
8 7 adantll ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∥ 𝑁 ) ∧ 𝐾 ∥ ( 𝑀 + 𝑁 ) ) → ( 𝐾 ∥ ( 𝑀 + 𝑁 ) ∧ 𝐾 ∥ 𝑁 ) )
9 dvds2sub ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ ( 𝑀 + 𝑁 ) ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ∥ ( ( 𝑀 + 𝑁 ) − 𝑁 ) ) )
10 6 8 9 sylc ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∥ 𝑁 ) ∧ 𝐾 ∥ ( 𝑀 + 𝑁 ) ) → 𝐾 ∥ ( ( 𝑀 + 𝑁 ) − 𝑁 ) )
11 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
12 11 3ad2ant2 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℂ )
13 12 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∥ 𝑁 ) ∧ 𝐾 ∥ ( 𝑀 + 𝑁 ) ) → 𝑀 ∈ ℂ )
14 4 zcnd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℂ )
15 14 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∥ 𝑁 ) ∧ 𝐾 ∥ ( 𝑀 + 𝑁 ) ) → 𝑁 ∈ ℂ )
16 13 15 pncand ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∥ 𝑁 ) ∧ 𝐾 ∥ ( 𝑀 + 𝑁 ) ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
17 10 16 breqtrd ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∥ 𝑁 ) ∧ 𝐾 ∥ ( 𝑀 + 𝑁 ) ) → 𝐾 ∥ 𝑀 )
18 17 adantlrl ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ¬ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ) ∧ 𝐾 ∥ ( 𝑀 + 𝑁 ) ) → 𝐾 ∥ 𝑀 )
19 simplrl ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ¬ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ) ∧ 𝐾 ∥ ( 𝑀 + 𝑁 ) ) → ¬ 𝐾 ∥ 𝑀 )
20 18 19 pm2.65da ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ¬ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ) → ¬ 𝐾 ∥ ( 𝑀 + 𝑁 ) )
21 20 ex ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ¬ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → ¬ 𝐾 ∥ ( 𝑀 + 𝑁 ) ) )