ndvdsi

Description: A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014)

Step	Hyp	Ref	Expression
1		ndvdsi.1	$⊢ A \in ℕ$
2		ndvdsi.2	$⊢ Q \in ℕ_{0}$
3		ndvdsi.3	$⊢ R \in ℕ$
4		ndvdsi.4	$⊢ A Q + R = B$
5		ndvdsi.5	$⊢ R < A$
6	1	nnzi	$⊢ A \in ℤ$
7	2	nn0zi	$⊢ Q \in ℤ$
8		dvdsmul1	$⊢ (A \in ℤ \land Q \in ℤ) \to A ∥ A Q$
9	6 7 8	mp2an	$⊢ A ∥ A Q$
10		zmulcl	$⊢ (A \in ℤ \land Q \in ℤ) \to A Q \in ℤ$
11	6 7 10	mp2an	$⊢ A Q \in ℤ$
12	3 5	pm3.2i	$⊢ (R \in ℕ \land R < A)$
13		ndvdsadd	$⊢ (A Q \in ℤ \land A \in ℕ \land (R \in ℕ \land R < A)) \to (A ∥ A Q \to \neg A ∥ (A Q + R))$
14	11 1 12 13	mp3an	$⊢ A ∥ A Q \to \neg A ∥ (A Q + R)$
15	9 14	ax-mp	$⊢ \neg A ∥ (A Q + R)$
16	4	breq2i	$⊢ A ∥ (A Q + R) \leftrightarrow A ∥ B$
17	15 16	mtbi	$⊢ \neg A ∥ B$

Metamath Proof Explorer