This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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