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 ) ) )