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 ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑅 = ( 𝑁 mod 𝐷 ) ↔ ( 𝑅 ∈ ℕ0 ∧ ( 𝑅 < 𝐷𝐷 ∥ ( 𝑁𝑅 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ovex ( 𝑁 mod 𝐷 ) ∈ V
2 1 snid ( 𝑁 mod 𝐷 ) ∈ { ( 𝑁 mod 𝐷 ) }
3 eleq1 ( 𝑅 = ( 𝑁 mod 𝐷 ) → ( 𝑅 ∈ { ( 𝑁 mod 𝐷 ) } ↔ ( 𝑁 mod 𝐷 ) ∈ { ( 𝑁 mod 𝐷 ) } ) )
4 2 3 mpbiri ( 𝑅 = ( 𝑁 mod 𝐷 ) → 𝑅 ∈ { ( 𝑁 mod 𝐷 ) } )
5 elsni ( 𝑅 ∈ { ( 𝑁 mod 𝐷 ) } → 𝑅 = ( 𝑁 mod 𝐷 ) )
6 4 5 impbii ( 𝑅 = ( 𝑁 mod 𝐷 ) ↔ 𝑅 ∈ { ( 𝑁 mod 𝐷 ) } )
7 zre ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
8 nnrp ( 𝐷 ∈ ℕ → 𝐷 ∈ ℝ+ )
9 modlt ( ( 𝑁 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝑁 mod 𝐷 ) < 𝐷 )
10 7 8 9 syl2an ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑁 mod 𝐷 ) < 𝐷 )
11 nnre ( 𝐷 ∈ ℕ → 𝐷 ∈ ℝ )
12 nnne0 ( 𝐷 ∈ ℕ → 𝐷 ≠ 0 )
13 redivcl ( ( 𝑁 ∈ ℝ ∧ 𝐷 ∈ ℝ ∧ 𝐷 ≠ 0 ) → ( 𝑁 / 𝐷 ) ∈ ℝ )
14 7 11 12 13 syl3an ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝑁 / 𝐷 ) ∈ ℝ )
15 14 3anidm23 ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑁 / 𝐷 ) ∈ ℝ )
16 15 flcld ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( ⌊ ‘ ( 𝑁 / 𝐷 ) ) ∈ ℤ )
17 nnz ( 𝐷 ∈ ℕ → 𝐷 ∈ ℤ )
18 17 adantl ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → 𝐷 ∈ ℤ )
19 zmodcl ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑁 mod 𝐷 ) ∈ ℕ0 )
20 19 nn0zd ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑁 mod 𝐷 ) ∈ ℤ )
21 zsubcl ( ( 𝑁 ∈ ℤ ∧ ( 𝑁 mod 𝐷 ) ∈ ℤ ) → ( 𝑁 − ( 𝑁 mod 𝐷 ) ) ∈ ℤ )
22 20 21 syldan ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑁 − ( 𝑁 mod 𝐷 ) ) ∈ ℤ )
23 nncn ( 𝐷 ∈ ℕ → 𝐷 ∈ ℂ )
24 23 adantl ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → 𝐷 ∈ ℂ )
25 16 zcnd ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( ⌊ ‘ ( 𝑁 / 𝐷 ) ) ∈ ℂ )
26 24 25 mulcomd ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝐷 · ( ⌊ ‘ ( 𝑁 / 𝐷 ) ) ) = ( ( ⌊ ‘ ( 𝑁 / 𝐷 ) ) · 𝐷 ) )
27 modval ( ( 𝑁 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝑁 mod 𝐷 ) = ( 𝑁 − ( 𝐷 · ( ⌊ ‘ ( 𝑁 / 𝐷 ) ) ) ) )
28 7 8 27 syl2an ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑁 mod 𝐷 ) = ( 𝑁 − ( 𝐷 · ( ⌊ ‘ ( 𝑁 / 𝐷 ) ) ) ) )
29 19 nn0cnd ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑁 mod 𝐷 ) ∈ ℂ )
30 zmulcl ( ( 𝐷 ∈ ℤ ∧ ( ⌊ ‘ ( 𝑁 / 𝐷 ) ) ∈ ℤ ) → ( 𝐷 · ( ⌊ ‘ ( 𝑁 / 𝐷 ) ) ) ∈ ℤ )
31 17 16 30 syl2an2 ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝐷 · ( ⌊ ‘ ( 𝑁 / 𝐷 ) ) ) ∈ ℤ )
32 31 zcnd ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝐷 · ( ⌊ ‘ ( 𝑁 / 𝐷 ) ) ) ∈ ℂ )
33 zcn ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
34 33 adantr ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → 𝑁 ∈ ℂ )
35 29 32 34 subexsub ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( ( 𝑁 mod 𝐷 ) = ( 𝑁 − ( 𝐷 · ( ⌊ ‘ ( 𝑁 / 𝐷 ) ) ) ) ↔ ( 𝐷 · ( ⌊ ‘ ( 𝑁 / 𝐷 ) ) ) = ( 𝑁 − ( 𝑁 mod 𝐷 ) ) ) )
36 28 35 mpbid ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝐷 · ( ⌊ ‘ ( 𝑁 / 𝐷 ) ) ) = ( 𝑁 − ( 𝑁 mod 𝐷 ) ) )
37 26 36 eqtr3d ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑁 / 𝐷 ) ) · 𝐷 ) = ( 𝑁 − ( 𝑁 mod 𝐷 ) ) )
38 dvds0lem ( ( ( ( ⌊ ‘ ( 𝑁 / 𝐷 ) ) ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ ( 𝑁 − ( 𝑁 mod 𝐷 ) ) ∈ ℤ ) ∧ ( ( ⌊ ‘ ( 𝑁 / 𝐷 ) ) · 𝐷 ) = ( 𝑁 − ( 𝑁 mod 𝐷 ) ) ) → 𝐷 ∥ ( 𝑁 − ( 𝑁 mod 𝐷 ) ) )
39 16 18 22 37 38 syl31anc ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → 𝐷 ∥ ( 𝑁 − ( 𝑁 mod 𝐷 ) ) )
40 divalg2 ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ∃! 𝑧 ∈ ℕ0 ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) )
41 breq1 ( 𝑧 = ( 𝑁 mod 𝐷 ) → ( 𝑧 < 𝐷 ↔ ( 𝑁 mod 𝐷 ) < 𝐷 ) )
42 oveq2 ( 𝑧 = ( 𝑁 mod 𝐷 ) → ( 𝑁𝑧 ) = ( 𝑁 − ( 𝑁 mod 𝐷 ) ) )
43 42 breq2d ( 𝑧 = ( 𝑁 mod 𝐷 ) → ( 𝐷 ∥ ( 𝑁𝑧 ) ↔ 𝐷 ∥ ( 𝑁 − ( 𝑁 mod 𝐷 ) ) ) )
44 41 43 anbi12d ( 𝑧 = ( 𝑁 mod 𝐷 ) → ( ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) ↔ ( ( 𝑁 mod 𝐷 ) < 𝐷𝐷 ∥ ( 𝑁 − ( 𝑁 mod 𝐷 ) ) ) ) )
45 44 riota2 ( ( ( 𝑁 mod 𝐷 ) ∈ ℕ0 ∧ ∃! 𝑧 ∈ ℕ0 ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) ) → ( ( ( 𝑁 mod 𝐷 ) < 𝐷𝐷 ∥ ( 𝑁 − ( 𝑁 mod 𝐷 ) ) ) ↔ ( 𝑧 ∈ ℕ0 ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) ) = ( 𝑁 mod 𝐷 ) ) )
46 19 40 45 syl2anc ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( ( ( 𝑁 mod 𝐷 ) < 𝐷𝐷 ∥ ( 𝑁 − ( 𝑁 mod 𝐷 ) ) ) ↔ ( 𝑧 ∈ ℕ0 ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) ) = ( 𝑁 mod 𝐷 ) ) )
47 10 39 46 mpbi2and ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑧 ∈ ℕ0 ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) ) = ( 𝑁 mod 𝐷 ) )
48 47 eqcomd ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑁 mod 𝐷 ) = ( 𝑧 ∈ ℕ0 ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) ) )
49 48 sneqd ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → { ( 𝑁 mod 𝐷 ) } = { ( 𝑧 ∈ ℕ0 ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) ) } )
50 snriota ( ∃! 𝑧 ∈ ℕ0 ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) → { 𝑧 ∈ ℕ0 ∣ ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) } = { ( 𝑧 ∈ ℕ0 ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) ) } )
51 40 50 syl ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → { 𝑧 ∈ ℕ0 ∣ ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) } = { ( 𝑧 ∈ ℕ0 ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) ) } )
52 49 51 eqtr4d ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → { ( 𝑁 mod 𝐷 ) } = { 𝑧 ∈ ℕ0 ∣ ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) } )
53 52 eleq2d ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑅 ∈ { ( 𝑁 mod 𝐷 ) } ↔ 𝑅 ∈ { 𝑧 ∈ ℕ0 ∣ ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) } ) )
54 6 53 syl5bb ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑅 = ( 𝑁 mod 𝐷 ) ↔ 𝑅 ∈ { 𝑧 ∈ ℕ0 ∣ ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) } ) )
55 breq1 ( 𝑧 = 𝑅 → ( 𝑧 < 𝐷𝑅 < 𝐷 ) )
56 oveq2 ( 𝑧 = 𝑅 → ( 𝑁𝑧 ) = ( 𝑁𝑅 ) )
57 56 breq2d ( 𝑧 = 𝑅 → ( 𝐷 ∥ ( 𝑁𝑧 ) ↔ 𝐷 ∥ ( 𝑁𝑅 ) ) )
58 55 57 anbi12d ( 𝑧 = 𝑅 → ( ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) ↔ ( 𝑅 < 𝐷𝐷 ∥ ( 𝑁𝑅 ) ) ) )
59 58 elrab ( 𝑅 ∈ { 𝑧 ∈ ℕ0 ∣ ( 𝑧 < 𝐷𝐷 ∥ ( 𝑁𝑧 ) ) } ↔ ( 𝑅 ∈ ℕ0 ∧ ( 𝑅 < 𝐷𝐷 ∥ ( 𝑁𝑅 ) ) ) )
60 54 59 bitrdi ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑅 = ( 𝑁 mod 𝐷 ) ↔ ( 𝑅 ∈ ℕ0 ∧ ( 𝑅 < 𝐷𝐷 ∥ ( 𝑁𝑅 ) ) ) ) )