Step | Hyp | Ref
| Expression |
1 | | irrapxlem2 36405 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
→ ∃𝑎 ∈
(0...𝐵)∃𝑏 ∈ (0...𝐵)(𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵))) |
2 | | 1m1e0 10966 |
. . . . . . . . 9
⊢ (1
− 1) = 0 |
3 | | elfzelz 12213 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (0...𝐵) → 𝑎 ∈ ℤ) |
4 | 3 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → 𝑎 ∈ ℤ) |
5 | 4 | zred 11358 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → 𝑎 ∈ ℝ) |
6 | | elfzelz 12213 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ (0...𝐵) → 𝑏 ∈ ℤ) |
7 | 6 | ad2antll 761 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → 𝑏 ∈ ℤ) |
8 | 7 | zred 11358 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → 𝑏 ∈ ℝ) |
9 | 5, 8 | posdifd 10493 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → (𝑎 < 𝑏 ↔ 0 < (𝑏 − 𝑎))) |
10 | 9 | biimpa 500 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 0 < (𝑏 − 𝑎)) |
11 | 2, 10 | syl5eqbr 4618 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (1 − 1) < (𝑏 − 𝑎)) |
12 | | 1z 11284 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
13 | | simplrr 797 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑏 ∈ (0...𝐵)) |
14 | 13, 6 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑏 ∈ ℤ) |
15 | | simplrl 796 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 ∈ (0...𝐵)) |
16 | 15, 3 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 ∈ ℤ) |
17 | 14, 16 | zsubcld 11363 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 𝑎) ∈ ℤ) |
18 | | zlem1lt 11306 |
. . . . . . . . 9
⊢ ((1
∈ ℤ ∧ (𝑏
− 𝑎) ∈ ℤ)
→ (1 ≤ (𝑏 −
𝑎) ↔ (1 − 1)
< (𝑏 − 𝑎))) |
19 | 12, 17, 18 | sylancr 694 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (1 ≤ (𝑏 − 𝑎) ↔ (1 − 1) < (𝑏 − 𝑎))) |
20 | 11, 19 | mpbird 246 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 1 ≤ (𝑏 − 𝑎)) |
21 | 14 | zred 11358 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑏 ∈ ℝ) |
22 | 16 | zred 11358 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 ∈ ℝ) |
23 | 21, 22 | resubcld 10337 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 𝑎) ∈ ℝ) |
24 | | 0red 9920 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 0 ∈ ℝ) |
25 | 21, 24 | resubcld 10337 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 0) ∈ ℝ) |
26 | | simpllr 795 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝐵 ∈ ℕ) |
27 | 26 | nnred 10912 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝐵 ∈ ℝ) |
28 | | elfzle1 12215 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (0...𝐵) → 0 ≤ 𝑎) |
29 | 15, 28 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 0 ≤ 𝑎) |
30 | 24, 22, 21, 29 | lesub2dd 10523 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 𝑎) ≤ (𝑏 − 0)) |
31 | 21 | recnd 9947 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑏 ∈ ℂ) |
32 | 31 | subid1d 10260 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 0) = 𝑏) |
33 | | elfzle2 12216 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (0...𝐵) → 𝑏 ≤ 𝐵) |
34 | 13, 33 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑏 ≤ 𝐵) |
35 | 32, 34 | eqbrtrd 4605 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 0) ≤ 𝐵) |
36 | 23, 25, 27, 30, 35 | letrd 10073 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 𝑎) ≤ 𝐵) |
37 | 12 | a1i 11 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 1 ∈ ℤ) |
38 | 26 | nnzd 11357 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝐵 ∈ ℤ) |
39 | | elfz 12203 |
. . . . . . . 8
⊢ (((𝑏 − 𝑎) ∈ ℤ ∧ 1 ∈ ℤ ∧
𝐵 ∈ ℤ) →
((𝑏 − 𝑎) ∈ (1...𝐵) ↔ (1 ≤ (𝑏 − 𝑎) ∧ (𝑏 − 𝑎) ≤ 𝐵))) |
40 | 17, 37, 38, 39 | syl3anc 1318 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝑏 − 𝑎) ∈ (1...𝐵) ↔ (1 ≤ (𝑏 − 𝑎) ∧ (𝑏 − 𝑎) ≤ 𝐵))) |
41 | 20, 36, 40 | mpbir2and 959 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 𝑎) ∈ (1...𝐵)) |
42 | 41 | adantrr 749 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ (𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵))) → (𝑏 − 𝑎) ∈ (1...𝐵)) |
43 | | rpre 11715 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
44 | 43 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝐴 ∈ ℝ) |
45 | 44, 22 | remulcld 9949 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · 𝑎) ∈ ℝ) |
46 | 44, 21 | remulcld 9949 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · 𝑏) ∈ ℝ) |
47 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 < 𝑏) |
48 | 22, 21, 47 | ltled 10064 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 ≤ 𝑏) |
49 | | rpgt0 11720 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ 0 < 𝐴) |
50 | 49 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 0 < 𝐴) |
51 | | lemul2 10755 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 <
𝐴)) → (𝑎 ≤ 𝑏 ↔ (𝐴 · 𝑎) ≤ (𝐴 · 𝑏))) |
52 | 22, 21, 44, 50, 51 | syl112anc 1322 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑎 ≤ 𝑏 ↔ (𝐴 · 𝑎) ≤ (𝐴 · 𝑏))) |
53 | 48, 52 | mpbid 221 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · 𝑎) ≤ (𝐴 · 𝑏)) |
54 | | flword2 12476 |
. . . . . . . 8
⊢ (((𝐴 · 𝑎) ∈ ℝ ∧ (𝐴 · 𝑏) ∈ ℝ ∧ (𝐴 · 𝑎) ≤ (𝐴 · 𝑏)) → (⌊‘(𝐴 · 𝑏)) ∈
(ℤ≥‘(⌊‘(𝐴 · 𝑎)))) |
55 | 45, 46, 53, 54 | syl3anc 1318 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (⌊‘(𝐴 · 𝑏)) ∈
(ℤ≥‘(⌊‘(𝐴 · 𝑎)))) |
56 | | uznn0sub 11595 |
. . . . . . 7
⊢
((⌊‘(𝐴
· 𝑏)) ∈
(ℤ≥‘(⌊‘(𝐴 · 𝑎))) → ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) ∈
ℕ0) |
57 | 55, 56 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) ∈
ℕ0) |
58 | 57 | adantrr 749 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ (𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵))) → ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) ∈
ℕ0) |
59 | 44 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝐴 ∈ ℂ) |
60 | 22 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 ∈ ℂ) |
61 | 59, 31, 60 | subdid 10365 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · (𝑏 − 𝑎)) = ((𝐴 · 𝑏) − (𝐴 · 𝑎))) |
62 | 61 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎)))) = (((𝐴 · 𝑏) − (𝐴 · 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) |
63 | 46 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · 𝑏) ∈ ℂ) |
64 | 45 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · 𝑎) ∈ ℂ) |
65 | 46 | flcld 12461 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (⌊‘(𝐴 · 𝑏)) ∈ ℤ) |
66 | 65 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (⌊‘(𝐴 · 𝑏)) ∈ ℂ) |
67 | 45 | flcld 12461 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (⌊‘(𝐴 · 𝑎)) ∈ ℤ) |
68 | 67 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (⌊‘(𝐴 · 𝑎)) ∈ ℂ) |
69 | 63, 64, 66, 68 | sub4d 10320 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (((𝐴 · 𝑏) − (𝐴 · 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎)))) = (((𝐴 · 𝑏) − (⌊‘(𝐴 · 𝑏))) − ((𝐴 · 𝑎) − (⌊‘(𝐴 · 𝑎))))) |
70 | | modfrac 12545 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 · 𝑏) ∈ ℝ → ((𝐴 · 𝑏) mod 1) = ((𝐴 · 𝑏) − (⌊‘(𝐴 · 𝑏)))) |
71 | 46, 70 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑏) mod 1) = ((𝐴 · 𝑏) − (⌊‘(𝐴 · 𝑏)))) |
72 | 71 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑏) − (⌊‘(𝐴 · 𝑏))) = ((𝐴 · 𝑏) mod 1)) |
73 | | modfrac 12545 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 · 𝑎) ∈ ℝ → ((𝐴 · 𝑎) mod 1) = ((𝐴 · 𝑎) − (⌊‘(𝐴 · 𝑎)))) |
74 | 45, 73 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑎) mod 1) = ((𝐴 · 𝑎) − (⌊‘(𝐴 · 𝑎)))) |
75 | 74 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑎) − (⌊‘(𝐴 · 𝑎))) = ((𝐴 · 𝑎) mod 1)) |
76 | 72, 75 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (((𝐴 · 𝑏) − (⌊‘(𝐴 · 𝑏))) − ((𝐴 · 𝑎) − (⌊‘(𝐴 · 𝑎)))) = (((𝐴 · 𝑏) mod 1) − ((𝐴 · 𝑎) mod 1))) |
77 | 62, 69, 76 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎)))) = (((𝐴 · 𝑏) mod 1) − ((𝐴 · 𝑎) mod 1))) |
78 | 77 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) = (abs‘(((𝐴 · 𝑏) mod 1) − ((𝐴 · 𝑎) mod 1)))) |
79 | | 1rp 11712 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ+ |
80 | 79 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 1 ∈
ℝ+) |
81 | 46, 80 | modcld 12536 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑏) mod 1) ∈ ℝ) |
82 | 81 | recnd 9947 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑏) mod 1) ∈ ℂ) |
83 | 45, 80 | modcld 12536 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑎) mod 1) ∈ ℝ) |
84 | 83 | recnd 9947 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑎) mod 1) ∈ ℂ) |
85 | 82, 84 | abssubd 14040 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (abs‘(((𝐴 · 𝑏) mod 1) − ((𝐴 · 𝑎) mod 1))) = (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1)))) |
86 | 78, 85 | eqtr2d 2645 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) = (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎)))))) |
87 | 86 | breq1d 4593 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵) ↔ (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) < (1 / 𝐵))) |
88 | 87 | biimpd 218 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵) → (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) < (1 / 𝐵))) |
89 | 88 | impr 647 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ (𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵))) → (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) < (1 / 𝐵)) |
90 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑥 = (𝑏 − 𝑎) → (𝐴 · 𝑥) = (𝐴 · (𝑏 − 𝑎))) |
91 | 90 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑥 = (𝑏 − 𝑎) → ((𝐴 · 𝑥) − 𝑦) = ((𝐴 · (𝑏 − 𝑎)) − 𝑦)) |
92 | 91 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = (𝑏 − 𝑎) → (abs‘((𝐴 · 𝑥) − 𝑦)) = (abs‘((𝐴 · (𝑏 − 𝑎)) − 𝑦))) |
93 | 92 | breq1d 4593 |
. . . . . 6
⊢ (𝑥 = (𝑏 − 𝑎) → ((abs‘((𝐴 · 𝑥) − 𝑦)) < (1 / 𝐵) ↔ (abs‘((𝐴 · (𝑏 − 𝑎)) − 𝑦)) < (1 / 𝐵))) |
94 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑦 = ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) → ((𝐴 · (𝑏 − 𝑎)) − 𝑦) = ((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) |
95 | 94 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑦 = ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) → (abs‘((𝐴 · (𝑏 − 𝑎)) − 𝑦)) = (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎)))))) |
96 | 95 | breq1d 4593 |
. . . . . 6
⊢ (𝑦 = ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) → ((abs‘((𝐴 · (𝑏 − 𝑎)) − 𝑦)) < (1 / 𝐵) ↔ (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) < (1 / 𝐵))) |
97 | 93, 96 | rspc2ev 3295 |
. . . . 5
⊢ (((𝑏 − 𝑎) ∈ (1...𝐵) ∧ ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) ∈ ℕ0 ∧
(abs‘((𝐴 ·
(𝑏 − 𝑎)) −
((⌊‘(𝐴 ·
𝑏)) −
(⌊‘(𝐴 ·
𝑎))))) < (1 / 𝐵)) → ∃𝑥 ∈ (1...𝐵)∃𝑦 ∈ ℕ0
(abs‘((𝐴 ·
𝑥) − 𝑦)) < (1 / 𝐵)) |
98 | 42, 58, 89, 97 | syl3anc 1318 |
. . . 4
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ (𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵))) → ∃𝑥 ∈ (1...𝐵)∃𝑦 ∈ ℕ0
(abs‘((𝐴 ·
𝑥) − 𝑦)) < (1 / 𝐵)) |
99 | 98 | ex 449 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → ((𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵)) → ∃𝑥 ∈ (1...𝐵)∃𝑦 ∈ ℕ0
(abs‘((𝐴 ·
𝑥) − 𝑦)) < (1 / 𝐵))) |
100 | 99 | rexlimdvva 3020 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
→ (∃𝑎 ∈
(0...𝐵)∃𝑏 ∈ (0...𝐵)(𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵)) → ∃𝑥 ∈ (1...𝐵)∃𝑦 ∈ ℕ0
(abs‘((𝐴 ·
𝑥) − 𝑦)) < (1 / 𝐵))) |
101 | 1, 100 | mpd 15 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
→ ∃𝑥 ∈
(1...𝐵)∃𝑦 ∈ ℕ0
(abs‘((𝐴 ·
𝑥) − 𝑦)) < (1 / 𝐵)) |