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	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((\neg K ∥ M \land K ∥ N) \to \neg K ∥ (M + N))$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \in ℤ$
2		zaddcl	$⊢ (M \in ℤ \land N \in ℤ) \to M + N \in ℤ$
3	2	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M + N \in ℤ$
4		simp3	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to N \in ℤ$
5	1 3 4	3jca	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in ℤ \land M + N \in ℤ \land N \in ℤ)$
6	5	ad2antrr	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K ∥ N) \land K ∥ (M + N)) \to (K \in ℤ \land M + N \in ℤ \land N \in ℤ)$
7		pm3.22	$⊢ (K ∥ N \land K ∥ (M + N)) \to (K ∥ (M + N) \land K ∥ N)$
8	7	adantll	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K ∥ N) \land K ∥ (M + N)) \to (K ∥ (M + N) \land K ∥ N)$
9		dvds2sub	$⊢ (K \in ℤ \land M + N \in ℤ \land N \in ℤ) \to ((K ∥ (M + N) \land K ∥ N) \to K ∥ (M + N - N))$
10	6 8 9	sylc	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K ∥ N) \land K ∥ (M + N)) \to K ∥ (M + N - N)$
11		zcn	$⊢ M \in ℤ \to M \in ℂ$
12	11	3ad2ant2	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M \in ℂ$
13	12	ad2antrr	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K ∥ N) \land K ∥ (M + N)) \to M \in ℂ$
14	4	zcnd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to N \in ℂ$
15	14	ad2antrr	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K ∥ N) \land K ∥ (M + N)) \to N \in ℂ$
16	13 15	pncand	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K ∥ N) \land K ∥ (M + N)) \to M + N - N = M$
17	10 16	breqtrd	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land K ∥ N) \land K ∥ (M + N)) \to K ∥ M$
18	17	adantlrl	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (\neg K ∥ M \land K ∥ N)) \land K ∥ (M + N)) \to K ∥ M$
19		simplrl	$⊢ (((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (\neg K ∥ M \land K ∥ N)) \land K ∥ (M + N)) \to \neg K ∥ M$
20	18 19	pm2.65da	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (\neg K ∥ M \land K ∥ N)) \to \neg K ∥ (M + N)$
21	20	ex	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((\neg K ∥ M \land K ∥ N) \to \neg K ∥ (M + N))$

Metamath Proof Explorer

Theorem dvdsn1add

Proof