Metamath Proof Explorer

Theorem divalg

Description: The division algorithm (theorem). Dividing an integer N by a nonzero integer D produces a (unique) quotient q and a unique remainder 0 <_ r < ( absD ) . Theorem 1.14 in ApostolNT p. 19. The proof does not use / or |_ or mod . (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( N = if ( N e. ZZ , N , 1 ) -> ( N = ( ( q x. D ) + r ) <-> if ( N e. ZZ , N , 1 ) = ( ( q x. D ) + r ) ) )
2 1 3anbi3d 
 |-  ( N = if ( N e. ZZ , N , 1 ) -> ( ( 0 <_ r /\ r < ( abs ` D ) /\ N = ( ( q x. D ) + r ) ) <-> ( 0 <_ r /\ r < ( abs ` D ) /\ if ( N e. ZZ , N , 1 ) = ( ( q x. D ) + r ) ) ) )
3 2 rexbidv 
 |-  ( N = if ( N e. ZZ , N , 1 ) -> ( E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ N = ( ( q x. D ) + r ) ) <-> E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ if ( N e. ZZ , N , 1 ) = ( ( q x. D ) + r ) ) ) )
4 3 reubidv 
 |-  ( N = if ( N e. ZZ , N , 1 ) -> ( E! r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ N = ( ( q x. D ) + r ) ) <-> E! r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ if ( N e. ZZ , N , 1 ) = ( ( q x. D ) + r ) ) ) )
5 fveq2 
 |-  ( D = if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) -> ( abs ` D ) = ( abs ` if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) ) )
6 5 breq2d 
 |-  ( D = if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) -> ( r < ( abs ` D ) <-> r < ( abs ` if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) ) ) )
7 oveq2 
 |-  ( D = if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) -> ( q x. D ) = ( q x. if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) ) )
8 7 oveq1d 
 |-  ( D = if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) -> ( ( q x. D ) + r ) = ( ( q x. if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) ) + r ) )
9 8 eqeq2d 
 |-  ( D = if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) -> ( if ( N e. ZZ , N , 1 ) = ( ( q x. D ) + r ) <-> if ( N e. ZZ , N , 1 ) = ( ( q x. if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) ) + r ) ) )
10 6 9 3anbi23d 
 |-  ( D = if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) -> ( ( 0 <_ r /\ r < ( abs ` D ) /\ if ( N e. ZZ , N , 1 ) = ( ( q x. D ) + r ) ) <-> ( 0 <_ r /\ r < ( abs ` if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) ) /\ if ( N e. ZZ , N , 1 ) = ( ( q x. if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) ) + r ) ) ) )
11 10 rexbidv 
 |-  ( D = if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) -> ( E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ if ( N e. ZZ , N , 1 ) = ( ( q x. D ) + r ) ) <-> E. q e. ZZ ( 0 <_ r /\ r < ( abs ` if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) ) /\ if ( N e. ZZ , N , 1 ) = ( ( q x. if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) ) + r ) ) ) )
12 11 reubidv 
 |-  ( D = if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) -> ( E! r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ if ( N e. ZZ , N , 1 ) = ( ( q x. D ) + r ) ) <-> E! r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) ) /\ if ( N e. ZZ , N , 1 ) = ( ( q x. if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) ) + r ) ) ) )
13 1z 
 |-  1 e. ZZ
14 13 elimel 
 |-  if ( N e. ZZ , N , 1 ) e. ZZ
15 simpl 
 |-  ( ( D e. ZZ /\ D =/= 0 ) -> D e. ZZ )
16 eleq1 
 |-  ( D = if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) -> ( D e. ZZ <-> if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) e. ZZ ) )
17 eleq1 
 |-  ( 1 = if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) -> ( 1 e. ZZ <-> if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) e. ZZ ) )
18 15 16 17 13 elimdhyp 
 |-  if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) e. ZZ
19 simpr 
 |-  ( ( D e. ZZ /\ D =/= 0 ) -> D =/= 0 )
20 neeq1 
 |-  ( D = if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) -> ( D =/= 0 <-> if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) =/= 0 ) )
21 neeq1 
 |-  ( 1 = if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) -> ( 1 =/= 0 <-> if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) =/= 0 ) )
22 ax-1ne0 
 |-  1 =/= 0
23 19 20 21 22 elimdhyp 
 |-  if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) =/= 0
24 eqid 
 |-  { r e. NN0 | if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) || ( if ( N e. ZZ , N , 1 ) - r ) } = { r e. NN0 | if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) || ( if ( N e. ZZ , N , 1 ) - r ) }
25 14 18 23 24 divalglem10 
 |-  E! r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) ) /\ if ( N e. ZZ , N , 1 ) = ( ( q x. if ( ( D e. ZZ /\ D =/= 0 ) , D , 1 ) ) + r ) )
26 4 12 25 dedth2h 
 |-  ( ( 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 ) ) )
27 26 3impb 
 |-  ( ( 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 ) ) )