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 ∧ ( 𝑅 < 𝐷 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) ) ) |