| Step |
Hyp |
Ref |
Expression |
| 1 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℝ+ ) |
| 2 |
1
|
rpreccld |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 1 / 𝐵 ) ∈ ℝ+ ) |
| 3 |
2
|
rprege0d |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( ( 1 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝐵 ) ) ) |
| 4 |
|
flge0nn0 |
⊢ ( ( ( 1 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝐵 ) ) → ( ⌊ ‘ ( 1 / 𝐵 ) ) ∈ ℕ0 ) |
| 5 |
|
nn0p1nn |
⊢ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) ∈ ℕ ) |
| 6 |
3 4 5
|
3syl |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) ∈ ℕ ) |
| 7 |
|
irrapxlem4 |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) ∈ ℕ ) → ∃ 𝑎 ∈ ℕ ∃ 𝑏 ∈ ℕ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) |
| 8 |
6 7
|
syldan |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑎 ∈ ℕ ∃ 𝑏 ∈ ℕ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) |
| 9 |
|
simplrr |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝑏 ∈ ℕ ) |
| 10 |
|
nnq |
⊢ ( 𝑏 ∈ ℕ → 𝑏 ∈ ℚ ) |
| 11 |
9 10
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝑏 ∈ ℚ ) |
| 12 |
|
simplrl |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝑎 ∈ ℕ ) |
| 13 |
|
nnq |
⊢ ( 𝑎 ∈ ℕ → 𝑎 ∈ ℚ ) |
| 14 |
12 13
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝑎 ∈ ℚ ) |
| 15 |
12
|
nnne0d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝑎 ≠ 0 ) |
| 16 |
|
qdivcl |
⊢ ( ( 𝑏 ∈ ℚ ∧ 𝑎 ∈ ℚ ∧ 𝑎 ≠ 0 ) → ( 𝑏 / 𝑎 ) ∈ ℚ ) |
| 17 |
11 14 15 16
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑏 / 𝑎 ) ∈ ℚ ) |
| 18 |
9
|
nnrpd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝑏 ∈ ℝ+ ) |
| 19 |
12
|
nnrpd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝑎 ∈ ℝ+ ) |
| 20 |
18 19
|
rpdivcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑏 / 𝑎 ) ∈ ℝ+ ) |
| 21 |
20
|
rpgt0d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 0 < ( 𝑏 / 𝑎 ) ) |
| 22 |
12
|
nnred |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝑎 ∈ ℝ ) |
| 23 |
12
|
nnnn0d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝑎 ∈ ℕ0 ) |
| 24 |
23
|
nn0ge0d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 0 ≤ 𝑎 ) |
| 25 |
22 24
|
absidd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( abs ‘ 𝑎 ) = 𝑎 ) |
| 26 |
25
|
eqcomd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝑎 = ( abs ‘ 𝑎 ) ) |
| 27 |
26
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑎 · ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ) = ( ( abs ‘ 𝑎 ) · ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ) ) |
| 28 |
12
|
nncnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝑎 ∈ ℂ ) |
| 29 |
|
qre |
⊢ ( ( 𝑏 / 𝑎 ) ∈ ℚ → ( 𝑏 / 𝑎 ) ∈ ℝ ) |
| 30 |
17 29
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑏 / 𝑎 ) ∈ ℝ ) |
| 31 |
|
rpre |
⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ ) |
| 32 |
31
|
ad3antrrr |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝐴 ∈ ℝ ) |
| 33 |
30 32
|
resubcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( 𝑏 / 𝑎 ) − 𝐴 ) ∈ ℝ ) |
| 34 |
33
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( 𝑏 / 𝑎 ) − 𝐴 ) ∈ ℂ ) |
| 35 |
28 34
|
absmuld |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( abs ‘ ( 𝑎 · ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ) = ( ( abs ‘ 𝑎 ) · ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ) ) |
| 36 |
27 35
|
eqtr4d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑎 · ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ) = ( abs ‘ ( 𝑎 · ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ) ) |
| 37 |
|
qcn |
⊢ ( ( 𝑏 / 𝑎 ) ∈ ℚ → ( 𝑏 / 𝑎 ) ∈ ℂ ) |
| 38 |
17 37
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑏 / 𝑎 ) ∈ ℂ ) |
| 39 |
|
rpcn |
⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ ) |
| 40 |
39
|
ad3antrrr |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝐴 ∈ ℂ ) |
| 41 |
28 38 40
|
subdid |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑎 · ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) = ( ( 𝑎 · ( 𝑏 / 𝑎 ) ) − ( 𝑎 · 𝐴 ) ) ) |
| 42 |
9
|
nncnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝑏 ∈ ℂ ) |
| 43 |
42 28 15
|
divcan2d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑎 · ( 𝑏 / 𝑎 ) ) = 𝑏 ) |
| 44 |
28 40
|
mulcomd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑎 · 𝐴 ) = ( 𝐴 · 𝑎 ) ) |
| 45 |
43 44
|
oveq12d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( 𝑎 · ( 𝑏 / 𝑎 ) ) − ( 𝑎 · 𝐴 ) ) = ( 𝑏 − ( 𝐴 · 𝑎 ) ) ) |
| 46 |
41 45
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑎 · ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) = ( 𝑏 − ( 𝐴 · 𝑎 ) ) ) |
| 47 |
46
|
fveq2d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( abs ‘ ( 𝑎 · ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ) = ( abs ‘ ( 𝑏 − ( 𝐴 · 𝑎 ) ) ) ) |
| 48 |
32 22
|
remulcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝐴 · 𝑎 ) ∈ ℝ ) |
| 49 |
48
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝐴 · 𝑎 ) ∈ ℂ ) |
| 50 |
42 49
|
abssubd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( abs ‘ ( 𝑏 − ( 𝐴 · 𝑎 ) ) ) = ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) ) |
| 51 |
36 47 50
|
3eqtrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑎 · ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ) = ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) ) |
| 52 |
9
|
nnred |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝑏 ∈ ℝ ) |
| 53 |
48 52
|
resubcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( 𝐴 · 𝑎 ) − 𝑏 ) ∈ ℝ ) |
| 54 |
53
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( 𝐴 · 𝑎 ) − 𝑏 ) ∈ ℂ ) |
| 55 |
54
|
abscld |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) ∈ ℝ ) |
| 56 |
|
simpllr |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝐵 ∈ ℝ+ ) |
| 57 |
56
|
rprecred |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 / 𝐵 ) ∈ ℝ ) |
| 58 |
56
|
rpreccld |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 / 𝐵 ) ∈ ℝ+ ) |
| 59 |
58
|
rpge0d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 0 ≤ ( 1 / 𝐵 ) ) |
| 60 |
57 59 4
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ⌊ ‘ ( 1 / 𝐵 ) ) ∈ ℕ0 ) |
| 61 |
60 5
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) ∈ ℕ ) |
| 62 |
61
|
nnrpd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) ∈ ℝ+ ) |
| 63 |
62 19
|
ifcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ∈ ℝ+ ) |
| 64 |
63
|
rprecred |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ∈ ℝ ) |
| 65 |
56
|
rpred |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝐵 ∈ ℝ ) |
| 66 |
22 65
|
remulcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑎 · 𝐵 ) ∈ ℝ ) |
| 67 |
|
simpr |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) |
| 68 |
58
|
rprecred |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 / ( 1 / 𝐵 ) ) ∈ ℝ ) |
| 69 |
61
|
nnred |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) ∈ ℝ ) |
| 70 |
69 22
|
ifcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ∈ ℝ ) |
| 71 |
|
fllep1 |
⊢ ( ( 1 / 𝐵 ) ∈ ℝ → ( 1 / 𝐵 ) ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) ) |
| 72 |
57 71
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 / 𝐵 ) ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) ) |
| 73 |
|
max2 |
⊢ ( ( 𝑎 ∈ ℝ ∧ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) ∈ ℝ ) → ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) ≤ if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) |
| 74 |
22 69 73
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) ≤ if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) |
| 75 |
57 69 70 72 74
|
letrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 / 𝐵 ) ≤ if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) |
| 76 |
58 63
|
lerecd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( 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 |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ≤ ( 1 / ( 1 / 𝐵 ) ) ) |
| 78 |
65
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝐵 ∈ ℂ ) |
| 79 |
56
|
rpne0d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝐵 ≠ 0 ) |
| 80 |
78 79
|
recrecd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 / ( 1 / 𝐵 ) ) = 𝐵 ) |
| 81 |
78
|
mulid2d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 · 𝐵 ) = 𝐵 ) |
| 82 |
80 81
|
eqtr4d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 / ( 1 / 𝐵 ) ) = ( 1 · 𝐵 ) ) |
| 83 |
12
|
nnge1d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 1 ≤ 𝑎 ) |
| 84 |
|
1red |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 1 ∈ ℝ ) |
| 85 |
84 22 56
|
lemul1d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 ≤ 𝑎 ↔ ( 1 · 𝐵 ) ≤ ( 𝑎 · 𝐵 ) ) ) |
| 86 |
83 85
|
mpbid |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 · 𝐵 ) ≤ ( 𝑎 · 𝐵 ) ) |
| 87 |
82 86
|
eqbrtrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 / ( 1 / 𝐵 ) ) ≤ ( 𝑎 · 𝐵 ) ) |
| 88 |
64 68 66 77 87
|
letrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ≤ ( 𝑎 · 𝐵 ) ) |
| 89 |
55 64 66 67 88
|
ltletrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 𝑎 · 𝐵 ) ) |
| 90 |
51 89
|
eqbrtrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑎 · ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ) < ( 𝑎 · 𝐵 ) ) |
| 91 |
34
|
abscld |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ∈ ℝ ) |
| 92 |
12
|
nngt0d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 0 < 𝑎 ) |
| 93 |
|
ltmul2 |
⊢ ( ( ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝑎 ∈ ℝ ∧ 0 < 𝑎 ) ) → ( ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) < 𝐵 ↔ ( 𝑎 · ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ) < ( 𝑎 · 𝐵 ) ) ) |
| 94 |
91 65 22 92 93
|
syl112anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) < 𝐵 ↔ ( 𝑎 · ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ) < ( 𝑎 · 𝐵 ) ) ) |
| 95 |
90 94
|
mpbird |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) < 𝐵 ) |
| 96 |
22 22
|
remulcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑎 · 𝑎 ) ∈ ℝ ) |
| 97 |
22 15
|
msqgt0d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 0 < ( 𝑎 · 𝑎 ) ) |
| 98 |
97
|
gt0ne0d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑎 · 𝑎 ) ≠ 0 ) |
| 99 |
96 98
|
rereccld |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 / ( 𝑎 · 𝑎 ) ) ∈ ℝ ) |
| 100 |
|
qdencl |
⊢ ( ( 𝑏 / 𝑎 ) ∈ ℚ → ( denom ‘ ( 𝑏 / 𝑎 ) ) ∈ ℕ ) |
| 101 |
17 100
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( denom ‘ ( 𝑏 / 𝑎 ) ) ∈ ℕ ) |
| 102 |
101
|
nnred |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( denom ‘ ( 𝑏 / 𝑎 ) ) ∈ ℝ ) |
| 103 |
102 102
|
remulcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ∈ ℝ ) |
| 104 |
101
|
nnne0d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( denom ‘ ( 𝑏 / 𝑎 ) ) ≠ 0 ) |
| 105 |
102 104
|
msqgt0d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 0 < ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ) |
| 106 |
105
|
gt0ne0d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ≠ 0 ) |
| 107 |
103 106
|
rereccld |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 / ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ) ∈ ℝ ) |
| 108 |
22 15
|
rereccld |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 / 𝑎 ) ∈ ℝ ) |
| 109 |
|
max1 |
⊢ ( ( 𝑎 ∈ ℝ ∧ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) ∈ ℝ ) → 𝑎 ≤ if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) |
| 110 |
22 69 109
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝑎 ≤ if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) |
| 111 |
19 63
|
lerecd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑎 ≤ if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ↔ ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ≤ ( 1 / 𝑎 ) ) ) |
| 112 |
110 111
|
mpbid |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ≤ ( 1 / 𝑎 ) ) |
| 113 |
55 64 108 67 112
|
ltletrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / 𝑎 ) ) |
| 114 |
28 28 28 15 15
|
divdiv1d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( 𝑎 / 𝑎 ) / 𝑎 ) = ( 𝑎 / ( 𝑎 · 𝑎 ) ) ) |
| 115 |
28 15
|
dividd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑎 / 𝑎 ) = 1 ) |
| 116 |
115
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( 𝑎 / 𝑎 ) / 𝑎 ) = ( 1 / 𝑎 ) ) |
| 117 |
96
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑎 · 𝑎 ) ∈ ℂ ) |
| 118 |
28 117 98
|
divrecd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑎 / ( 𝑎 · 𝑎 ) ) = ( 𝑎 · ( 1 / ( 𝑎 · 𝑎 ) ) ) ) |
| 119 |
114 116 118
|
3eqtr3rd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑎 · ( 1 / ( 𝑎 · 𝑎 ) ) ) = ( 1 / 𝑎 ) ) |
| 120 |
113 51 119
|
3brtr4d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 𝑎 · ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ) < ( 𝑎 · ( 1 / ( 𝑎 · 𝑎 ) ) ) ) |
| 121 |
|
ltmul2 |
⊢ ( ( ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ∈ ℝ ∧ ( 1 / ( 𝑎 · 𝑎 ) ) ∈ ℝ ∧ ( 𝑎 ∈ ℝ ∧ 0 < 𝑎 ) ) → ( ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) < ( 1 / ( 𝑎 · 𝑎 ) ) ↔ ( 𝑎 · ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ) < ( 𝑎 · ( 1 / ( 𝑎 · 𝑎 ) ) ) ) ) |
| 122 |
91 99 22 92 121
|
syl112anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) < ( 1 / ( 𝑎 · 𝑎 ) ) ↔ ( 𝑎 · ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ) < ( 𝑎 · ( 1 / ( 𝑎 · 𝑎 ) ) ) ) ) |
| 123 |
120 122
|
mpbird |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) < ( 1 / ( 𝑎 · 𝑎 ) ) ) |
| 124 |
9
|
nnzd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 𝑏 ∈ ℤ ) |
| 125 |
|
divdenle |
⊢ ( ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℕ ) → ( denom ‘ ( 𝑏 / 𝑎 ) ) ≤ 𝑎 ) |
| 126 |
124 12 125
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( denom ‘ ( 𝑏 / 𝑎 ) ) ≤ 𝑎 ) |
| 127 |
101
|
nnnn0d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( denom ‘ ( 𝑏 / 𝑎 ) ) ∈ ℕ0 ) |
| 128 |
127
|
nn0ge0d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → 0 ≤ ( denom ‘ ( 𝑏 / 𝑎 ) ) ) |
| 129 |
|
le2msq |
⊢ ( ( ( ( denom ‘ ( 𝑏 / 𝑎 ) ) ∈ ℝ ∧ 0 ≤ ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ∧ ( 𝑎 ∈ ℝ ∧ 0 ≤ 𝑎 ) ) → ( ( denom ‘ ( 𝑏 / 𝑎 ) ) ≤ 𝑎 ↔ ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ≤ ( 𝑎 · 𝑎 ) ) ) |
| 130 |
102 128 22 24 129
|
syl22anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( denom ‘ ( 𝑏 / 𝑎 ) ) ≤ 𝑎 ↔ ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ≤ ( 𝑎 · 𝑎 ) ) ) |
| 131 |
126 130
|
mpbid |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ≤ ( 𝑎 · 𝑎 ) ) |
| 132 |
|
lerec |
⊢ ( ( ( ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ∈ ℝ ∧ 0 < ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ) ∧ ( ( 𝑎 · 𝑎 ) ∈ ℝ ∧ 0 < ( 𝑎 · 𝑎 ) ) ) → ( ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ≤ ( 𝑎 · 𝑎 ) ↔ ( 1 / ( 𝑎 · 𝑎 ) ) ≤ ( 1 / ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ) ) ) |
| 133 |
103 105 96 97 132
|
syl22anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ≤ ( 𝑎 · 𝑎 ) ↔ ( 1 / ( 𝑎 · 𝑎 ) ) ≤ ( 1 / ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ) ) ) |
| 134 |
131 133
|
mpbid |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 / ( 𝑎 · 𝑎 ) ) ≤ ( 1 / ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ) ) |
| 135 |
91 99 107 123 134
|
ltletrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) < ( 1 / ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ) ) |
| 136 |
101
|
nncnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( denom ‘ ( 𝑏 / 𝑎 ) ) ∈ ℂ ) |
| 137 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
| 138 |
|
expneg |
⊢ ( ( ( denom ‘ ( 𝑏 / 𝑎 ) ) ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( ( denom ‘ ( 𝑏 / 𝑎 ) ) ↑ - 2 ) = ( 1 / ( ( denom ‘ ( 𝑏 / 𝑎 ) ) ↑ 2 ) ) ) |
| 139 |
136 137 138
|
sylancl |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( denom ‘ ( 𝑏 / 𝑎 ) ) ↑ - 2 ) = ( 1 / ( ( denom ‘ ( 𝑏 / 𝑎 ) ) ↑ 2 ) ) ) |
| 140 |
136
|
sqvald |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( denom ‘ ( 𝑏 / 𝑎 ) ) ↑ 2 ) = ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ) |
| 141 |
140
|
oveq2d |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( 1 / ( ( denom ‘ ( 𝑏 / 𝑎 ) ) ↑ 2 ) ) = ( 1 / ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ) ) |
| 142 |
139 141
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( ( denom ‘ ( 𝑏 / 𝑎 ) ) ↑ - 2 ) = ( 1 / ( ( denom ‘ ( 𝑏 / 𝑎 ) ) · ( denom ‘ ( 𝑏 / 𝑎 ) ) ) ) ) |
| 143 |
135 142
|
breqtrrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) < ( ( denom ‘ ( 𝑏 / 𝑎 ) ) ↑ - 2 ) ) |
| 144 |
|
breq2 |
⊢ ( 𝑥 = ( 𝑏 / 𝑎 ) → ( 0 < 𝑥 ↔ 0 < ( 𝑏 / 𝑎 ) ) ) |
| 145 |
|
fvoveq1 |
⊢ ( 𝑥 = ( 𝑏 / 𝑎 ) → ( abs ‘ ( 𝑥 − 𝐴 ) ) = ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) ) |
| 146 |
145
|
breq1d |
⊢ ( 𝑥 = ( 𝑏 / 𝑎 ) → ( ( abs ‘ ( 𝑥 − 𝐴 ) ) < 𝐵 ↔ ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) < 𝐵 ) ) |
| 147 |
|
fveq2 |
⊢ ( 𝑥 = ( 𝑏 / 𝑎 ) → ( denom ‘ 𝑥 ) = ( denom ‘ ( 𝑏 / 𝑎 ) ) ) |
| 148 |
147
|
oveq1d |
⊢ ( 𝑥 = ( 𝑏 / 𝑎 ) → ( ( denom ‘ 𝑥 ) ↑ - 2 ) = ( ( denom ‘ ( 𝑏 / 𝑎 ) ) ↑ - 2 ) ) |
| 149 |
145 148
|
breq12d |
⊢ ( 𝑥 = ( 𝑏 / 𝑎 ) → ( ( abs ‘ ( 𝑥 − 𝐴 ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ↔ ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) < ( ( denom ‘ ( 𝑏 / 𝑎 ) ) ↑ - 2 ) ) ) |
| 150 |
144 146 149
|
3anbi123d |
⊢ ( 𝑥 = ( 𝑏 / 𝑎 ) → ( ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − 𝐴 ) ) < 𝐵 ∧ ( abs ‘ ( 𝑥 − 𝐴 ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) ↔ ( 0 < ( 𝑏 / 𝑎 ) ∧ ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) < 𝐵 ∧ ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) < ( ( denom ‘ ( 𝑏 / 𝑎 ) ) ↑ - 2 ) ) ) ) |
| 151 |
150
|
rspcev |
⊢ ( ( ( 𝑏 / 𝑎 ) ∈ ℚ ∧ ( 0 < ( 𝑏 / 𝑎 ) ∧ ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) < 𝐵 ∧ ( abs ‘ ( ( 𝑏 / 𝑎 ) − 𝐴 ) ) < ( ( denom ‘ ( 𝑏 / 𝑎 ) ) ↑ - 2 ) ) ) → ∃ 𝑥 ∈ ℚ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − 𝐴 ) ) < 𝐵 ∧ ( abs ‘ ( 𝑥 − 𝐴 ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) ) |
| 152 |
17 21 95 143 151
|
syl13anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) ) → ∃ 𝑥 ∈ ℚ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − 𝐴 ) ) < 𝐵 ∧ ( abs ‘ ( 𝑥 − 𝐴 ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) ) |
| 153 |
152
|
ex |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) → ∃ 𝑥 ∈ ℚ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − 𝐴 ) ) < 𝐵 ∧ ( abs ‘ ( 𝑥 − 𝐴 ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) ) ) |
| 154 |
153
|
rexlimdvva |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( ∃ 𝑎 ∈ ℕ ∃ 𝑏 ∈ ℕ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐵 ) ) + 1 ) , 𝑎 ) ) → ∃ 𝑥 ∈ ℚ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − 𝐴 ) ) < 𝐵 ∧ ( abs ‘ ( 𝑥 − 𝐴 ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) ) ) |
| 155 |
8 154
|
mpd |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑥 ∈ ℚ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − 𝐴 ) ) < 𝐵 ∧ ( abs ‘ ( 𝑥 − 𝐴 ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) ) |