Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  irrapxlem5 Structured version   Visualization version   GIF version

Theorem irrapxlem5 38071
Description: Lemma for irrapx1 38073. Switching to real intervals and fraction syntax. (Contributed by Stefan O'Rear, 13-Sep-2014.)
Assertion
Ref Expression
irrapxlem5 ((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) → ∃𝑥 ∈ ℚ (0 < 𝑥 ∧ (abs‘(𝑥𝐴)) < 𝐵 ∧ (abs‘(𝑥𝐴)) < ((denom‘𝑥)↑-2)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem irrapxlem5
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 477 . . . . . 6 ((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) → 𝐵 ∈ ℝ+)
21rpreccld 12083 . . . . 5 ((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) → (1 / 𝐵) ∈ ℝ+)
32rprege0d 12080 . . . 4 ((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) → ((1 / 𝐵) ∈ ℝ ∧ 0 ≤ (1 / 𝐵)))
4 flge0nn0 12832 . . . 4 (((1 / 𝐵) ∈ ℝ ∧ 0 ≤ (1 / 𝐵)) → (⌊‘(1 / 𝐵)) ∈ ℕ0)
5 nn0p1nn 11581 . . . 4 ((⌊‘(1 / 𝐵)) ∈ ℕ0 → ((⌊‘(1 / 𝐵)) + 1) ∈ ℕ)
63, 4, 53syl 18 . . 3 ((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) → ((⌊‘(1 / 𝐵)) + 1) ∈ ℕ)
7 irrapxlem4 38070 . . 3 ((𝐴 ∈ ℝ+ ∧ ((⌊‘(1 / 𝐵)) + 1) ∈ ℕ) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)))
86, 7syldan 585 . 2 ((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)))
9 simplrr 796 . . . . . . 7 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑏 ∈ ℕ)
10 nnq 12005 . . . . . . 7 (𝑏 ∈ ℕ → 𝑏 ∈ ℚ)
119, 10syl 17 . . . . . 6 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑏 ∈ ℚ)
12 simplrl 795 . . . . . . 7 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 ∈ ℕ)
13 nnq 12005 . . . . . . 7 (𝑎 ∈ ℕ → 𝑎 ∈ ℚ)
1412, 13syl 17 . . . . . 6 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 ∈ ℚ)
1512nnne0d 11324 . . . . . 6 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 ≠ 0)
16 qdivcl 12013 . . . . . 6 ((𝑏 ∈ ℚ ∧ 𝑎 ∈ ℚ ∧ 𝑎 ≠ 0) → (𝑏 / 𝑎) ∈ ℚ)
1711, 14, 15, 16syl3anc 1490 . . . . 5 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑏 / 𝑎) ∈ ℚ)
189nnrpd 12071 . . . . . . 7 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑏 ∈ ℝ+)
1912nnrpd 12071 . . . . . . 7 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 ∈ ℝ+)
2018, 19rpdivcld 12090 . . . . . 6 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑏 / 𝑎) ∈ ℝ+)
2120rpgt0d 12076 . . . . 5 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 0 < (𝑏 / 𝑎))
2212nnred 11293 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 ∈ ℝ)
2312nnnn0d 11600 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 ∈ ℕ0)
2423nn0ge0d 11603 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 0 ≤ 𝑎)
2522, 24absidd 14449 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘𝑎) = 𝑎)
2625eqcomd 2771 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 = (abs‘𝑎))
2726oveq1d 6859 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) = ((abs‘𝑎) · (abs‘((𝑏 / 𝑎) − 𝐴))))
2812nncnd 11294 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 ∈ ℂ)
29 qre 11997 . . . . . . . . . . . . 13 ((𝑏 / 𝑎) ∈ ℚ → (𝑏 / 𝑎) ∈ ℝ)
3017, 29syl 17 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑏 / 𝑎) ∈ ℝ)
31 rpre 12039 . . . . . . . . . . . . 13 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
3231ad3antrrr 721 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝐴 ∈ ℝ)
3330, 32resubcld 10714 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((𝑏 / 𝑎) − 𝐴) ∈ ℝ)
3433recnd 10324 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((𝑏 / 𝑎) − 𝐴) ∈ ℂ)
3528, 34absmuld 14481 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘(𝑎 · ((𝑏 / 𝑎) − 𝐴))) = ((abs‘𝑎) · (abs‘((𝑏 / 𝑎) − 𝐴))))
3627, 35eqtr4d 2802 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) = (abs‘(𝑎 · ((𝑏 / 𝑎) − 𝐴))))
37 qcn 12006 . . . . . . . . . . . 12 ((𝑏 / 𝑎) ∈ ℚ → (𝑏 / 𝑎) ∈ ℂ)
3817, 37syl 17 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑏 / 𝑎) ∈ ℂ)
39 rpcn 12043 . . . . . . . . . . . 12 (𝐴 ∈ ℝ+𝐴 ∈ ℂ)
4039ad3antrrr 721 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝐴 ∈ ℂ)
4128, 38, 40subdid 10742 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · ((𝑏 / 𝑎) − 𝐴)) = ((𝑎 · (𝑏 / 𝑎)) − (𝑎 · 𝐴)))
429nncnd 11294 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑏 ∈ ℂ)
4342, 28, 15divcan2d 11059 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · (𝑏 / 𝑎)) = 𝑏)
4428, 40mulcomd 10317 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · 𝐴) = (𝐴 · 𝑎))
4543, 44oveq12d 6862 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((𝑎 · (𝑏 / 𝑎)) − (𝑎 · 𝐴)) = (𝑏 − (𝐴 · 𝑎)))
4641, 45eqtrd 2799 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · ((𝑏 / 𝑎) − 𝐴)) = (𝑏 − (𝐴 · 𝑎)))
4746fveq2d 6381 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘(𝑎 · ((𝑏 / 𝑎) − 𝐴))) = (abs‘(𝑏 − (𝐴 · 𝑎))))
4832, 22remulcld 10326 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝐴 · 𝑎) ∈ ℝ)
4948recnd 10324 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝐴 · 𝑎) ∈ ℂ)
5042, 49abssubd 14480 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘(𝑏 − (𝐴 · 𝑎))) = (abs‘((𝐴 · 𝑎) − 𝑏)))
5136, 47, 503eqtrd 2803 . . . . . . 7 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) = (abs‘((𝐴 · 𝑎) − 𝑏)))
529nnred 11293 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑏 ∈ ℝ)
5348, 52resubcld 10714 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((𝐴 · 𝑎) − 𝑏) ∈ ℝ)
5453recnd 10324 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((𝐴 · 𝑎) − 𝑏) ∈ ℂ)
5554abscld 14463 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝐴 · 𝑎) − 𝑏)) ∈ ℝ)
56 simpllr 793 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝐵 ∈ ℝ+)
5756rprecred 12084 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / 𝐵) ∈ ℝ)
5856rpreccld 12083 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / 𝐵) ∈ ℝ+)
5958rpge0d 12077 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 0 ≤ (1 / 𝐵))
6057, 59, 4syl2anc 579 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (⌊‘(1 / 𝐵)) ∈ ℕ0)
6160, 5syl 17 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((⌊‘(1 / 𝐵)) + 1) ∈ ℕ)
6261nnrpd 12071 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((⌊‘(1 / 𝐵)) + 1) ∈ ℝ+)
6362, 19ifcld 4290 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎) ∈ ℝ+)
6463rprecred 12084 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) ∈ ℝ)
6556rpred 12073 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝐵 ∈ ℝ)
6622, 65remulcld 10326 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · 𝐵) ∈ ℝ)
67 simpr 477 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)))
6858rprecred 12084 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / (1 / 𝐵)) ∈ ℝ)
6961nnred 11293 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((⌊‘(1 / 𝐵)) + 1) ∈ ℝ)
7069, 22ifcld 4290 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎) ∈ ℝ)
71 fllep1 12813 . . . . . . . . . . . 12 ((1 / 𝐵) ∈ ℝ → (1 / 𝐵) ≤ ((⌊‘(1 / 𝐵)) + 1))
7257, 71syl 17 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / 𝐵) ≤ ((⌊‘(1 / 𝐵)) + 1))
73 max2 12223 . . . . . . . . . . . 12 ((𝑎 ∈ ℝ ∧ ((⌊‘(1 / 𝐵)) + 1) ∈ ℝ) → ((⌊‘(1 / 𝐵)) + 1) ≤ if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))
7422, 69, 73syl2anc 579 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((⌊‘(1 / 𝐵)) + 1) ≤ if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))
7557, 69, 70, 72, 74letrd 10450 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / 𝐵) ≤ if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))
7658, 63lerecd 12092 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((1 / 𝐵) ≤ if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎) ↔ (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) ≤ (1 / (1 / 𝐵))))
7775, 76mpbid 223 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) ≤ (1 / (1 / 𝐵)))
7865recnd 10324 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝐵 ∈ ℂ)
7956rpne0d 12078 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝐵 ≠ 0)
8078, 79recrecd 11054 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / (1 / 𝐵)) = 𝐵)
8178mulid2d 10314 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 · 𝐵) = 𝐵)
8280, 81eqtr4d 2802 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / (1 / 𝐵)) = (1 · 𝐵))
8312nnge1d 11322 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 1 ≤ 𝑎)
84 1red 10296 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 1 ∈ ℝ)
8584, 22, 56lemul1d 12116 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 ≤ 𝑎 ↔ (1 · 𝐵) ≤ (𝑎 · 𝐵)))
8683, 85mpbid 223 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 · 𝐵) ≤ (𝑎 · 𝐵))
8782, 86eqbrtrd 4833 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / (1 / 𝐵)) ≤ (𝑎 · 𝐵))
8864, 68, 66, 77, 87letrd 10450 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) ≤ (𝑎 · 𝐵))
8955, 64, 66, 67, 88ltletrd 10453 . . . . . . 7 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝐴 · 𝑎) − 𝑏)) < (𝑎 · 𝐵))
9051, 89eqbrtrd 4833 . . . . . 6 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) < (𝑎 · 𝐵))
9134abscld 14463 . . . . . . 7 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝑏 / 𝑎) − 𝐴)) ∈ ℝ)
9212nngt0d 11323 . . . . . . 7 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 0 < 𝑎)
93 ltmul2 11130 . . . . . . 7 (((abs‘((𝑏 / 𝑎) − 𝐴)) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑎 ∈ ℝ ∧ 0 < 𝑎)) → ((abs‘((𝑏 / 𝑎) − 𝐴)) < 𝐵 ↔ (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) < (𝑎 · 𝐵)))
9491, 65, 22, 92, 93syl112anc 1493 . . . . . 6 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((abs‘((𝑏 / 𝑎) − 𝐴)) < 𝐵 ↔ (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) < (𝑎 · 𝐵)))
9590, 94mpbird 248 . . . . 5 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝑏 / 𝑎) − 𝐴)) < 𝐵)
9622, 22remulcld 10326 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · 𝑎) ∈ ℝ)
9722, 15msqgt0d 10851 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 0 < (𝑎 · 𝑎))
9897gt0ne0d 10848 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · 𝑎) ≠ 0)
9996, 98rereccld 11108 . . . . . . 7 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / (𝑎 · 𝑎)) ∈ ℝ)
100 qdencl 15731 . . . . . . . . . . 11 ((𝑏 / 𝑎) ∈ ℚ → (denom‘(𝑏 / 𝑎)) ∈ ℕ)
10117, 100syl 17 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (denom‘(𝑏 / 𝑎)) ∈ ℕ)
102101nnred 11293 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (denom‘(𝑏 / 𝑎)) ∈ ℝ)
103102, 102remulcld 10326 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))) ∈ ℝ)
104101nnne0d 11324 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (denom‘(𝑏 / 𝑎)) ≠ 0)
105102, 104msqgt0d 10851 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 0 < ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))))
106105gt0ne0d 10848 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))) ≠ 0)
107103, 106rereccld 11108 . . . . . . 7 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎)))) ∈ ℝ)
10822, 15rereccld 11108 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / 𝑎) ∈ ℝ)
109 max1 12221 . . . . . . . . . . . 12 ((𝑎 ∈ ℝ ∧ ((⌊‘(1 / 𝐵)) + 1) ∈ ℝ) → 𝑎 ≤ if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))
11022, 69, 109syl2anc 579 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑎 ≤ if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))
11119, 63lerecd 12092 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 ≤ if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎) ↔ (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) ≤ (1 / 𝑎)))
112110, 111mpbid 223 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) ≤ (1 / 𝑎))
11355, 64, 108, 67, 112ltletrd 10453 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / 𝑎))
11428, 28, 28, 15, 15divdiv1d 11088 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((𝑎 / 𝑎) / 𝑎) = (𝑎 / (𝑎 · 𝑎)))
11528, 15dividd 11055 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 / 𝑎) = 1)
116115oveq1d 6859 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((𝑎 / 𝑎) / 𝑎) = (1 / 𝑎))
11796recnd 10324 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · 𝑎) ∈ ℂ)
11828, 117, 98divrecd 11060 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 / (𝑎 · 𝑎)) = (𝑎 · (1 / (𝑎 · 𝑎))))
119114, 116, 1183eqtr3rd 2808 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · (1 / (𝑎 · 𝑎))) = (1 / 𝑎))
120113, 51, 1193brtr4d 4843 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) < (𝑎 · (1 / (𝑎 · 𝑎))))
121 ltmul2 11130 . . . . . . . . 9 (((abs‘((𝑏 / 𝑎) − 𝐴)) ∈ ℝ ∧ (1 / (𝑎 · 𝑎)) ∈ ℝ ∧ (𝑎 ∈ ℝ ∧ 0 < 𝑎)) → ((abs‘((𝑏 / 𝑎) − 𝐴)) < (1 / (𝑎 · 𝑎)) ↔ (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) < (𝑎 · (1 / (𝑎 · 𝑎)))))
12291, 99, 22, 92, 121syl112anc 1493 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((abs‘((𝑏 / 𝑎) − 𝐴)) < (1 / (𝑎 · 𝑎)) ↔ (𝑎 · (abs‘((𝑏 / 𝑎) − 𝐴))) < (𝑎 · (1 / (𝑎 · 𝑎)))))
123120, 122mpbird 248 . . . . . . 7 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝑏 / 𝑎) − 𝐴)) < (1 / (𝑎 · 𝑎)))
1249nnzd 11731 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 𝑏 ∈ ℤ)
125 divdenle 15739 . . . . . . . . . 10 ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℕ) → (denom‘(𝑏 / 𝑎)) ≤ 𝑎)
126124, 12, 125syl2anc 579 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (denom‘(𝑏 / 𝑎)) ≤ 𝑎)
127101nnnn0d 11600 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (denom‘(𝑏 / 𝑎)) ∈ ℕ0)
128127nn0ge0d 11603 . . . . . . . . . 10 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → 0 ≤ (denom‘(𝑏 / 𝑎)))
129 le2msq 11179 . . . . . . . . . 10 ((((denom‘(𝑏 / 𝑎)) ∈ ℝ ∧ 0 ≤ (denom‘(𝑏 / 𝑎))) ∧ (𝑎 ∈ ℝ ∧ 0 ≤ 𝑎)) → ((denom‘(𝑏 / 𝑎)) ≤ 𝑎 ↔ ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))) ≤ (𝑎 · 𝑎)))
130102, 128, 22, 24, 129syl22anc 867 . . . . . . . . 9 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((denom‘(𝑏 / 𝑎)) ≤ 𝑎 ↔ ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))) ≤ (𝑎 · 𝑎)))
131126, 130mpbid 223 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))) ≤ (𝑎 · 𝑎))
132 lerec 11162 . . . . . . . . 9 (((((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))) ∈ ℝ ∧ 0 < ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎)))) ∧ ((𝑎 · 𝑎) ∈ ℝ ∧ 0 < (𝑎 · 𝑎))) → (((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))) ≤ (𝑎 · 𝑎) ↔ (1 / (𝑎 · 𝑎)) ≤ (1 / ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))))))
133103, 105, 96, 97, 132syl22anc 867 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))) ≤ (𝑎 · 𝑎) ↔ (1 / (𝑎 · 𝑎)) ≤ (1 / ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))))))
134131, 133mpbid 223 . . . . . . 7 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / (𝑎 · 𝑎)) ≤ (1 / ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎)))))
13591, 99, 107, 123, 134ltletrd 10453 . . . . . 6 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝑏 / 𝑎) − 𝐴)) < (1 / ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎)))))
136101nncnd 11294 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (denom‘(𝑏 / 𝑎)) ∈ ℂ)
137 2nn0 11559 . . . . . . . 8 2 ∈ ℕ0
138 expneg 13078 . . . . . . . 8 (((denom‘(𝑏 / 𝑎)) ∈ ℂ ∧ 2 ∈ ℕ0) → ((denom‘(𝑏 / 𝑎))↑-2) = (1 / ((denom‘(𝑏 / 𝑎))↑2)))
139136, 137, 138sylancl 580 . . . . . . 7 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((denom‘(𝑏 / 𝑎))↑-2) = (1 / ((denom‘(𝑏 / 𝑎))↑2)))
140136sqvald 13215 . . . . . . . 8 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((denom‘(𝑏 / 𝑎))↑2) = ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎))))
141140oveq2d 6860 . . . . . . 7 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (1 / ((denom‘(𝑏 / 𝑎))↑2)) = (1 / ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎)))))
142139, 141eqtrd 2799 . . . . . 6 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ((denom‘(𝑏 / 𝑎))↑-2) = (1 / ((denom‘(𝑏 / 𝑎)) · (denom‘(𝑏 / 𝑎)))))
143135, 142breqtrrd 4839 . . . . 5 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → (abs‘((𝑏 / 𝑎) − 𝐴)) < ((denom‘(𝑏 / 𝑎))↑-2))
144 breq2 4815 . . . . . . 7 (𝑥 = (𝑏 / 𝑎) → (0 < 𝑥 ↔ 0 < (𝑏 / 𝑎)))
145 fvoveq1 6867 . . . . . . . 8 (𝑥 = (𝑏 / 𝑎) → (abs‘(𝑥𝐴)) = (abs‘((𝑏 / 𝑎) − 𝐴)))
146145breq1d 4821 . . . . . . 7 (𝑥 = (𝑏 / 𝑎) → ((abs‘(𝑥𝐴)) < 𝐵 ↔ (abs‘((𝑏 / 𝑎) − 𝐴)) < 𝐵))
147 fveq2 6377 . . . . . . . . 9 (𝑥 = (𝑏 / 𝑎) → (denom‘𝑥) = (denom‘(𝑏 / 𝑎)))
148147oveq1d 6859 . . . . . . . 8 (𝑥 = (𝑏 / 𝑎) → ((denom‘𝑥)↑-2) = ((denom‘(𝑏 / 𝑎))↑-2))
149145, 148breq12d 4824 . . . . . . 7 (𝑥 = (𝑏 / 𝑎) → ((abs‘(𝑥𝐴)) < ((denom‘𝑥)↑-2) ↔ (abs‘((𝑏 / 𝑎) − 𝐴)) < ((denom‘(𝑏 / 𝑎))↑-2)))
150144, 146, 1493anbi123d 1560 . . . . . 6 (𝑥 = (𝑏 / 𝑎) → ((0 < 𝑥 ∧ (abs‘(𝑥𝐴)) < 𝐵 ∧ (abs‘(𝑥𝐴)) < ((denom‘𝑥)↑-2)) ↔ (0 < (𝑏 / 𝑎) ∧ (abs‘((𝑏 / 𝑎) − 𝐴)) < 𝐵 ∧ (abs‘((𝑏 / 𝑎) − 𝐴)) < ((denom‘(𝑏 / 𝑎))↑-2))))
151150rspcev 3462 . . . . 5 (((𝑏 / 𝑎) ∈ ℚ ∧ (0 < (𝑏 / 𝑎) ∧ (abs‘((𝑏 / 𝑎) − 𝐴)) < 𝐵 ∧ (abs‘((𝑏 / 𝑎) − 𝐴)) < ((denom‘(𝑏 / 𝑎))↑-2))) → ∃𝑥 ∈ ℚ (0 < 𝑥 ∧ (abs‘(𝑥𝐴)) < 𝐵 ∧ (abs‘(𝑥𝐴)) < ((denom‘𝑥)↑-2)))
15217, 21, 95, 143, 151syl13anc 1491 . . . 4 ((((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎))) → ∃𝑥 ∈ ℚ (0 < 𝑥 ∧ (abs‘(𝑥𝐴)) < 𝐵 ∧ (abs‘(𝑥𝐴)) < ((denom‘𝑥)↑-2)))
153152ex 401 . . 3 (((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) ∧ (𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ)) → ((abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) → ∃𝑥 ∈ ℚ (0 < 𝑥 ∧ (abs‘(𝑥𝐴)) < 𝐵 ∧ (abs‘(𝑥𝐴)) < ((denom‘𝑥)↑-2))))
154153rexlimdvva 3185 . 2 ((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) → (∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎 ≤ ((⌊‘(1 / 𝐵)) + 1), ((⌊‘(1 / 𝐵)) + 1), 𝑎)) → ∃𝑥 ∈ ℚ (0 < 𝑥 ∧ (abs‘(𝑥𝐴)) < 𝐵 ∧ (abs‘(𝑥𝐴)) < ((denom‘𝑥)↑-2))))
1558, 154mpd 15 1 ((𝐴 ∈ ℝ+𝐵 ∈ ℝ+) → ∃𝑥 ∈ ℚ (0 < 𝑥 ∧ (abs‘(𝑥𝐴)) < 𝐵 ∧ (abs‘(𝑥𝐴)) < ((denom‘𝑥)↑-2)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wrex 3056  ifcif 4245   class class class wbr 4811  cfv 6070  (class class class)co 6844  cc 10189  cr 10190  0cc0 10191  1c1 10192   + caddc 10194   · cmul 10196   < clt 10330  cle 10331  cmin 10522  -cneg 10523   / cdiv 10940  cn 11276  2c2 11329  0cn0 11540  cz 11626  cq 11992  +crp 12031  cfl 12802  cexp 13070  abscabs 14262  denomcdenom 15724
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-cnex 10247  ax-resscn 10248  ax-1cn 10249  ax-icn 10250  ax-addcl 10251  ax-addrcl 10252  ax-mulcl 10253  ax-mulrcl 10254  ax-mulcom 10255  ax-addass 10256  ax-mulass 10257  ax-distr 10258  ax-i2m1 10259  ax-1ne0 10260  ax-1rid 10261  ax-rnegex 10262  ax-rrecex 10263  ax-cnre 10264  ax-pre-lttri 10265  ax-pre-lttrn 10266  ax-pre-ltadd 10267  ax-pre-mulgt0 10268  ax-pre-sup 10269
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6805  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-om 7266  df-1st 7368  df-2nd 7369  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-1o 7766  df-oadd 7770  df-er 7949  df-en 8163  df-dom 8164  df-sdom 8165  df-fin 8166  df-sup 8557  df-inf 8558  df-card 9018  df-pnf 10332  df-mnf 10333  df-xr 10334  df-ltxr 10335  df-le 10336  df-sub 10524  df-neg 10525  df-div 10941  df-nn 11277  df-2 11337  df-3 11338  df-n0 11541  df-xnn0 11613  df-z 11627  df-uz 11890  df-q 11993  df-rp 12032  df-ico 12386  df-fz 12537  df-fl 12804  df-mod 12880  df-seq 13012  df-exp 13071  df-hash 13325  df-cj 14127  df-re 14128  df-im 14129  df-sqrt 14263  df-abs 14264  df-dvds 15269  df-gcd 15501  df-numer 15725  df-denom 15726
This theorem is referenced by:  irrapxlem6  38072
  Copyright terms: Public domain W3C validator