Step |
Hyp |
Ref |
Expression |
1 |
|
divalglem0.1 |
⊢ 𝑁 ∈ ℤ |
2 |
|
divalglem0.2 |
⊢ 𝐷 ∈ ℤ |
3 |
|
divalglem1.3 |
⊢ 𝐷 ≠ 0 |
4 |
|
divalglem2.4 |
⊢ 𝑆 = { 𝑟 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑟 ) } |
5 |
|
divalglem5.5 |
⊢ 𝑅 = inf ( 𝑆 , ℝ , < ) |
6 |
1 2 3 4
|
divalglem2 |
⊢ inf ( 𝑆 , ℝ , < ) ∈ 𝑆 |
7 |
5 6
|
eqeltri |
⊢ 𝑅 ∈ 𝑆 |
8 |
|
oveq2 |
⊢ ( 𝑥 = 𝑅 → ( 𝑁 − 𝑥 ) = ( 𝑁 − 𝑅 ) ) |
9 |
8
|
breq2d |
⊢ ( 𝑥 = 𝑅 → ( 𝐷 ∥ ( 𝑁 − 𝑥 ) ↔ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) |
10 |
|
oveq2 |
⊢ ( 𝑟 = 𝑥 → ( 𝑁 − 𝑟 ) = ( 𝑁 − 𝑥 ) ) |
11 |
10
|
breq2d |
⊢ ( 𝑟 = 𝑥 → ( 𝐷 ∥ ( 𝑁 − 𝑟 ) ↔ 𝐷 ∥ ( 𝑁 − 𝑥 ) ) ) |
12 |
11
|
cbvrabv |
⊢ { 𝑟 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑟 ) } = { 𝑥 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑥 ) } |
13 |
4 12
|
eqtri |
⊢ 𝑆 = { 𝑥 ∈ ℕ0 ∣ 𝐷 ∥ ( 𝑁 − 𝑥 ) } |
14 |
9 13
|
elrab2 |
⊢ ( 𝑅 ∈ 𝑆 ↔ ( 𝑅 ∈ ℕ0 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) |
15 |
7 14
|
mpbi |
⊢ ( 𝑅 ∈ ℕ0 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) |
16 |
15
|
simpli |
⊢ 𝑅 ∈ ℕ0 |
17 |
16
|
nn0ge0i |
⊢ 0 ≤ 𝑅 |
18 |
|
nnabscl |
⊢ ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) → ( abs ‘ 𝐷 ) ∈ ℕ ) |
19 |
2 3 18
|
mp2an |
⊢ ( abs ‘ 𝐷 ) ∈ ℕ |
20 |
19
|
nngt0i |
⊢ 0 < ( abs ‘ 𝐷 ) |
21 |
|
0re |
⊢ 0 ∈ ℝ |
22 |
|
zcn |
⊢ ( 𝐷 ∈ ℤ → 𝐷 ∈ ℂ ) |
23 |
2 22
|
ax-mp |
⊢ 𝐷 ∈ ℂ |
24 |
23
|
abscli |
⊢ ( abs ‘ 𝐷 ) ∈ ℝ |
25 |
21 24
|
ltnlei |
⊢ ( 0 < ( abs ‘ 𝐷 ) ↔ ¬ ( abs ‘ 𝐷 ) ≤ 0 ) |
26 |
20 25
|
mpbi |
⊢ ¬ ( abs ‘ 𝐷 ) ≤ 0 |
27 |
4
|
ssrab3 |
⊢ 𝑆 ⊆ ℕ0 |
28 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
29 |
27 28
|
sseqtri |
⊢ 𝑆 ⊆ ( ℤ≥ ‘ 0 ) |
30 |
|
nn0abscl |
⊢ ( 𝐷 ∈ ℤ → ( abs ‘ 𝐷 ) ∈ ℕ0 ) |
31 |
2 30
|
ax-mp |
⊢ ( abs ‘ 𝐷 ) ∈ ℕ0 |
32 |
|
nn0sub2 |
⊢ ( ( ( abs ‘ 𝐷 ) ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ ( abs ‘ 𝐷 ) ≤ 𝑅 ) → ( 𝑅 − ( abs ‘ 𝐷 ) ) ∈ ℕ0 ) |
33 |
31 16 32
|
mp3an12 |
⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → ( 𝑅 − ( abs ‘ 𝐷 ) ) ∈ ℕ0 ) |
34 |
15
|
a1i |
⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → ( 𝑅 ∈ ℕ0 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) ) |
35 |
|
nn0z |
⊢ ( 𝑅 ∈ ℕ0 → 𝑅 ∈ ℤ ) |
36 |
|
1z |
⊢ 1 ∈ ℤ |
37 |
1 2
|
divalglem0 |
⊢ ( ( 𝑅 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝐷 ∥ ( 𝑁 − 𝑅 ) → 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( 1 · ( abs ‘ 𝐷 ) ) ) ) ) ) |
38 |
36 37
|
mpan2 |
⊢ ( 𝑅 ∈ ℤ → ( 𝐷 ∥ ( 𝑁 − 𝑅 ) → 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( 1 · ( abs ‘ 𝐷 ) ) ) ) ) ) |
39 |
24
|
recni |
⊢ ( abs ‘ 𝐷 ) ∈ ℂ |
40 |
39
|
mulid2i |
⊢ ( 1 · ( abs ‘ 𝐷 ) ) = ( abs ‘ 𝐷 ) |
41 |
40
|
oveq2i |
⊢ ( 𝑅 − ( 1 · ( abs ‘ 𝐷 ) ) ) = ( 𝑅 − ( abs ‘ 𝐷 ) ) |
42 |
41
|
oveq2i |
⊢ ( 𝑁 − ( 𝑅 − ( 1 · ( abs ‘ 𝐷 ) ) ) ) = ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) |
43 |
42
|
breq2i |
⊢ ( 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( 1 · ( abs ‘ 𝐷 ) ) ) ) ↔ 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) ) |
44 |
38 43
|
syl6ib |
⊢ ( 𝑅 ∈ ℤ → ( 𝐷 ∥ ( 𝑁 − 𝑅 ) → 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) ) ) |
45 |
35 44
|
syl |
⊢ ( 𝑅 ∈ ℕ0 → ( 𝐷 ∥ ( 𝑁 − 𝑅 ) → 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) ) ) |
46 |
45
|
imp |
⊢ ( ( 𝑅 ∈ ℕ0 ∧ 𝐷 ∥ ( 𝑁 − 𝑅 ) ) → 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) ) |
47 |
34 46
|
syl |
⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) ) |
48 |
|
oveq2 |
⊢ ( 𝑥 = ( 𝑅 − ( abs ‘ 𝐷 ) ) → ( 𝑁 − 𝑥 ) = ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) ) |
49 |
48
|
breq2d |
⊢ ( 𝑥 = ( 𝑅 − ( abs ‘ 𝐷 ) ) → ( 𝐷 ∥ ( 𝑁 − 𝑥 ) ↔ 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) ) ) |
50 |
49 13
|
elrab2 |
⊢ ( ( 𝑅 − ( abs ‘ 𝐷 ) ) ∈ 𝑆 ↔ ( ( 𝑅 − ( abs ‘ 𝐷 ) ) ∈ ℕ0 ∧ 𝐷 ∥ ( 𝑁 − ( 𝑅 − ( abs ‘ 𝐷 ) ) ) ) ) |
51 |
33 47 50
|
sylanbrc |
⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → ( 𝑅 − ( abs ‘ 𝐷 ) ) ∈ 𝑆 ) |
52 |
|
infssuzle |
⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 0 ) ∧ ( 𝑅 − ( abs ‘ 𝐷 ) ) ∈ 𝑆 ) → inf ( 𝑆 , ℝ , < ) ≤ ( 𝑅 − ( abs ‘ 𝐷 ) ) ) |
53 |
29 51 52
|
sylancr |
⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → inf ( 𝑆 , ℝ , < ) ≤ ( 𝑅 − ( abs ‘ 𝐷 ) ) ) |
54 |
5 53
|
eqbrtrid |
⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → 𝑅 ≤ ( 𝑅 − ( abs ‘ 𝐷 ) ) ) |
55 |
34
|
simpld |
⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → 𝑅 ∈ ℕ0 ) |
56 |
55
|
nn0red |
⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → 𝑅 ∈ ℝ ) |
57 |
|
lesub |
⊢ ( ( 𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ( abs ‘ 𝐷 ) ∈ ℝ ) → ( 𝑅 ≤ ( 𝑅 − ( abs ‘ 𝐷 ) ) ↔ ( abs ‘ 𝐷 ) ≤ ( 𝑅 − 𝑅 ) ) ) |
58 |
24 57
|
mp3an3 |
⊢ ( ( 𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 𝑅 ≤ ( 𝑅 − ( abs ‘ 𝐷 ) ) ↔ ( abs ‘ 𝐷 ) ≤ ( 𝑅 − 𝑅 ) ) ) |
59 |
56 56 58
|
syl2anc |
⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → ( 𝑅 ≤ ( 𝑅 − ( abs ‘ 𝐷 ) ) ↔ ( abs ‘ 𝐷 ) ≤ ( 𝑅 − 𝑅 ) ) ) |
60 |
56
|
recnd |
⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → 𝑅 ∈ ℂ ) |
61 |
60
|
subidd |
⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → ( 𝑅 − 𝑅 ) = 0 ) |
62 |
61
|
breq2d |
⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → ( ( abs ‘ 𝐷 ) ≤ ( 𝑅 − 𝑅 ) ↔ ( abs ‘ 𝐷 ) ≤ 0 ) ) |
63 |
59 62
|
bitrd |
⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → ( 𝑅 ≤ ( 𝑅 − ( abs ‘ 𝐷 ) ) ↔ ( abs ‘ 𝐷 ) ≤ 0 ) ) |
64 |
54 63
|
mpbid |
⊢ ( ( abs ‘ 𝐷 ) ≤ 𝑅 → ( abs ‘ 𝐷 ) ≤ 0 ) |
65 |
26 64
|
mto |
⊢ ¬ ( abs ‘ 𝐷 ) ≤ 𝑅 |
66 |
16
|
nn0rei |
⊢ 𝑅 ∈ ℝ |
67 |
66 24
|
ltnlei |
⊢ ( 𝑅 < ( abs ‘ 𝐷 ) ↔ ¬ ( abs ‘ 𝐷 ) ≤ 𝑅 ) |
68 |
65 67
|
mpbir |
⊢ 𝑅 < ( abs ‘ 𝐷 ) |
69 |
17 68
|
pm3.2i |
⊢ ( 0 ≤ 𝑅 ∧ 𝑅 < ( abs ‘ 𝐷 ) ) |