| Step | Hyp | Ref
| Expression |
| 1 | | irrapxlem2 42834 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
→ ∃𝑎 ∈
(0...𝐵)∃𝑏 ∈ (0...𝐵)(𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵))) |
| 2 | | 1z 12647 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
| 3 | 2 | a1i 11 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 1 ∈ ℤ) |
| 4 | | simpllr 776 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝐵 ∈ ℕ) |
| 5 | 4 | nnzd 12640 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝐵 ∈ ℤ) |
| 6 | | simplrr 778 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑏 ∈ (0...𝐵)) |
| 7 | 6 | elfzelzd 13565 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑏 ∈ ℤ) |
| 8 | | simplrl 777 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 ∈ (0...𝐵)) |
| 9 | 8 | elfzelzd 13565 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 ∈ ℤ) |
| 10 | 7, 9 | zsubcld 12727 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 𝑎) ∈ ℤ) |
| 11 | | 1m1e0 12338 |
. . . . . . . . 9
⊢ (1
− 1) = 0 |
| 12 | | elfzelz 13564 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (0...𝐵) → 𝑎 ∈ ℤ) |
| 13 | 12 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → 𝑎 ∈ ℤ) |
| 14 | 13 | zred 12722 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → 𝑎 ∈ ℝ) |
| 15 | | elfzelz 13564 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ (0...𝐵) → 𝑏 ∈ ℤ) |
| 16 | 15 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → 𝑏 ∈ ℤ) |
| 17 | 16 | zred 12722 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → 𝑏 ∈ ℝ) |
| 18 | 14, 17 | posdifd 11850 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → (𝑎 < 𝑏 ↔ 0 < (𝑏 − 𝑎))) |
| 19 | 18 | biimpa 476 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 0 < (𝑏 − 𝑎)) |
| 20 | 11, 19 | eqbrtrid 5178 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (1 − 1) < (𝑏 − 𝑎)) |
| 21 | | zlem1lt 12669 |
. . . . . . . . 9
⊢ ((1
∈ ℤ ∧ (𝑏
− 𝑎) ∈ ℤ)
→ (1 ≤ (𝑏 −
𝑎) ↔ (1 − 1)
< (𝑏 − 𝑎))) |
| 22 | 2, 10, 21 | sylancr 587 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (1 ≤ (𝑏 − 𝑎) ↔ (1 − 1) < (𝑏 − 𝑎))) |
| 23 | 20, 22 | mpbird 257 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 1 ≤ (𝑏 − 𝑎)) |
| 24 | 7 | zred 12722 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑏 ∈ ℝ) |
| 25 | 9 | zred 12722 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 ∈ ℝ) |
| 26 | 24, 25 | resubcld 11691 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 𝑎) ∈ ℝ) |
| 27 | | 0red 11264 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 0 ∈ ℝ) |
| 28 | 24, 27 | resubcld 11691 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 0) ∈ ℝ) |
| 29 | 4 | nnred 12281 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝐵 ∈ ℝ) |
| 30 | | elfzle1 13567 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (0...𝐵) → 0 ≤ 𝑎) |
| 31 | 8, 30 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 0 ≤ 𝑎) |
| 32 | 27, 25, 24, 31 | lesub2dd 11880 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 𝑎) ≤ (𝑏 − 0)) |
| 33 | 24 | recnd 11289 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑏 ∈ ℂ) |
| 34 | 33 | subid1d 11609 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 0) = 𝑏) |
| 35 | | elfzle2 13568 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (0...𝐵) → 𝑏 ≤ 𝐵) |
| 36 | 6, 35 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑏 ≤ 𝐵) |
| 37 | 34, 36 | eqbrtrd 5165 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 0) ≤ 𝐵) |
| 38 | 26, 28, 29, 32, 37 | letrd 11418 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 𝑎) ≤ 𝐵) |
| 39 | 3, 5, 10, 23, 38 | elfzd 13555 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑏 − 𝑎) ∈ (1...𝐵)) |
| 40 | 39 | adantrr 717 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ (𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵))) → (𝑏 − 𝑎) ∈ (1...𝐵)) |
| 41 | | rpre 13043 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
| 42 | 41 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝐴 ∈ ℝ) |
| 43 | 42, 25 | remulcld 11291 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · 𝑎) ∈ ℝ) |
| 44 | 42, 24 | remulcld 11291 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · 𝑏) ∈ ℝ) |
| 45 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 < 𝑏) |
| 46 | 25, 24, 45 | ltled 11409 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 ≤ 𝑏) |
| 47 | | rpgt0 13047 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ 0 < 𝐴) |
| 48 | 47 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 0 < 𝐴) |
| 49 | | lemul2 12120 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 <
𝐴)) → (𝑎 ≤ 𝑏 ↔ (𝐴 · 𝑎) ≤ (𝐴 · 𝑏))) |
| 50 | 25, 24, 42, 48, 49 | syl112anc 1376 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝑎 ≤ 𝑏 ↔ (𝐴 · 𝑎) ≤ (𝐴 · 𝑏))) |
| 51 | 46, 50 | mpbid 232 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · 𝑎) ≤ (𝐴 · 𝑏)) |
| 52 | | flword2 13853 |
. . . . . . . 8
⊢ (((𝐴 · 𝑎) ∈ ℝ ∧ (𝐴 · 𝑏) ∈ ℝ ∧ (𝐴 · 𝑎) ≤ (𝐴 · 𝑏)) → (⌊‘(𝐴 · 𝑏)) ∈
(ℤ≥‘(⌊‘(𝐴 · 𝑎)))) |
| 53 | 43, 44, 51, 52 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (⌊‘(𝐴 · 𝑏)) ∈
(ℤ≥‘(⌊‘(𝐴 · 𝑎)))) |
| 54 | | uznn0sub 12917 |
. . . . . . 7
⊢
((⌊‘(𝐴
· 𝑏)) ∈
(ℤ≥‘(⌊‘(𝐴 · 𝑎))) → ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) ∈
ℕ0) |
| 55 | 53, 54 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) ∈
ℕ0) |
| 56 | 55 | adantrr 717 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ (𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵))) → ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) ∈
ℕ0) |
| 57 | 42 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝐴 ∈ ℂ) |
| 58 | 25 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 𝑎 ∈ ℂ) |
| 59 | 57, 33, 58 | subdid 11719 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · (𝑏 − 𝑎)) = ((𝐴 · 𝑏) − (𝐴 · 𝑎))) |
| 60 | 59 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎)))) = (((𝐴 · 𝑏) − (𝐴 · 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) |
| 61 | 44 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · 𝑏) ∈ ℂ) |
| 62 | 43 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (𝐴 · 𝑎) ∈ ℂ) |
| 63 | 44 | flcld 13838 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (⌊‘(𝐴 · 𝑏)) ∈ ℤ) |
| 64 | 63 | zcnd 12723 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (⌊‘(𝐴 · 𝑏)) ∈ ℂ) |
| 65 | 43 | flcld 13838 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (⌊‘(𝐴 · 𝑎)) ∈ ℤ) |
| 66 | 65 | zcnd 12723 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (⌊‘(𝐴 · 𝑎)) ∈ ℂ) |
| 67 | 61, 62, 64, 66 | sub4d 11669 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (((𝐴 · 𝑏) − (𝐴 · 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎)))) = (((𝐴 · 𝑏) − (⌊‘(𝐴 · 𝑏))) − ((𝐴 · 𝑎) − (⌊‘(𝐴 · 𝑎))))) |
| 68 | | modfrac 13924 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 · 𝑏) ∈ ℝ → ((𝐴 · 𝑏) mod 1) = ((𝐴 · 𝑏) − (⌊‘(𝐴 · 𝑏)))) |
| 69 | 44, 68 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑏) mod 1) = ((𝐴 · 𝑏) − (⌊‘(𝐴 · 𝑏)))) |
| 70 | 69 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑏) − (⌊‘(𝐴 · 𝑏))) = ((𝐴 · 𝑏) mod 1)) |
| 71 | | modfrac 13924 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 · 𝑎) ∈ ℝ → ((𝐴 · 𝑎) mod 1) = ((𝐴 · 𝑎) − (⌊‘(𝐴 · 𝑎)))) |
| 72 | 43, 71 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑎) mod 1) = ((𝐴 · 𝑎) − (⌊‘(𝐴 · 𝑎)))) |
| 73 | 72 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑎) − (⌊‘(𝐴 · 𝑎))) = ((𝐴 · 𝑎) mod 1)) |
| 74 | 70, 73 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (((𝐴 · 𝑏) − (⌊‘(𝐴 · 𝑏))) − ((𝐴 · 𝑎) − (⌊‘(𝐴 · 𝑎)))) = (((𝐴 · 𝑏) mod 1) − ((𝐴 · 𝑎) mod 1))) |
| 75 | 60, 67, 74 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎)))) = (((𝐴 · 𝑏) mod 1) − ((𝐴 · 𝑎) mod 1))) |
| 76 | 75 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) = (abs‘(((𝐴 · 𝑏) mod 1) − ((𝐴 · 𝑎) mod 1)))) |
| 77 | | 1rp 13038 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ+ |
| 78 | 77 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → 1 ∈
ℝ+) |
| 79 | 44, 78 | modcld 13915 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑏) mod 1) ∈ ℝ) |
| 80 | 79 | recnd 11289 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑏) mod 1) ∈ ℂ) |
| 81 | 43, 78 | modcld 13915 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑎) mod 1) ∈ ℝ) |
| 82 | 81 | recnd 11289 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((𝐴 · 𝑎) mod 1) ∈ ℂ) |
| 83 | 80, 82 | abssubd 15492 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (abs‘(((𝐴 · 𝑏) mod 1) − ((𝐴 · 𝑎) mod 1))) = (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1)))) |
| 84 | 76, 83 | eqtr2d 2778 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) = (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎)))))) |
| 85 | 84 | breq1d 5153 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵) ↔ (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) < (1 / 𝐵))) |
| 86 | 85 | biimpd 229 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ 𝑎 < 𝑏) → ((abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵) → (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) < (1 / 𝐵))) |
| 87 | 86 | impr 454 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ (𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵))) → (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) < (1 / 𝐵)) |
| 88 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = (𝑏 − 𝑎) → (𝐴 · 𝑥) = (𝐴 · (𝑏 − 𝑎))) |
| 89 | 88 | fvoveq1d 7453 |
. . . . . . 7
⊢ (𝑥 = (𝑏 − 𝑎) → (abs‘((𝐴 · 𝑥) − 𝑦)) = (abs‘((𝐴 · (𝑏 − 𝑎)) − 𝑦))) |
| 90 | 89 | breq1d 5153 |
. . . . . 6
⊢ (𝑥 = (𝑏 − 𝑎) → ((abs‘((𝐴 · 𝑥) − 𝑦)) < (1 / 𝐵) ↔ (abs‘((𝐴 · (𝑏 − 𝑎)) − 𝑦)) < (1 / 𝐵))) |
| 91 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑦 = ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) → ((𝐴 · (𝑏 − 𝑎)) − 𝑦) = ((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) |
| 92 | 91 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑦 = ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) → (abs‘((𝐴 · (𝑏 − 𝑎)) − 𝑦)) = (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎)))))) |
| 93 | 92 | breq1d 5153 |
. . . . . 6
⊢ (𝑦 = ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) → ((abs‘((𝐴 · (𝑏 − 𝑎)) − 𝑦)) < (1 / 𝐵) ↔ (abs‘((𝐴 · (𝑏 − 𝑎)) − ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))))) < (1 / 𝐵))) |
| 94 | 90, 93 | rspc2ev 3635 |
. . . . 5
⊢ (((𝑏 − 𝑎) ∈ (1...𝐵) ∧ ((⌊‘(𝐴 · 𝑏)) − (⌊‘(𝐴 · 𝑎))) ∈ ℕ0 ∧
(abs‘((𝐴 ·
(𝑏 − 𝑎)) −
((⌊‘(𝐴 ·
𝑏)) −
(⌊‘(𝐴 ·
𝑎))))) < (1 / 𝐵)) → ∃𝑥 ∈ (1...𝐵)∃𝑦 ∈ ℕ0
(abs‘((𝐴 ·
𝑥) − 𝑦)) < (1 / 𝐵)) |
| 95 | 40, 56, 87, 94 | syl3anc 1373 |
. . . 4
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) ∧ (𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵))) → ∃𝑥 ∈ (1...𝐵)∃𝑦 ∈ ℕ0
(abs‘((𝐴 ·
𝑥) − 𝑦)) < (1 / 𝐵)) |
| 96 | 95 | ex 412 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
∧ (𝑎 ∈ (0...𝐵) ∧ 𝑏 ∈ (0...𝐵))) → ((𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵)) → ∃𝑥 ∈ (1...𝐵)∃𝑦 ∈ ℕ0
(abs‘((𝐴 ·
𝑥) − 𝑦)) < (1 / 𝐵))) |
| 97 | 96 | rexlimdvva 3213 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
→ (∃𝑎 ∈
(0...𝐵)∃𝑏 ∈ (0...𝐵)(𝑎 < 𝑏 ∧ (abs‘(((𝐴 · 𝑎) mod 1) − ((𝐴 · 𝑏) mod 1))) < (1 / 𝐵)) → ∃𝑥 ∈ (1...𝐵)∃𝑦 ∈ ℕ0
(abs‘((𝐴 ·
𝑥) − 𝑦)) < (1 / 𝐵))) |
| 98 | 1, 97 | mpd 15 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℕ)
→ ∃𝑥 ∈
(1...𝐵)∃𝑦 ∈ ℕ0
(abs‘((𝐴 ·
𝑥) − 𝑦)) < (1 / 𝐵)) |