Step |
Hyp |
Ref |
Expression |
1 |
|
divalglem8.1 |
⊢ 𝑁 ∈ ℤ |
2 |
|
divalglem8.2 |
⊢ 𝐷 ∈ ℤ |
3 |
|
divalglem8.3 |
⊢ 𝐷 ≠ 0 |
4 |
|
divalglem8.4 |
⊢ 𝑆 = { 𝑟 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑟 ) } |
5 |
4
|
ssrab3 |
⊢ 𝑆 ⊆ ℕ0 |
6 |
|
nn0sscn |
⊢ ℕ0 ⊆ ℂ |
7 |
5 6
|
sstri |
⊢ 𝑆 ⊆ ℂ |
8 |
7
|
sseli |
⊢ ( 𝑌 ∈ 𝑆 → 𝑌 ∈ ℂ ) |
9 |
7
|
sseli |
⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ∈ ℂ ) |
10 |
|
nnabscl |
⊢ ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) → ( abs ‘ 𝐷 ) ∈ ℕ ) |
11 |
2 3 10
|
mp2an |
⊢ ( abs ‘ 𝐷 ) ∈ ℕ |
12 |
11
|
nnzi |
⊢ ( abs ‘ 𝐷 ) ∈ ℤ |
13 |
|
zmulcl |
⊢ ( ( 𝐾 ∈ ℤ ∧ ( abs ‘ 𝐷 ) ∈ ℤ ) → ( 𝐾 · ( abs ‘ 𝐷 ) ) ∈ ℤ ) |
14 |
12 13
|
mpan2 |
⊢ ( 𝐾 ∈ ℤ → ( 𝐾 · ( abs ‘ 𝐷 ) ) ∈ ℤ ) |
15 |
14
|
zcnd |
⊢ ( 𝐾 ∈ ℤ → ( 𝐾 · ( abs ‘ 𝐷 ) ) ∈ ℂ ) |
16 |
|
subadd |
⊢ ( ( 𝑌 ∈ ℂ ∧ 𝑋 ∈ ℂ ∧ ( 𝐾 · ( abs ‘ 𝐷 ) ) ∈ ℂ ) → ( ( 𝑌 − 𝑋 ) = ( 𝐾 · ( abs ‘ 𝐷 ) ) ↔ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) = 𝑌 ) ) |
17 |
8 9 15 16
|
syl3an |
⊢ ( ( 𝑌 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆 ∧ 𝐾 ∈ ℤ ) → ( ( 𝑌 − 𝑋 ) = ( 𝐾 · ( abs ‘ 𝐷 ) ) ↔ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) = 𝑌 ) ) |
18 |
17
|
3com12 |
⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ∧ 𝐾 ∈ ℤ ) → ( ( 𝑌 − 𝑋 ) = ( 𝐾 · ( abs ‘ 𝐷 ) ) ↔ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) = 𝑌 ) ) |
19 |
|
eqcom |
⊢ ( ( 𝑌 − 𝑋 ) = ( 𝐾 · ( abs ‘ 𝐷 ) ) ↔ ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) ) |
20 |
|
eqcom |
⊢ ( ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) = 𝑌 ↔ 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ) |
21 |
18 19 20
|
3bitr3g |
⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) ↔ 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ) ) |
22 |
21
|
3adant1r |
⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ 𝑌 ∈ 𝑆 ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) ↔ 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ) ) |
23 |
22
|
3adant2r |
⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) ↔ 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ) ) |
24 |
|
breq1 |
⊢ ( 𝑧 = 𝑌 → ( 𝑧 < ( abs ‘ 𝐷 ) ↔ 𝑌 < ( abs ‘ 𝐷 ) ) ) |
25 |
|
eleq1 |
⊢ ( 𝑧 = 𝑌 → ( 𝑧 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ↔ 𝑌 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) |
26 |
24 25
|
imbi12d |
⊢ ( 𝑧 = 𝑌 → ( ( 𝑧 < ( abs ‘ 𝐷 ) → 𝑧 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ↔ ( 𝑌 < ( abs ‘ 𝐷 ) → 𝑌 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) ) |
27 |
5
|
sseli |
⊢ ( 𝑧 ∈ 𝑆 → 𝑧 ∈ ℕ0 ) |
28 |
|
elnn0z |
⊢ ( 𝑧 ∈ ℕ0 ↔ ( 𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ) ) |
29 |
27 28
|
sylib |
⊢ ( 𝑧 ∈ 𝑆 → ( 𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ) ) |
30 |
29
|
anim1i |
⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑧 < ( abs ‘ 𝐷 ) ) → ( ( 𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ) ∧ 𝑧 < ( abs ‘ 𝐷 ) ) ) |
31 |
|
df-3an |
⊢ ( ( 𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ∧ 𝑧 < ( abs ‘ 𝐷 ) ) ↔ ( ( 𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ) ∧ 𝑧 < ( abs ‘ 𝐷 ) ) ) |
32 |
30 31
|
sylibr |
⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑧 < ( abs ‘ 𝐷 ) ) → ( 𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ∧ 𝑧 < ( abs ‘ 𝐷 ) ) ) |
33 |
|
0z |
⊢ 0 ∈ ℤ |
34 |
|
elfzm11 |
⊢ ( ( 0 ∈ ℤ ∧ ( abs ‘ 𝐷 ) ∈ ℤ ) → ( 𝑧 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ↔ ( 𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ∧ 𝑧 < ( abs ‘ 𝐷 ) ) ) ) |
35 |
33 12 34
|
mp2an |
⊢ ( 𝑧 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ↔ ( 𝑧 ∈ ℤ ∧ 0 ≤ 𝑧 ∧ 𝑧 < ( abs ‘ 𝐷 ) ) ) |
36 |
32 35
|
sylibr |
⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑧 < ( abs ‘ 𝐷 ) ) → 𝑧 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) |
37 |
36
|
ex |
⊢ ( 𝑧 ∈ 𝑆 → ( 𝑧 < ( abs ‘ 𝐷 ) → 𝑧 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) |
38 |
26 37
|
vtoclga |
⊢ ( 𝑌 ∈ 𝑆 → ( 𝑌 < ( abs ‘ 𝐷 ) → 𝑌 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) |
39 |
|
eleq1 |
⊢ ( 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) → ( 𝑌 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ↔ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) |
40 |
39
|
biimpd |
⊢ ( 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) → ( 𝑌 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) → ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) |
41 |
38 40
|
sylan9 |
⊢ ( ( 𝑌 ∈ 𝑆 ∧ 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ) → ( 𝑌 < ( abs ‘ 𝐷 ) → ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) |
42 |
41
|
impancom |
⊢ ( ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) → ( 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) → ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) |
43 |
42
|
3ad2ant2 |
⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) → ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) |
44 |
|
breq1 |
⊢ ( 𝑧 = 𝑋 → ( 𝑧 < ( abs ‘ 𝐷 ) ↔ 𝑋 < ( abs ‘ 𝐷 ) ) ) |
45 |
|
eleq1 |
⊢ ( 𝑧 = 𝑋 → ( 𝑧 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ↔ 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) |
46 |
44 45
|
imbi12d |
⊢ ( 𝑧 = 𝑋 → ( ( 𝑧 < ( abs ‘ 𝐷 ) → 𝑧 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ↔ ( 𝑋 < ( abs ‘ 𝐷 ) → 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) ) |
47 |
46 37
|
vtoclga |
⊢ ( 𝑋 ∈ 𝑆 → ( 𝑋 < ( abs ‘ 𝐷 ) → 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) |
48 |
47
|
imp |
⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) → 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) |
49 |
2 3
|
divalglem7 |
⊢ ( ( 𝑋 ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ≠ 0 → ¬ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) |
50 |
48 49
|
sylan |
⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ≠ 0 → ¬ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) |
51 |
50
|
3adant2 |
⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ≠ 0 → ¬ ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) ) ) |
52 |
51
|
con2d |
⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) ∈ ( 0 ... ( ( abs ‘ 𝐷 ) − 1 ) ) → ¬ 𝐾 ≠ 0 ) ) |
53 |
43 52
|
syld |
⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) → ¬ 𝐾 ≠ 0 ) ) |
54 |
|
df-ne |
⊢ ( 𝐾 ≠ 0 ↔ ¬ 𝐾 = 0 ) |
55 |
54
|
con2bii |
⊢ ( 𝐾 = 0 ↔ ¬ 𝐾 ≠ 0 ) |
56 |
53 55
|
syl6ibr |
⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( 𝑌 = ( 𝑋 + ( 𝐾 · ( abs ‘ 𝐷 ) ) ) → 𝐾 = 0 ) ) |
57 |
23 56
|
sylbid |
⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) → 𝐾 = 0 ) ) |
58 |
|
oveq1 |
⊢ ( 𝐾 = 0 → ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 0 · ( abs ‘ 𝐷 ) ) ) |
59 |
11
|
nncni |
⊢ ( abs ‘ 𝐷 ) ∈ ℂ |
60 |
59
|
mul02i |
⊢ ( 0 · ( abs ‘ 𝐷 ) ) = 0 |
61 |
58 60
|
eqtrdi |
⊢ ( 𝐾 = 0 → ( 𝐾 · ( abs ‘ 𝐷 ) ) = 0 ) |
62 |
61
|
eqeq1d |
⊢ ( 𝐾 = 0 → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) ↔ 0 = ( 𝑌 − 𝑋 ) ) ) |
63 |
62
|
biimpac |
⊢ ( ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) ∧ 𝐾 = 0 ) → 0 = ( 𝑌 − 𝑋 ) ) |
64 |
|
subeq0 |
⊢ ( ( 𝑌 ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( ( 𝑌 − 𝑋 ) = 0 ↔ 𝑌 = 𝑋 ) ) |
65 |
8 9 64
|
syl2anr |
⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ( 𝑌 − 𝑋 ) = 0 ↔ 𝑌 = 𝑋 ) ) |
66 |
|
eqcom |
⊢ ( ( 𝑌 − 𝑋 ) = 0 ↔ 0 = ( 𝑌 − 𝑋 ) ) |
67 |
|
eqcom |
⊢ ( 𝑌 = 𝑋 ↔ 𝑋 = 𝑌 ) |
68 |
65 66 67
|
3bitr3g |
⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 0 = ( 𝑌 − 𝑋 ) ↔ 𝑋 = 𝑌 ) ) |
69 |
63 68
|
syl5ib |
⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) ∧ 𝐾 = 0 ) → 𝑋 = 𝑌 ) ) |
70 |
69
|
ad2ant2r |
⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ) → ( ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) ∧ 𝐾 = 0 ) → 𝑋 = 𝑌 ) ) |
71 |
70
|
3adant3 |
⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) ∧ 𝐾 = 0 ) → 𝑋 = 𝑌 ) ) |
72 |
71
|
expd |
⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) → ( 𝐾 = 0 → 𝑋 = 𝑌 ) ) ) |
73 |
57 72
|
mpdd |
⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) → 𝑋 = 𝑌 ) ) |
74 |
73
|
3expia |
⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑋 < ( abs ‘ 𝐷 ) ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ) → ( 𝐾 ∈ ℤ → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) → 𝑋 = 𝑌 ) ) ) |
75 |
74
|
an4s |
⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑋 < ( abs ‘ 𝐷 ) ∧ 𝑌 < ( abs ‘ 𝐷 ) ) ) → ( 𝐾 ∈ ℤ → ( ( 𝐾 · ( abs ‘ 𝐷 ) ) = ( 𝑌 − 𝑋 ) → 𝑋 = 𝑌 ) ) ) |