Metamath Proof Explorer

Theorem divalgmod

Description: The result of the mod operator satisfies the requirements for the remainder R in the division algorithm for a positive divisor (compare divalg2 and divalgb ). This demonstration theorem justifies the use of mod to yield an explicit remainder from this point forward. (Contributed by Paul Chapman, 31-Mar-2011) (Revised by AV, 21-Aug-2021)

Ref Expression
Assertion divalgmod 
|- ( ( N e. ZZ /\ D e. NN ) -> ( R = ( N mod D ) <-> ( R e. NN0 /\ ( R < D /\ D || ( N - R ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( N mod D ) e. _V
2 1 snid 
 |-  ( N mod D ) e. { ( N mod D ) }
3 eleq1 
 |-  ( R = ( N mod D ) -> ( R e. { ( N mod D ) } <-> ( N mod D ) e. { ( N mod D ) } ) )
4 2 3 mpbiri 
 |-  ( R = ( N mod D ) -> R e. { ( N mod D ) } )
5 elsni 
 |-  ( R e. { ( N mod D ) } -> R = ( N mod D ) )
6 4 5 impbii 
 |-  ( R = ( N mod D ) <-> R e. { ( N mod D ) } )
7 zre 
 |-  ( N e. ZZ -> N e. RR )
8 nnrp 
 |-  ( D e. NN -> D e. RR+ )
9 modlt 
 |-  ( ( N e. RR /\ D e. RR+ ) -> ( N mod D ) < D )
10 7 8 9 syl2an 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( N mod D ) < D )
11 nnre 
 |-  ( D e. NN -> D e. RR )
12 nnne0 
 |-  ( D e. NN -> D =/= 0 )
13 redivcl 
 |-  ( ( N e. RR /\ D e. RR /\ D =/= 0 ) -> ( N / D ) e. RR )
14 7 11 12 13 syl3an 
 |-  ( ( N e. ZZ /\ D e. NN /\ D e. NN ) -> ( N / D ) e. RR )
15 14 3anidm23 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( N / D ) e. RR )
16 15 flcld 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( |_ ` ( N / D ) ) e. ZZ )
17 nnz 
 |-  ( D e. NN -> D e. ZZ )
18 17 adantl 
 |-  ( ( N e. ZZ /\ D e. NN ) -> D e. ZZ )
19 zmodcl 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( N mod D ) e. NN0 )
20 19 nn0zd 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( N mod D ) e. ZZ )
21 zsubcl 
 |-  ( ( N e. ZZ /\ ( N mod D ) e. ZZ ) -> ( N - ( N mod D ) ) e. ZZ )
22 20 21 syldan 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( N - ( N mod D ) ) e. ZZ )
23 nncn 
 |-  ( D e. NN -> D e. CC )
24 23 adantl 
 |-  ( ( N e. ZZ /\ D e. NN ) -> D e. CC )
25 16 zcnd 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( |_ ` ( N / D ) ) e. CC )
26 24 25 mulcomd 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( D x. ( |_ ` ( N / D ) ) ) = ( ( |_ ` ( N / D ) ) x. D ) )
27 modval 
 |-  ( ( N e. RR /\ D e. RR+ ) -> ( N mod D ) = ( N - ( D x. ( |_ ` ( N / D ) ) ) ) )
28 7 8 27 syl2an 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( N mod D ) = ( N - ( D x. ( |_ ` ( N / D ) ) ) ) )
29 19 nn0cnd 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( N mod D ) e. CC )
30 zmulcl 
 |-  ( ( D e. ZZ /\ ( |_ ` ( N / D ) ) e. ZZ ) -> ( D x. ( |_ ` ( N / D ) ) ) e. ZZ )
31 17 16 30 syl2an2 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( D x. ( |_ ` ( N / D ) ) ) e. ZZ )
32 31 zcnd 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( D x. ( |_ ` ( N / D ) ) ) e. CC )
33 zcn 
 |-  ( N e. ZZ -> N e. CC )
34 33 adantr 
 |-  ( ( N e. ZZ /\ D e. NN ) -> N e. CC )
