Step | Hyp | Ref
| Expression |
1 | | irrapxlem2 38926 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
→ ∃𝑎 ∈
(0...𝐵)∃𝑏 ∈ (0...𝐵)(𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵))) |
2 | | 1m1e0 11563 |
. . . . . . . . 9
⊢ (1
− 1) = 0 |
3 | | elfzelz 12762 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (0...𝐵) → 𝑎 ∈ ℤ) |
4 | 3 | ad2antrl 724 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → 𝑎 ∈ ℤ) |
5 | 4 | zred 11941 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → 𝑎 ∈ ℝ) |
6 | | elfzelz 12762 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ (0...𝐵) → 𝑏 ∈ ℤ) |
7 | 6 | ad2antll 725 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → 𝑏 ∈ ℤ) |
8 | 7 | zred 11941 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → 𝑏 ∈ ℝ) |
9 | 5, 8 | posdifd 11081 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → (𝑎 < 𝑏 ↔ 0 < (𝑏 − 𝑎))) |
10 | 9 | biimpa 477 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 0 < (𝑏 − 𝑎)) |
11 | 2, 10 | eqbrtrid 5003 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (1 − 1) < (𝑏 − 𝑎)) |
12 | | 1z 11866 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
13 | | simplrr 774 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑏 ∈ (0...𝐵)) |
14 | 13, 6 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑏 ∈ ℤ) |
15 | | simplrl 773 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 ∈ (0...𝐵)) |
16 | 15, 3 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 ∈ ℤ) |
17 | 14, 16 | zsubcld 11946 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 𝑎) ∈ ℤ) |
18 | | zlem1lt 11888 |
. . . . . . . . 9
⊢ ((1
∈ ℤ ∧ (𝑏
− 𝑎) ∈ ℤ)
→ (1 ≤ (𝑏 −
𝑎) ↔ (1 − 1)
< (𝑏 − 𝑎))) |
19 | 12, 17, 18 | sylancr 587 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (1 ≤ (𝑏 − 𝑎) ↔ (1 − 1) < (𝑏 − 𝑎))) |
20 | 11, 19 | mpbird 258 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 1 ≤ (𝑏 − 𝑎)) |
21 | 14 | zred 11941 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑏 ∈ ℝ) |
22 | 16 | zred 11941 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 ∈ ℝ) |
23 | 21, 22 | resubcld 10922 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 𝑎) ∈ ℝ) |
24 | | 0red 10497 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 0 ∈ ℝ) |
25 | 21, 24 | resubcld 10922 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 0) ∈ ℝ) |
26 | | simpllr 772 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝐵 ∈ ℕ) |
27 | 26 | nnred 11507 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝐵 ∈ ℝ) |
28 | | elfzle1 12764 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (0...𝐵) → 0 ≤ 𝑎) |
29 | 15, 28 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 0 ≤ 𝑎) |
30 | 24, 22, 21, 29 | lesub2dd 11111 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 𝑎) ≤ (𝑏 − 0)) |
31 | 21 | recnd 10522 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑏 ∈ ℂ) |
32 | 31 | subid1d 10840 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 0) = 𝑏) |
33 | | elfzle2 12765 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (0...𝐵) → 𝑏 ≤ 𝐵) |
34 | 13, 33 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑏 ≤ 𝐵) |
35 | 32, 34 | eqbrtrd 4990 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 0) ≤ 𝐵) |
36 | 23, 25, 27, 30, 35 | letrd 10650 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 𝑎) ≤ 𝐵) |
37 | 12 | a1i 11 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 1 ∈ ℤ) |
38 | 26 | nnzd 11940 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝐵 ∈ ℤ) |
39 | | elfz 12752 |
. . . . . . . 8
⊢ (((𝑏 − 𝑎) ∈ ℤ ∧ 1 ∈ ℤ ∧
𝐵 ∈ ℤ) →
((𝑏 − 𝑎) ∈ (1...𝐵) ↔ (1 ≤ (𝑏 − 𝑎) ∧ (𝑏 − 𝑎) ≤ 𝐵))) |
40 | 17, 37, 38, 39 | syl3anc 1364 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝑏 − 𝑎) ∈ (1...𝐵) ↔ (1 ≤ (𝑏 − 𝑎) ∧ (𝑏 − 𝑎) ≤ 𝐵))) |
41 | 20, 36, 40 | mpbir2and 709 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 𝑎) ∈ (1...𝐵)) |
42 | 41 | adantrr 713 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ (𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵))) → (𝑏 − 𝑎) ∈ (1...𝐵)) |
43 | | rpre 12251 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
44 | 43 | ad3antrrr 726 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝐴 ∈ ℝ) |
45 | 44, 22 | remulcld 10524 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · 𝑎) ∈ ℝ) |
46 | 44, 21 | remulcld 10524 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · 𝑏) ∈ ℝ) |
47 | | simpr 485 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 < 𝑏) |
48 | 22, 21, 47 | ltled 10641 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 ≤ 𝑏) |
49 | | rpgt0 12255 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ 0 < 𝐴) |
50 | 49 | ad3antrrr 726 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 0 < 𝐴) |
51 | | lemul2 11347 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 <
𝐴)) → (𝑎 ≤ 𝑏 ↔ (𝐴 · 𝑎) ≤ (𝐴 · 𝑏))) |
52 | 22, 21, 44, 50, 51 | syl112anc 1367 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑎 ≤ 𝑏 ↔ (𝐴 · 𝑎) ≤ (𝐴 · 𝑏))) |
53 | 48, 52 | mpbid 233 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · 𝑎) ≤ (𝐴 · 𝑏)) |
54 | | flword2 13037 |
. . . . . . . 8
⊢ (((𝐴 · 𝑎) ∈ ℝ ∧ (𝐴 · 𝑏) ∈ ℝ ∧ (𝐴 · 𝑎) ≤ (𝐴 · 𝑏)) → (⌊‘(𝐴 · 𝑏)) ∈
(ℤ≥‘(⌊‘(𝐴 · 𝑎)))) |
55 | 45, 46, 53, 54 | syl3anc 1364 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (⌊‘(𝐴 · 𝑏)) ∈
(ℤ≥‘(⌊‘(𝐴 · 𝑎)))) |
56 | | uznn0sub 12130 |
. . . . . . 7
⊢
((⌊‘(𝐴
· 𝑏)) ∈
(ℤ≥‘(⌊‘(𝐴 · 𝑎))) → ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) ∈
ℕ0) |
57 | 55, 56 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) ∈
ℕ0) |
58 | 57 | adantrr 713 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ (𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵))) → ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) ∈
ℕ0) |
59 | 44 | recnd 10522 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝐴 ∈ ℂ) |
60 | 22 | recnd 10522 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 ∈ ℂ) |
61 | 59, 31, 60 | subdid 10950 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · (𝑏 − 𝑎)) = ((𝐴 · 𝑏) − (𝐴 · 𝑎))) |
62 | 61 | oveq1d 7038 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎)))) = (((𝐴 · 𝑏) − (𝐴 · 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) |
63 | 46 | recnd 10522 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · 𝑏) ∈ ℂ) |
64 | 45 | recnd 10522 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · 𝑎) ∈ ℂ) |
65 | 46 | flcld 13022 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (⌊‘(𝐴 · 𝑏)) ∈ ℤ) |
66 | 65 | zcnd 11942 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (⌊‘(𝐴 · 𝑏)) ∈ ℂ) |
67 | 45 | flcld 13022 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (⌊‘(𝐴 · 𝑎)) ∈ ℤ) |
68 | 67 | zcnd 11942 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (⌊‘(𝐴 · 𝑎)) ∈ ℂ) |
69 | 63, 64, 66, 68 | sub4d 10900 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (((𝐴 · 𝑏) − (𝐴 · 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎)))) = (((𝐴 · 𝑏) − (⌊‘(𝐴 · 𝑏))) − ((𝐴 · 𝑎) − (⌊‘(𝐴 · 𝑎))))) |
70 | | modfrac 13106 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 · 𝑏) ∈ ℝ → ((𝐴 · 𝑏) mod 1) = ((𝐴 · 𝑏) − (⌊‘(𝐴 · 𝑏)))) |
71 | 46, 70 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑏) mod 1) = ((𝐴 · 𝑏) − (⌊‘(𝐴 · 𝑏)))) |
72 | 71 | eqcomd 2803 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑏) − (⌊‘(𝐴 · 𝑏))) = ((𝐴 · 𝑏) mod 1)) |
73 | | modfrac 13106 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 · 𝑎) ∈ ℝ → ((𝐴 · 𝑎) mod 1) = ((𝐴 · 𝑎) − (⌊‘(𝐴 · 𝑎)))) |
74 | 45, 73 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑎) mod 1) = ((𝐴 · 𝑎) − (⌊‘(𝐴 · 𝑎)))) |
75 | 74 | eqcomd 2803 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑎) − (⌊‘(𝐴 · 𝑎))) = ((𝐴 · 𝑎) mod 1)) |
76 | 72, 75 | oveq12d 7041 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (((𝐴 · 𝑏) − (⌊‘(𝐴 · 𝑏))) − ((𝐴 · 𝑎) − (⌊‘(𝐴 · 𝑎)))) = (((𝐴 · 𝑏) mod 1) − ((𝐴 · 𝑎) mod 1))) |
77 | 62, 69, 76 | 3eqtrd 2837 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎)))) = (((𝐴 · 𝑏) mod 1) − ((𝐴 · 𝑎) mod 1))) |
78 | 77 | fveq2d 6549 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) = (abs‘(((𝐴 · 𝑏) mod 1) − ((𝐴 · 𝑎) mod 1)))) |
79 | | 1rp 12247 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ+ |
80 | 79 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 1 ∈
ℝ+) |
81 | 46, 80 | modcld 13097 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑏) mod 1) ∈ ℝ) |
82 | 81 | recnd 10522 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑏) mod 1) ∈ ℂ) |
83 | 45, 80 | modcld 13097 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑎) mod 1) ∈ ℝ) |
84 | 83 | recnd 10522 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑎) mod 1) ∈ ℂ) |
85 | 82, 84 | abssubd 14651 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (abs‘(((𝐴 · 𝑏) mod 1) − ((𝐴 · 𝑎) mod 1))) = (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1)))) |
86 | 78, 85 | eqtr2d 2834 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) = (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎)))))) |
87 | 86 | breq1d 4978 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵) ↔ (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) < (1 / 𝐵))) |
88 | 87 | biimpd 230 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵) → (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) < (1 / 𝐵))) |
89 | 88 | impr 455 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ (𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵))) → (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) < (1 / 𝐵)) |
90 | | oveq2 7031 |
. . . . . . . 8
⊢ (𝑥 = (𝑏 − 𝑎) → (𝐴 · 𝑥) = (𝐴 · (𝑏 − 𝑎))) |
91 | 90 | fvoveq1d 7045 |
. . . . . . 7
⊢ (𝑥 = (𝑏 − 𝑎) → (abs‘((𝐴 · 𝑥) − 𝑦)) = (abs‘((𝐴 · (𝑏 − 𝑎)) − 𝑦))) |
92 | 91 | breq1d 4978 |
. . . . . 6
⊢ (𝑥 = (𝑏 − 𝑎) → ((abs‘((𝐴 · 𝑥) − 𝑦)) < (1 / 𝐵) ↔ (abs‘((𝐴 · (𝑏 − 𝑎)) − 𝑦)) < (1 / 𝐵))) |
93 | | oveq2 7031 |
. . . . . . . 8
⊢ (𝑦 = ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) → ((𝐴 · (𝑏 − 𝑎)) − 𝑦) = ((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) |
94 | 93 | fveq2d 6549 |
. . . . . . 7
⊢ (𝑦 = ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) → (abs‘((𝐴 · (𝑏 − 𝑎)) − 𝑦)) = (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎)))))) |
95 | 94 | breq1d 4978 |
. . . . . 6
⊢ (𝑦 = ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) → ((abs‘((𝐴 · (𝑏 − 𝑎)) − 𝑦)) < (1 / 𝐵) ↔ (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) < (1 / 𝐵))) |
96 | 92, 95 | rspc2ev 3576 |
. . . . 5
⊢ (((𝑏 − 𝑎) ∈ (1...𝐵) ∧ ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) ∈ ℕ0 ∧
(abs‘((𝐴 ·
(𝑏 − 𝑎)) −
((⌊‘(𝐴 ·
𝑏)) −
(⌊‘(𝐴 ·
𝑎))))) < (1 / 𝐵)) → ∃𝑥 ∈ (1...𝐵)∃𝑦 ∈ ℕ0
(abs‘((𝐴 ·
𝑥) − 𝑦)) < (1 / 𝐵)) |
97 | 42, 58, 89, 96 | syl3anc 1364 |
. . . 4
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ (𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵))) → ∃𝑥 ∈ (1...𝐵)∃𝑦 ∈ ℕ0
(abs‘((𝐴 ·
𝑥) − 𝑦)) < (1 / 𝐵)) |
98 | 97 | ex 413 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → ((𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵)) → ∃𝑥 ∈ (1...𝐵)∃𝑦 ∈ ℕ0
(abs‘((𝐴 ·
𝑥) − 𝑦)) < (1 / 𝐵))) |
99 | 98 | rexlimdvva 3259 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
→ (∃𝑎 ∈
(0...𝐵)∃𝑏 ∈ (0...𝐵)(𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵)) → ∃𝑥 ∈ (1...𝐵)∃𝑦 ∈ ℕ0
(abs‘((𝐴 ·
𝑥) − 𝑦)) < (1 / 𝐵))) |
100 | 1, 99 | mpd 15 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
→ ∃𝑥 ∈
(1...𝐵)∃𝑦 ∈ ℕ0
(abs‘((𝐴 ·
𝑥) − 𝑦)) < (1 / 𝐵)) |