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

Metamath Proof Explorer

Theorem divalg2

Description: The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion divalg2 
|- ( ( N e. ZZ /\ D e. NN ) -> E! r e. NN0 ( r < D /\ D || ( N - r ) ) )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( D e. NN -> D e. ZZ )
2 nnne0 
 |-  ( D e. NN -> D =/= 0 )
3 1 2 jca 
 |-  ( D e. NN -> ( D e. ZZ /\ D =/= 0 ) )
4 divalg 
 |-  ( ( N e. ZZ /\ D e. ZZ /\ D =/= 0 ) -> E! r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ N = ( ( q x. D ) + r ) ) )
5 divalgb 
 |-  ( ( N e. ZZ /\ D e. ZZ /\ D =/= 0 ) -> ( E! r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ N = ( ( q x. D ) + r ) ) <-> E! r e. NN0 ( r < ( abs ` D ) /\ D || ( N - r ) ) ) )
6 4 5 mpbid 
 |-  ( ( N e. ZZ /\ D e. ZZ /\ D =/= 0 ) -> E! r e. NN0 ( r < ( abs ` D ) /\ D || ( N - r ) ) )
7 6 3expb 
 |-  ( ( N e. ZZ /\ ( D e. ZZ /\ D =/= 0 ) ) -> E! r e. NN0 ( r < ( abs ` D ) /\ D || ( N - r ) ) )
8 3 7 sylan2 
 |-  ( ( N e. ZZ /\ D e. NN ) -> E! r e. NN0 ( r < ( abs ` D ) /\ D || ( N - r ) ) )
9 nnre 
 |-  ( D e. NN -> D e. RR )
10 nnnn0 
 |-  ( D e. NN -> D e. NN0 )
11 10 nn0ge0d 
 |-  ( D e. NN -> 0 <_ D )
12 9 11 absidd 
 |-  ( D e. NN -> ( abs ` D ) = D )
13 12 breq2d 
 |-  ( D e. NN -> ( r < ( abs ` D ) <-> r < D ) )
14 13 anbi1d 
 |-  ( D e. NN -> ( ( r < ( abs ` D ) /\ D || ( N - r ) ) <-> ( r < D /\ D || ( N - r ) ) ) )
15 14 reubidv 
 |-  ( D e. NN -> ( E! r e. NN0 ( r < ( abs ` D ) /\ D || ( N - r ) ) <-> E! r e. NN0 ( r < D /\ D || ( N - r ) ) ) )
16 15 adantl 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( E! r e. NN0 ( r < ( abs ` D ) /\ D || ( N - r ) ) <-> E! r e. NN0 ( r < D /\ D || ( N - r ) ) ) )
17 8 16 mpbid 
 |-  ( ( N e. ZZ /\ D e. NN ) -> E! r e. NN0 ( r < D /\ D || ( N - r ) ) )