Theorem ndvdsi

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

	Ref	Expression
Hypotheses	ndvdsi.1	|- A e. NN
	ndvdsi.2	|- Q e. NN0
	ndvdsi.3	|- R e. NN
	ndvdsi.4	|- ( ( A x. Q ) + R ) = B
	ndvdsi.5	|- R < A
Assertion	ndvdsi	|- -. A || B

Proof

Step	Hyp	Ref	Expression
1		ndvdsi.1	|- A e. NN
2		ndvdsi.2	|- Q e. NN0
3		ndvdsi.3	|- R e. NN
4		ndvdsi.4	|- ( ( A x. Q ) + R ) = B
5		ndvdsi.5	|- R < A
6	1	nnzi	|- A e. ZZ
7	2	nn0zi	|- Q e. ZZ
8		dvdsmul1	|- ( ( A e. ZZ /\ Q e. ZZ ) -> A || ( A x. Q ) )
9	6 7 8	mp2an	|- A || ( A x. Q )
10		zmulcl	|- ( ( A e. ZZ /\ Q e. ZZ ) -> ( A x. Q ) e. ZZ )
11	6 7 10	mp2an	|- ( A x. Q ) e. ZZ
12	3 5	pm3.2i	|- ( R e. NN /\ R < A )
13		ndvdsadd	|- ( ( ( A x. Q ) e. ZZ /\ A e. NN /\ ( R e. NN /\ R < A ) ) -> ( A || ( A x. Q ) -> -. A || ( ( A x. Q ) + R ) ) )
14	11 1 12 13	mp3an	|- ( A || ( A x. Q ) -> -. A || ( ( A x. Q ) + R ) )
15	9 14	ax-mp	|- -. A || ( ( A x. Q ) + R )
16	4	breq2i	|- ( A || ( ( A x. Q ) + R ) <-> A || B )
17	15 16	mtbi	|- -. A || B