Theorem ndvdsi

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

	Ref	Expression
Hypotheses	ndvdsi.1	$$⊢A\in \mathbb{N}$$
	ndvdsi.2	$$⊢Q\in {\mathbb{N}}_0$$
	ndvdsi.3	$$⊢R\in \mathbb{N}$$
	ndvdsi.4	$$⊢AQ+R=B$$
	ndvdsi.5	$$⊢R<A$$
Assertion	ndvdsi	$$⊢\neg A\parallel B$$

Proof

Step	Hyp	Ref	Expression
1		ndvdsi.1	$$⊢A\in \mathbb{N}$$
2		ndvdsi.2	$$⊢Q\in {\mathbb{N}}_0$$
3		ndvdsi.3	$$⊢R\in \mathbb{N}$$
4		ndvdsi.4	$$⊢AQ+R=B$$
5		ndvdsi.5	$$⊢R<A$$
6	1	nnzi	$$⊢A\in \mathbb{Z}$$
7	2	nn0zi	$$⊢Q\in \mathbb{Z}$$
8		dvdsmul1	$$⊢\left(A\in \mathbb{Z}\wedge Q\in \mathbb{Z}\right)\to A\parallel AQ$$
9	6 7 8	mp2an	$$⊢A\parallel AQ$$
10		zmulcl	$$⊢\left(A\in \mathbb{Z}\wedge Q\in \mathbb{Z}\right)\to AQ\in \mathbb{Z}$$
11	6 7 10	mp2an	$$⊢AQ\in \mathbb{Z}$$
12	3 5	pm3.2i	$$⊢\left(R\in \mathbb{N}\wedge R<A\right)$$
13		ndvdsadd	$$⊢\left(AQ\in \mathbb{Z}\wedge A\in \mathbb{N}\wedge \left(R\in \mathbb{N}\wedge R<A\right)\right)\to \left(A\parallel AQ\to \neg A\parallel \left(AQ+R\right)\right)$$
14	11 1 12 13	mp3an	$$⊢A\parallel AQ\to \neg A\parallel \left(AQ+R\right)$$
15	9 14	ax-mp	$$⊢\neg A\parallel \left(AQ+R\right)$$
16	4	breq2i	$$⊢A\parallel \left(AQ+R\right)\leftrightarrow A\parallel B$$
17	15 16	mtbi	$$⊢\neg A\parallel B$$