| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) → 𝐵 ∈
ℝ+) |
| 2 | 1 | rpreccld 13087 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) → (1 / 𝐵) ∈
ℝ+) |
| 3 | 2 | rprege0d 13084 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) → ((1 / 𝐵) ∈ ℝ ∧ 0 ≤ (1 / 𝐵))) |
| 4 | | flge0nn0 13860 |
. . . 4
⊢ (((1 /
𝐵) ∈ ℝ ∧ 0
≤ (1 / 𝐵)) →
(⌊‘(1 / 𝐵))
∈ ℕ0) |
| 5 | | nn0p1nn 12565 |
. . . 4
⊢
((⌊‘(1 / 𝐵)) ∈ ℕ0 →
((⌊‘(1 / 𝐵)) +
1) ∈ ℕ) |
| 6 | 3, 4, 5 | 3syl 18 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) → ((⌊‘(1 / 𝐵)) + 1) ∈ ℕ) |
| 7 | | irrapxlem4 42836 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ ((⌊‘(1 / 𝐵)) + 1) ∈ ℕ) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ
(abs‘((𝐴 ·
𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 /
𝐵)) + 1), 𝑎))) |
| 8 | 6, 7 | syldan 591 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) |
| 9 | | simplrr 778 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑏 ∈ ℕ) |
| 10 | | nnq 13004 |
. . . . . . 7
⊢ (𝑏 ∈ ℕ → 𝑏 ∈
ℚ) |
| 11 | 9, 10 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑏 ∈ ℚ) |
| 12 | | simplrl 777 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 ∈ ℕ) |
| 13 | | nnq 13004 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℚ) |
| 14 | 12, 13 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 ∈ ℚ) |
| 15 | 12 | nnne0d 12316 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 ≠ 0) |
| 16 | | qdivcl 13012 |
. . . . . 6
⊢ ((𝑏 ∈ ℚ ∧ 𝑎 ∈ ℚ ∧ 𝑎 ≠ 0) → (𝑏 / 𝑎) ∈ ℚ) |
| 17 | 11, 14, 15, 16 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑏 / 𝑎) ∈ ℚ) |
| 18 | 9 | nnrpd 13075 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑏 ∈ ℝ+) |
| 19 | 12 | nnrpd 13075 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 ∈ ℝ+) |
| 20 | 18, 19 | rpdivcld 13094 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑏 / 𝑎) ∈
ℝ+) |
| 21 | 20 | rpgt0d 13080 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 0 < (𝑏 / 𝑎)) |
| 22 | 12 | nnred 12281 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 ∈ ℝ) |
| 23 | 12 | nnnn0d 12587 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 ∈ ℕ0) |
| 24 | 23 | nn0ge0d 12590 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 0 ≤ 𝑎) |
| 25 | 22, 24 | absidd 15461 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘𝑎) = 𝑎) |
| 26 | 25 | eqcomd 2743 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 = (abs‘𝑎)) |
| 27 | 26 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) = ((abs‘𝑎) · (abs‘((𝑏 / 𝑎) − 𝐴)))) |
| 28 | 12 | nncnd 12282 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 ∈ ℂ) |
| 29 | | qre 12995 |
. . . . . . . . . . . . 13
⊢ ((𝑏 / 𝑎) ∈ ℚ → (𝑏 / 𝑎) ∈ ℝ) |
| 30 | 17, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑏 / 𝑎) ∈ ℝ) |
| 31 | | rpre 13043 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
| 32 | 31 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝐴 ∈ ℝ) |
| 33 | 30, 32 | resubcld 11691 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((𝑏 / 𝑎) − 𝐴) ∈ ℝ) |
| 34 | 33 | recnd 11289 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((𝑏 / 𝑎) − 𝐴) ∈ ℂ) |
| 35 | 28, 34 | absmuld 15493 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘(𝑎 · ((𝑏 / 𝑎) − 𝐴))) = ((abs‘𝑎) · (abs‘((𝑏 / 𝑎) − 𝐴)))) |
| 36 | 27, 35 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) = (abs‘(𝑎 · ((𝑏 / 𝑎) − 𝐴)))) |
| 37 | | qcn 13005 |
. . . . . . . . . . . 12
⊢ ((𝑏 / 𝑎) ∈ ℚ → (𝑏 / 𝑎) ∈ ℂ) |
| 38 | 17, 37 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑏 / 𝑎) ∈ ℂ) |
| 39 | | rpcn 13045 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℂ) |
| 40 | 39 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝐴 ∈ ℂ) |
| 41 | 28, 38, 40 | subdid 11719 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · ((𝑏 / 𝑎) − 𝐴)) = ((𝑎 · (𝑏 / 𝑎)) − (𝑎 · 𝐴))) |
| 42 | 9 | nncnd 12282 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑏 ∈ ℂ) |
| 43 | 42, 28, 15 | divcan2d 12045 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · (𝑏 / 𝑎)) = 𝑏) |
| 44 | 28, 40 | mulcomd 11282 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · 𝐴) = (𝐴 · 𝑎)) |
| 45 | 43, 44 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((𝑎 · (𝑏 / 𝑎)) − (𝑎 · 𝐴)) = (𝑏 − (𝐴 · 𝑎))) |
| 46 | 41, 45 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · ((𝑏 / 𝑎) − 𝐴)) = (𝑏 − (𝐴 · 𝑎))) |
| 47 | 46 | fveq2d 6910 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘(𝑎 · ((𝑏 / 𝑎) − 𝐴))) = (abs‘(𝑏 − (𝐴 · 𝑎)))) |
| 48 | 32, 22 | remulcld 11291 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝐴 · 𝑎) ∈ ℝ) |
| 49 | 48 | recnd 11289 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝐴 · 𝑎) ∈ ℂ) |
| 50 | 42, 49 | abssubd 15492 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘(𝑏 − (𝐴 · 𝑎))) = (abs‘((𝐴 · 𝑎) − 𝑏))) |
| 51 | 36, 47, 50 | 3eqtrd 2781 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) = (abs‘((𝐴 · 𝑎) − 𝑏))) |
| 52 | 9 | nnred 12281 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑏 ∈ ℝ) |
| 53 | 48, 52 | resubcld 11691 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((𝐴 · 𝑎) − 𝑏) ∈ ℝ) |
| 54 | 53 | recnd 11289 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((𝐴 · 𝑎) − 𝑏) ∈ ℂ) |
| 55 | 54 | abscld 15475 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝐴 · 𝑎) − 𝑏)) ∈ ℝ) |
| 56 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝐵 ∈
ℝ+) |
| 57 | 56 | rprecred 13088 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / 𝐵) ∈ ℝ) |
| 58 | 56 | rpreccld 13087 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / 𝐵) ∈
ℝ+) |
| 59 | 58 | rpge0d 13081 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 0 ≤ (1 / 𝐵)) |
| 60 | 57, 59, 4 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (⌊‘(1 / 𝐵)) ∈
ℕ0) |
| 61 | 60, 5 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((⌊‘(1 / 𝐵)) + 1) ∈
ℕ) |
| 62 | 61 | nnrpd 13075 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((⌊‘(1 / 𝐵)) + 1) ∈
ℝ+) |
| 63 | 62, 19 | ifcld 4572 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎) ∈
ℝ+) |
| 64 | 63 | rprecred 13088 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) ∈ ℝ) |
| 65 | 56 | rpred 13077 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝐵 ∈ ℝ) |
| 66 | 22, 65 | remulcld 11291 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · 𝐵) ∈ ℝ) |
| 67 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) |
| 68 | 58 | rprecred 13088 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / (1 / 𝐵)) ∈ ℝ) |
| 69 | 61 | nnred 12281 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((⌊‘(1 / 𝐵)) + 1) ∈
ℝ) |
| 70 | 69, 22 | ifcld 4572 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎) ∈ ℝ) |
| 71 | | fllep1 13841 |
. . . . . . . . . . . 12
⊢ ((1 /
𝐵) ∈ ℝ → (1
/ 𝐵) ≤
((⌊‘(1 / 𝐵)) +
1)) |
| 72 | 57, 71 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / 𝐵) ≤ ((⌊‘(1 / 𝐵)) + 1)) |
| 73 | | max2 13229 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ ∧
((⌊‘(1 / 𝐵)) +
1) ∈ ℝ) → ((⌊‘(1 / 𝐵)) + 1) ≤ if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) |
| 74 | 22, 69, 73 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((⌊‘(1 / 𝐵)) + 1) ≤ if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 /
𝐵)) + 1), 𝑎)) |
| 75 | 57, 69, 70, 72, 74 | letrd 11418 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / 𝐵) ≤ if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) |
| 76 | 58, 63 | lerecd 13096 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((1 / 𝐵) ≤ if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎) ↔ (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) ≤ (1 / (1 / 𝐵)))) |
| 77 | 75, 76 | mpbid 232 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) ≤ (1 / (1 / 𝐵))) |
| 78 | 65 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝐵 ∈ ℂ) |
| 79 | 56 | rpne0d 13082 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝐵 ≠ 0) |
| 80 | 78, 79 | recrecd 12040 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / (1 / 𝐵)) = 𝐵) |
| 81 | 78 | mullidd 11279 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 · 𝐵) = 𝐵) |
| 82 | 80, 81 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / (1 / 𝐵)) = (1 · 𝐵)) |
| 83 | 12 | nnge1d 12314 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 1 ≤ 𝑎) |
| 84 | | 1red 11262 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 1 ∈ ℝ) |
| 85 | 84, 22, 56 | lemul1d 13120 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 ≤ 𝑎 ↔ (1 · 𝐵) ≤ (𝑎 · 𝐵))) |
| 86 | 83, 85 | mpbid 232 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 · 𝐵) ≤ (𝑎 · 𝐵)) |
| 87 | 82, 86 | eqbrtrd 5165 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / (1 / 𝐵)) ≤ (𝑎 · 𝐵)) |
| 88 | 64, 68, 66, 77, 87 | letrd 11418 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) ≤ (𝑎 · 𝐵)) |
| 89 | 55, 64, 66, 67, 88 | ltletrd 11421 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝐴 · 𝑎) − 𝑏)) < (𝑎 · 𝐵)) |
| 90 | 51, 89 | eqbrtrd 5165 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) < (𝑎 · 𝐵)) |
| 91 | 34 | abscld 15475 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝑏 / 𝑎) − 𝐴)) ∈ ℝ) |
| 92 | 12 | nngt0d 12315 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 0 < 𝑎) |
| 93 | | ltmul2 12118 |
. . . . . . 7
⊢
(((abs‘((𝑏 /
𝑎) − 𝐴)) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑎 ∈ ℝ ∧ 0 <
𝑎)) →
((abs‘((𝑏 / 𝑎) − 𝐴)) < 𝐵 ↔ (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) < (𝑎 · 𝐵))) |
| 94 | 91, 65, 22, 92, 93 | syl112anc 1376 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((abs‘((𝑏 / 𝑎) − 𝐴)) < 𝐵 ↔ (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) < (𝑎 · 𝐵))) |
| 95 | 90, 94 | mpbird 257 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝑏 / 𝑎) − 𝐴)) < 𝐵) |
| 96 | 22, 22 | remulcld 11291 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · 𝑎) ∈ ℝ) |
| 97 | 22, 15 | msqgt0d 11830 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 0 < (𝑎 · 𝑎)) |
| 98 | 97 | gt0ne0d 11827 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · 𝑎) ≠ 0) |
| 99 | 96, 98 | rereccld 12094 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / (𝑎 · 𝑎)) ∈ ℝ) |
| 100 | | qdencl 16778 |
. . . . . . . . . . 11
⊢ ((𝑏 / 𝑎) ∈ ℚ → (denom‘(𝑏 / 𝑎)) ∈ ℕ) |
| 101 | 17, 100 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (denom‘(𝑏 / 𝑎)) ∈ ℕ) |
| 102 | 101 | nnred 12281 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (denom‘(𝑏 / 𝑎)) ∈ ℝ) |
| 103 | 102, 102 | remulcld 11291 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))) ∈ ℝ) |
| 104 | 101 | nnne0d 12316 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (denom‘(𝑏 / 𝑎)) ≠ 0) |
| 105 | 102, 104 | msqgt0d 11830 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 0 < ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎)))) |
| 106 | 105 | gt0ne0d 11827 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))) ≠ 0) |
| 107 | 103, 106 | rereccld 12094 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎)))) ∈ ℝ) |
| 108 | 22, 15 | rereccld 12094 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / 𝑎) ∈ ℝ) |
| 109 | | max1 13227 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ ∧
((⌊‘(1 / 𝐵)) +
1) ∈ ℝ) → 𝑎
≤ if(𝑎 ≤
((⌊‘(1 / 𝐵)) +
1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) |
| 110 | 22, 69, 109 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 ≤ if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) |
| 111 | 19, 63 | lerecd 13096 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 ≤ if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎) ↔ (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) ≤ (1 / 𝑎))) |
| 112 | 110, 111 | mpbid 232 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) ≤ (1 / 𝑎)) |
| 113 | 55, 64, 108, 67, 112 | ltletrd 11421 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / 𝑎)) |
| 114 | 28, 28, 28, 15, 15 | divdiv1d 12074 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((𝑎 / 𝑎) / 𝑎) = (𝑎 / (𝑎 · 𝑎))) |
| 115 | 28, 15 | dividd 12041 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 / 𝑎) = 1) |
| 116 | 115 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((𝑎 / 𝑎) / 𝑎) = (1 / 𝑎)) |
| 117 | 96 | recnd 11289 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · 𝑎) ∈ ℂ) |
| 118 | 28, 117, 98 | divrecd 12046 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 / (𝑎 · 𝑎)) = (𝑎 · (1 / (𝑎 · 𝑎)))) |
| 119 | 114, 116,
118 | 3eqtr3rd 2786 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · (1 / (𝑎 · 𝑎))) = (1 / 𝑎)) |
| 120 | 113, 51, 119 | 3brtr4d 5175 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) < (𝑎 · (1 / (𝑎 · 𝑎)))) |
| 121 | | ltmul2 12118 |
. . . . . . . . 9
⊢
(((abs‘((𝑏 /
𝑎) − 𝐴)) ∈ ℝ ∧ (1 /
(𝑎 · 𝑎)) ∈ ℝ ∧ (𝑎 ∈ ℝ ∧ 0 <
𝑎)) →
((abs‘((𝑏 / 𝑎) − 𝐴)) < (1 / (𝑎 · 𝑎)) ↔ (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) < (𝑎 · (1 / (𝑎 · 𝑎))))) |
| 122 | 91, 99, 22, 92, 121 | syl112anc 1376 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((abs‘((𝑏 / 𝑎) − 𝐴)) < (1 / (𝑎 · 𝑎)) ↔ (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) < (𝑎 · (1 / (𝑎 · 𝑎))))) |
| 123 | 120, 122 | mpbird 257 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝑏 / 𝑎) − 𝐴)) < (1 / (𝑎 · 𝑎))) |
| 124 | 9 | nnzd 12640 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑏 ∈ ℤ) |
| 125 | | divdenle 16786 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℕ) →
(denom‘(𝑏 / 𝑎)) ≤ 𝑎) |
| 126 | 124, 12, 125 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (denom‘(𝑏 / 𝑎)) ≤ 𝑎) |
| 127 | 101 | nnnn0d 12587 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (denom‘(𝑏 / 𝑎)) ∈
ℕ0) |
| 128 | 127 | nn0ge0d 12590 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 0 ≤ (denom‘(𝑏 / 𝑎))) |
| 129 | | le2msq 12168 |
. . . . . . . . . 10
⊢
((((denom‘(𝑏 /
𝑎)) ∈ ℝ ∧ 0
≤ (denom‘(𝑏 /
𝑎))) ∧ (𝑎 ∈ ℝ ∧ 0 ≤
𝑎)) →
((denom‘(𝑏 / 𝑎)) ≤ 𝑎 ↔ ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))) ≤ (𝑎 · 𝑎))) |
| 130 | 102, 128,
22, 24, 129 | syl22anc 839 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((denom‘(𝑏 / 𝑎)) ≤ 𝑎 ↔ ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))) ≤ (𝑎 · 𝑎))) |
| 131 | 126, 130 | mpbid 232 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))) ≤ (𝑎 · 𝑎)) |
| 132 | | lerec 12151 |
. . . . . . . . 9
⊢
(((((denom‘(𝑏
/ 𝑎)) ·
(denom‘(𝑏 / 𝑎))) ∈ ℝ ∧ 0 <
((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎)))) ∧ ((𝑎 · 𝑎) ∈ ℝ ∧ 0 < (𝑎 · 𝑎))) → (((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))) ≤ (𝑎 · 𝑎) ↔ (1 / (𝑎 · 𝑎)) ≤ (1 / ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎)))))) |
| 133 | 103, 105,
96, 97, 132 | syl22anc 839 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))) ≤ (𝑎 · 𝑎) ↔ (1 / (𝑎 · 𝑎)) ≤ (1 / ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎)))))) |
| 134 | 131, 133 | mpbid 232 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / (𝑎 · 𝑎)) ≤ (1 / ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))))) |
| 135 | 91, 99, 107, 123, 134 | ltletrd 11421 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝑏 / 𝑎) − 𝐴)) < (1 / ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))))) |
| 136 | 101 | nncnd 12282 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (denom‘(𝑏 / 𝑎)) ∈ ℂ) |
| 137 | | 2nn0 12543 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
| 138 | | expneg 14110 |
. . . . . . . 8
⊢
(((denom‘(𝑏 /
𝑎)) ∈ ℂ ∧ 2
∈ ℕ0) → ((denom‘(𝑏 / 𝑎))↑-2) = (1 / ((denom‘(𝑏 / 𝑎))↑2))) |
| 139 | 136, 137,
138 | sylancl 586 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((denom‘(𝑏 / 𝑎))↑-2) = (1 / ((denom‘(𝑏 / 𝑎))↑2))) |
| 140 | 136 | sqvald 14183 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((denom‘(𝑏 / 𝑎))↑2) = ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎)))) |
| 141 | 140 | oveq2d 7447 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / ((denom‘(𝑏 / 𝑎))↑2)) = (1 / ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))))) |
| 142 | 139, 141 | eqtrd 2777 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((denom‘(𝑏 / 𝑎))↑-2) = (1 / ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))))) |
| 143 | 135, 142 | breqtrrd 5171 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝑏 / 𝑎) − 𝐴)) < ((denom‘(𝑏 / 𝑎))↑-2)) |
| 144 | | breq2 5147 |
. . . . . . 7
⊢ (𝑥 = (𝑏 / 𝑎) → (0 < 𝑥 ↔ 0 < (𝑏 / 𝑎))) |
| 145 | | fvoveq1 7454 |
. . . . . . . 8
⊢ (𝑥 = (𝑏 / 𝑎) → (abs‘(𝑥 − 𝐴)) = (abs‘((𝑏 / 𝑎) − 𝐴))) |
| 146 | 145 | breq1d 5153 |
. . . . . . 7
⊢ (𝑥 = (𝑏 / 𝑎) → ((abs‘(𝑥 − 𝐴)) < 𝐵 ↔ (abs‘((𝑏 / 𝑎) − 𝐴)) < 𝐵)) |
| 147 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = (𝑏 / 𝑎) → (denom‘𝑥) = (denom‘(𝑏 / 𝑎))) |
| 148 | 147 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑥 = (𝑏 / 𝑎) → ((denom‘𝑥)↑-2) = ((denom‘(𝑏 / 𝑎))↑-2)) |
| 149 | 145, 148 | breq12d 5156 |
. . . . . . 7
⊢ (𝑥 = (𝑏 / 𝑎) → ((abs‘(𝑥 − 𝐴)) < ((denom‘𝑥)↑-2) ↔ (abs‘((𝑏 / 𝑎) − 𝐴)) < ((denom‘(𝑏 / 𝑎))↑-2))) |
| 150 | 144, 146,
149 | 3anbi123d 1438 |
. . . . . 6
⊢ (𝑥 = (𝑏 / 𝑎) → ((0 < 𝑥 ∧ (abs‘(𝑥 − 𝐴)) < 𝐵 ∧ (abs‘(𝑥 − 𝐴)) < ((denom‘𝑥)↑-2)) ↔ (0 < (𝑏 / 𝑎) ∧ (abs‘((𝑏 / 𝑎) − 𝐴)) < 𝐵 ∧ (abs‘((𝑏 / 𝑎) − 𝐴)) < ((denom‘(𝑏 / 𝑎))↑-2)))) |
| 151 | 150 | rspcev 3622 |
. . . . 5
⊢ (((𝑏 / 𝑎) ∈ ℚ ∧ (0 < (𝑏 / 𝑎) ∧ (abs‘((𝑏 / 𝑎) − 𝐴)) < 𝐵 ∧ (abs‘((𝑏 / 𝑎) − 𝐴)) < ((denom‘(𝑏 / 𝑎))↑-2))) → ∃𝑥 ∈ ℚ (0 < 𝑥 ∧ (abs‘(𝑥 − 𝐴)) < 𝐵 ∧ (abs‘(𝑥 − 𝐴)) < ((denom‘𝑥)↑-2))) |
| 152 | 17, 21, 95, 143, 151 | syl13anc 1374 |
. . . 4
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ∃𝑥 ∈ ℚ (0 < 𝑥 ∧ (abs‘(𝑥 − 𝐴)) < 𝐵 ∧ (abs‘(𝑥 − 𝐴)) < ((denom‘𝑥)↑-2))) |
| 153 | 152 | ex 412 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → ((abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) → ∃𝑥 ∈ ℚ (0 < 𝑥 ∧ (abs‘(𝑥 − 𝐴)) < 𝐵 ∧ (abs‘(𝑥 − 𝐴)) < ((denom‘𝑥)↑-2)))) |
| 154 | 153 | rexlimdvva 3213 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) → (∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) → ∃𝑥 ∈ ℚ (0 < 𝑥 ∧ (abs‘(𝑥 − 𝐴)) < 𝐵 ∧ (abs‘(𝑥 − 𝐴)) < ((denom‘𝑥)↑-2)))) |
| 155 | 8, 154 | mpd 15 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈
ℝ+) → ∃𝑥 ∈ ℚ (0 < 𝑥 ∧ (abs‘(𝑥 − 𝐴)) < 𝐵 ∧ (abs‘(𝑥 − 𝐴)) < ((denom‘𝑥)↑-2))) |