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 bitrid ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑅 = ( 𝑁 mod 𝐷 ) ↔ 𝑅 ∈ { 𝑧 ∈ ℕ0 ∣ ( 𝑧 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑧 ) ) } ) )
55 breq1 ⊢ ( 𝑧 = 𝑅 → ( 𝑧 < 𝐷 ↔ 𝑅 < 𝐷 ) )
56 oveq2 ⊢ ( 𝑧 = 𝑅 → ( 𝑁 − 𝑧 ) = ( 𝑁 − 𝑅 ) )
57 56 breq2d ⊢ ( 𝑧 = 𝑅 → ( 𝐷 ∥ ( 𝑁 − 𝑧 ) ↔ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) )
58 55 57 anbi12d ⊢ ( 𝑧 = 𝑅 → ( ( 𝑧 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑧 ) ) ↔ ( 𝑅 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) )
59 58 elrab ⊢ ( 𝑅 ∈ { 𝑧 ∈ ℕ0 ∣ ( 𝑧 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑧 ) ) } ↔ ( 𝑅 ∈ ℕ0 ∧ ( 𝑅 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) )
60 54 59 bitrdi ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑅 = ( 𝑁 mod 𝐷 ) ↔ ( 𝑅 ∈ ℕ0 ∧ ( 𝑅 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) ) )