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	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ¬ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → ¬ 𝐾 ∥ ( 𝑀 + 𝑁 ) ) )