35 29 32 34 subexsub 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( ( N mod D ) = ( N - ( D x. ( |_ ` ( N / D ) ) ) ) <-> ( D x. ( |_ ` ( N / D ) ) ) = ( N - ( N mod D ) ) ) )
36 28 35 mpbid 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( D x. ( |_ ` ( N / D ) ) ) = ( N - ( N mod D ) ) )
37 26 36 eqtr3d 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( ( |_ ` ( N / D ) ) x. D ) = ( N - ( N mod D ) ) )
38 dvds0lem 
 |-  ( ( ( ( |_ ` ( N / D ) ) e. ZZ /\ D e. ZZ /\ ( N - ( N mod D ) ) e. ZZ ) /\ ( ( |_ ` ( N / D ) ) x. D ) = ( N - ( N mod D ) ) ) -> D || ( N - ( N mod D ) ) )
39 16 18 22 37 38 syl31anc 
 |-  ( ( N e. ZZ /\ D e. NN ) -> D || ( N - ( N mod D ) ) )
40 divalg2 
 |-  ( ( N e. ZZ /\ D e. NN ) -> E! z e. NN0 ( z < D /\ D || ( N - z ) ) )
41 breq1 
 |-  ( z = ( N mod D ) -> ( z < D <-> ( N mod D ) < D ) )
42 oveq2 
 |-  ( z = ( N mod D ) -> ( N - z ) = ( N - ( N mod D ) ) )
43 42 breq2d 
 |-  ( z = ( N mod D ) -> ( D || ( N - z ) <-> D || ( N - ( N mod D ) ) ) )
44 41 43 anbi12d 
 |-  ( z = ( N mod D ) -> ( ( z < D /\ D || ( N - z ) ) <-> ( ( N mod D ) < D /\ D || ( N - ( N mod D ) ) ) ) )
45 44 riota2 
 |-  ( ( ( N mod D ) e. NN0 /\ E! z e. NN0 ( z < D /\ D || ( N - z ) ) ) -> ( ( ( N mod D ) < D /\ D || ( N - ( N mod D ) ) ) <-> ( iota_ z e. NN0 ( z < D /\ D || ( N - z ) ) ) = ( N mod D ) ) )
46 19 40 45 syl2anc 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( ( ( N mod D ) < D /\ D || ( N - ( N mod D ) ) ) <-> ( iota_ z e. NN0 ( z < D /\ D || ( N - z ) ) ) = ( N mod D ) ) )
47 10 39 46 mpbi2and 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( iota_ z e. NN0 ( z < D /\ D || ( N - z ) ) ) = ( N mod D ) )
48 47 eqcomd 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( N mod D ) = ( iota_ z e. NN0 ( z < D /\ D || ( N - z ) ) ) )
49 48 sneqd 
 |-  ( ( N e. ZZ /\ D e. NN ) -> { ( N mod D ) } = { ( iota_ z e. NN0 ( z < D /\ D || ( N - z ) ) ) } )
50 snriota 
 |-  ( E! z e. NN0 ( z < D /\ D || ( N - z ) ) -> { z e. NN0 | ( z < D /\ D || ( N - z ) ) } = { ( iota_ z e. NN0 ( z < D /\ D || ( N - z ) ) ) } )
51 40 50 syl 
 |-  ( ( N e. ZZ /\ D e. NN ) -> { z e. NN0 | ( z < D /\ D || ( N - z ) ) } = { ( iota_ z e. NN0 ( z < D /\ D || ( N - z ) ) ) } )
52 49 51 eqtr4d 
 |-  ( ( N e. ZZ /\ D e. NN ) -> { ( N mod D ) } = { z e. NN0 | ( z < D /\ D || ( N - z ) ) } )
53 52 eleq2d 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( R e. { ( N mod D ) } <-> R e. { z e. NN0 | ( z < D /\ D || ( N - z ) ) } ) )
54 6 53 bitrid 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( R = ( N mod D ) <-> R e. { z e. NN0 | ( z < D /\ D || ( N - z ) ) } ) )
55 breq1 
 |-  ( z = R -> ( z < D <-> R < D ) )
56 oveq2 
 |-  ( z = R -> ( N - z ) = ( N - R ) )
57 56 breq2d 
 |-  ( z = R -> ( D || ( N - z ) <-> D || ( N - R ) ) )
58 55 57 anbi12d 
 |-  ( z = R -> ( ( z < D /\ D || ( N - z ) ) <-> ( R < D /\ D || ( N - R ) ) ) )
59 58 elrab 
 |-  ( R e. { z e. NN0 | ( z < D /\ D || ( N - z ) ) } <-> ( R e. NN0 /\ ( R < D /\ D || ( N - R ) ) ) )
60 54 59 bitrdi 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( R = ( N mod D ) <-> ( R e. NN0 /\ ( R < D /\ D || ( N - R ) ) ) ) )