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

Theorem irrapxlem4 38067
Description: Lemma for irrapx1 38070. Eliminate ranges, use positivity of the input to force positivity of the output by increasing 𝐵 as needed. (Contributed by Stefan O'Rear, 13-Sep-2014.)
Assertion
Ref Expression
irrapxlem4 ((𝐴 ∈ ℝ+𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ (abs‘((𝐴 · 𝑥) − 𝑦)) < (1 / if(𝑥𝐵, 𝐵, 𝑥)))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Proof of Theorem irrapxlem4
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfznn 12577 . . . 4 (𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵)) → 𝑎 ∈ ℕ)
21ad3antlr 722 . . 3 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 𝑎 ∈ ℕ)
3 nn0z 11647 . . . . 5 (𝑏 ∈ ℕ0𝑏 ∈ ℤ)
43ad2antlr 718 . . . 4 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 𝑏 ∈ ℤ)
5 simpl 474 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ+𝐵 ∈ ℕ) → 𝐴 ∈ ℝ+)
65ad3antrrr 721 . . . . . . . . . . . . 13 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 𝐴 ∈ ℝ+)
76rpred 12070 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 𝐴 ∈ ℝ)
82nnred 11291 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 𝑎 ∈ ℝ)
97, 8remulcld 10324 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (𝐴 · 𝑎) ∈ ℝ)
10 nn0re 11548 . . . . . . . . . . . 12 (𝑏 ∈ ℕ0𝑏 ∈ ℝ)
1110ad2antlr 718 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 𝑏 ∈ ℝ)
129, 11resubcld 10712 . . . . . . . . . 10 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → ((𝐴 · 𝑎) − 𝑏) ∈ ℝ)
1312recnd 10322 . . . . . . . . 9 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → ((𝐴 · 𝑎) − 𝑏) ∈ ℂ)
1413abscld 14460 . . . . . . . 8 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (abs‘((𝐴 · 𝑎) − 𝑏)) ∈ ℝ)
155rpreccld 12080 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ+𝐵 ∈ ℕ) → (1 / 𝐴) ∈ ℝ+)
1615rprege0d 12077 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ+𝐵 ∈ ℕ) → ((1 / 𝐴) ∈ ℝ ∧ 0 ≤ (1 / 𝐴)))
17 flge0nn0 12829 . . . . . . . . . . . 12 (((1 / 𝐴) ∈ ℝ ∧ 0 ≤ (1 / 𝐴)) → (⌊‘(1 / 𝐴)) ∈ ℕ0)
18 nn0p1nn 11579 . . . . . . . . . . . 12 ((⌊‘(1 / 𝐴)) ∈ ℕ0 → ((⌊‘(1 / 𝐴)) + 1) ∈ ℕ)
1916, 17, 183syl 18 . . . . . . . . . . 11 ((𝐴 ∈ ℝ+𝐵 ∈ ℕ) → ((⌊‘(1 / 𝐴)) + 1) ∈ ℕ)
2019ad3antrrr 721 . . . . . . . . . 10 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → ((⌊‘(1 / 𝐴)) + 1) ∈ ℕ)
21 simpr 477 . . . . . . . . . . 11 ((𝐴 ∈ ℝ+𝐵 ∈ ℕ) → 𝐵 ∈ ℕ)
2221ad3antrrr 721 . . . . . . . . . 10 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 𝐵 ∈ ℕ)
2320, 22ifcld 4288 . . . . . . . . 9 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵) ∈ ℕ)
2423nnrecred 11323 . . . . . . . 8 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵)) ∈ ℝ)
25 0red 10297 . . . . . . . . 9 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 0 ∈ ℝ)
269, 25resubcld 10712 . . . . . . . 8 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → ((𝐴 · 𝑎) − 0) ∈ ℝ)
27 simpr 477 . . . . . . . 8 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵)))
2820nnrecred 11323 . . . . . . . . . 10 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (1 / ((⌊‘(1 / 𝐴)) + 1)) ∈ ℝ)
2922nnred 11291 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 𝐵 ∈ ℝ)
306rprecred 12081 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (1 / 𝐴) ∈ ℝ)
3130flcld 12807 . . . . . . . . . . . . . 14 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (⌊‘(1 / 𝐴)) ∈ ℤ)
3231zred 11729 . . . . . . . . . . . . 13 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (⌊‘(1 / 𝐴)) ∈ ℝ)
33 peano2re 10463 . . . . . . . . . . . . 13 ((⌊‘(1 / 𝐴)) ∈ ℝ → ((⌊‘(1 / 𝐴)) + 1) ∈ ℝ)
3432, 33syl 17 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → ((⌊‘(1 / 𝐴)) + 1) ∈ ℝ)
35 max2 12220 . . . . . . . . . . . 12 ((𝐵 ∈ ℝ ∧ ((⌊‘(1 / 𝐴)) + 1) ∈ ℝ) → ((⌊‘(1 / 𝐴)) + 1) ≤ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))
3629, 34, 35syl2anc 579 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → ((⌊‘(1 / 𝐴)) + 1) ≤ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))
3720nngt0d 11321 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 0 < ((⌊‘(1 / 𝐴)) + 1))
3823nnred 11291 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵) ∈ ℝ)
3923nngt0d 11321 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 0 < if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))
40 lerec 11160 . . . . . . . . . . . 12 (((((⌊‘(1 / 𝐴)) + 1) ∈ ℝ ∧ 0 < ((⌊‘(1 / 𝐴)) + 1)) ∧ (if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵) ∈ ℝ ∧ 0 < if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (((⌊‘(1 / 𝐴)) + 1) ≤ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵) ↔ (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵)) ≤ (1 / ((⌊‘(1 / 𝐴)) + 1))))
4134, 37, 38, 39, 40syl22anc 867 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (((⌊‘(1 / 𝐴)) + 1) ≤ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵) ↔ (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵)) ≤ (1 / ((⌊‘(1 / 𝐴)) + 1))))
4236, 41mpbid 223 . . . . . . . . . 10 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵)) ≤ (1 / ((⌊‘(1 / 𝐴)) + 1)))
43 fllep1 12810 . . . . . . . . . . . . 13 ((1 / 𝐴) ∈ ℝ → (1 / 𝐴) ≤ ((⌊‘(1 / 𝐴)) + 1))
4430, 43syl 17 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (1 / 𝐴) ≤ ((⌊‘(1 / 𝐴)) + 1))
4520nncnd 11292 . . . . . . . . . . . . 13 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → ((⌊‘(1 / 𝐴)) + 1) ∈ ℂ)
4620nnne0d 11322 . . . . . . . . . . . . 13 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → ((⌊‘(1 / 𝐴)) + 1) ≠ 0)
4745, 46recrecd 11052 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (1 / (1 / ((⌊‘(1 / 𝐴)) + 1))) = ((⌊‘(1 / 𝐴)) + 1))
4844, 47breqtrrd 4837 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (1 / 𝐴) ≤ (1 / (1 / ((⌊‘(1 / 𝐴)) + 1))))
4934, 37recgt0d 11212 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 0 < (1 / ((⌊‘(1 / 𝐴)) + 1)))
506rpgt0d 12073 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 0 < 𝐴)
51 lerec 11160 . . . . . . . . . . . 12 ((((1 / ((⌊‘(1 / 𝐴)) + 1)) ∈ ℝ ∧ 0 < (1 / ((⌊‘(1 / 𝐴)) + 1))) ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → ((1 / ((⌊‘(1 / 𝐴)) + 1)) ≤ 𝐴 ↔ (1 / 𝐴) ≤ (1 / (1 / ((⌊‘(1 / 𝐴)) + 1)))))
5228, 49, 7, 50, 51syl22anc 867 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → ((1 / ((⌊‘(1 / 𝐴)) + 1)) ≤ 𝐴 ↔ (1 / 𝐴) ≤ (1 / (1 / ((⌊‘(1 / 𝐴)) + 1)))))
5348, 52mpbird 248 . . . . . . . . . 10 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (1 / ((⌊‘(1 / 𝐴)) + 1)) ≤ 𝐴)
5424, 28, 7, 42, 53letrd 10448 . . . . . . . . 9 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵)) ≤ 𝐴)
557recnd 10322 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 𝐴 ∈ ℂ)
5655mulid1d 10311 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (𝐴 · 1) = 𝐴)
572nnge1d 11320 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 1 ≤ 𝑎)
58 1red 10294 . . . . . . . . . . . . 13 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 1 ∈ ℝ)
5958, 8, 6lemul2d 12114 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (1 ≤ 𝑎 ↔ (𝐴 · 1) ≤ (𝐴 · 𝑎)))
6057, 59mpbid 223 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (𝐴 · 1) ≤ (𝐴 · 𝑎))
6156, 60eqbrtrrd 4833 . . . . . . . . . 10 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 𝐴 ≤ (𝐴 · 𝑎))
629recnd 10322 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (𝐴 · 𝑎) ∈ ℂ)
6362subid1d 10635 . . . . . . . . . 10 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → ((𝐴 · 𝑎) − 0) = (𝐴 · 𝑎))
6461, 63breqtrrd 4837 . . . . . . . . 9 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 𝐴 ≤ ((𝐴 · 𝑎) − 0))
6524, 7, 26, 54, 64letrd 10448 . . . . . . . 8 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵)) ≤ ((𝐴 · 𝑎) − 0))
6614, 24, 26, 27, 65ltletrd 10451 . . . . . . 7 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (abs‘((𝐴 · 𝑎) − 𝑏)) < ((𝐴 · 𝑎) − 0))
6712, 26absltd 14453 . . . . . . 7 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → ((abs‘((𝐴 · 𝑎) − 𝑏)) < ((𝐴 · 𝑎) − 0) ↔ (-((𝐴 · 𝑎) − 0) < ((𝐴 · 𝑎) − 𝑏) ∧ ((𝐴 · 𝑎) − 𝑏) < ((𝐴 · 𝑎) − 0))))
6866, 67mpbid 223 . . . . . 6 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (-((𝐴 · 𝑎) − 0) < ((𝐴 · 𝑎) − 𝑏) ∧ ((𝐴 · 𝑎) − 𝑏) < ((𝐴 · 𝑎) − 0)))
6968simprd 489 . . . . 5 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → ((𝐴 · 𝑎) − 𝑏) < ((𝐴 · 𝑎) − 0))
7025, 11, 9ltsub2d 10891 . . . . 5 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (0 < 𝑏 ↔ ((𝐴 · 𝑎) − 𝑏) < ((𝐴 · 𝑎) − 0)))
7169, 70mpbird 248 . . . 4 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 0 < 𝑏)
72 elnnz 11634 . . . 4 (𝑏 ∈ ℕ ↔ (𝑏 ∈ ℤ ∧ 0 < 𝑏))
734, 71, 72sylanbrc 578 . . 3 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 𝑏 ∈ ℕ)
7422, 2ifcld 4288 . . . . 5 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → if(𝑎𝐵, 𝐵, 𝑎) ∈ ℕ)
7574nnrecred 11323 . . . 4 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (1 / if(𝑎𝐵, 𝐵, 𝑎)) ∈ ℝ)
76 elfzle2 12552 . . . . . . 7 (𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵)) → 𝑎 ≤ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))
7776ad3antlr 722 . . . . . 6 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 𝑎 ≤ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))
78 max1 12218 . . . . . . 7 ((𝐵 ∈ ℝ ∧ ((⌊‘(1 / 𝐴)) + 1) ∈ ℝ) → 𝐵 ≤ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))
7929, 34, 78syl2anc 579 . . . . . 6 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 𝐵 ≤ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))
80 maxle 12224 . . . . . . 7 ((𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵) ∈ ℝ) → (if(𝑎𝐵, 𝐵, 𝑎) ≤ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵) ↔ (𝑎 ≤ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵) ∧ 𝐵 ≤ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))))
818, 29, 38, 80syl3anc 1490 . . . . . 6 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (if(𝑎𝐵, 𝐵, 𝑎) ≤ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵) ↔ (𝑎 ≤ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵) ∧ 𝐵 ≤ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))))
8277, 79, 81mpbir2and 704 . . . . 5 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → if(𝑎𝐵, 𝐵, 𝑎) ≤ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))
8329, 8ifcld 4288 . . . . . 6 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → if(𝑎𝐵, 𝐵, 𝑎) ∈ ℝ)
8422nngt0d 11321 . . . . . . 7 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 0 < 𝐵)
85 max2 12220 . . . . . . . 8 ((𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ if(𝑎𝐵, 𝐵, 𝑎))
868, 29, 85syl2anc 579 . . . . . . 7 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 𝐵 ≤ if(𝑎𝐵, 𝐵, 𝑎))
8725, 29, 83, 84, 86ltletrd 10451 . . . . . 6 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → 0 < if(𝑎𝐵, 𝐵, 𝑎))
88 lerec 11160 . . . . . 6 (((if(𝑎𝐵, 𝐵, 𝑎) ∈ ℝ ∧ 0 < if(𝑎𝐵, 𝐵, 𝑎)) ∧ (if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵) ∈ ℝ ∧ 0 < if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (if(𝑎𝐵, 𝐵, 𝑎) ≤ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵) ↔ (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵)) ≤ (1 / if(𝑎𝐵, 𝐵, 𝑎))))
8983, 87, 38, 39, 88syl22anc 867 . . . . 5 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (if(𝑎𝐵, 𝐵, 𝑎) ≤ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵) ↔ (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵)) ≤ (1 / if(𝑎𝐵, 𝐵, 𝑎))))
9082, 89mpbid 223 . . . 4 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵)) ≤ (1 / if(𝑎𝐵, 𝐵, 𝑎)))
9114, 24, 75, 27, 90ltletrd 10451 . . 3 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎𝐵, 𝐵, 𝑎)))
92 oveq2 6850 . . . . . 6 (𝑥 = 𝑎 → (𝐴 · 𝑥) = (𝐴 · 𝑎))
9392fvoveq1d 6864 . . . . 5 (𝑥 = 𝑎 → (abs‘((𝐴 · 𝑥) − 𝑦)) = (abs‘((𝐴 · 𝑎) − 𝑦)))
94 breq1 4812 . . . . . . 7 (𝑥 = 𝑎 → (𝑥𝐵𝑎𝐵))
95 id 22 . . . . . . 7 (𝑥 = 𝑎𝑥 = 𝑎)
9694, 95ifbieq2d 4268 . . . . . 6 (𝑥 = 𝑎 → if(𝑥𝐵, 𝐵, 𝑥) = if(𝑎𝐵, 𝐵, 𝑎))
9796oveq2d 6858 . . . . 5 (𝑥 = 𝑎 → (1 / if(𝑥𝐵, 𝐵, 𝑥)) = (1 / if(𝑎𝐵, 𝐵, 𝑎)))
9893, 97breq12d 4822 . . . 4 (𝑥 = 𝑎 → ((abs‘((𝐴 · 𝑥) − 𝑦)) < (1 / if(𝑥𝐵, 𝐵, 𝑥)) ↔ (abs‘((𝐴 · 𝑎) − 𝑦)) < (1 / if(𝑎𝐵, 𝐵, 𝑎))))
99 oveq2 6850 . . . . . 6 (𝑦 = 𝑏 → ((𝐴 · 𝑎) − 𝑦) = ((𝐴 · 𝑎) − 𝑏))
10099fveq2d 6379 . . . . 5 (𝑦 = 𝑏 → (abs‘((𝐴 · 𝑎) − 𝑦)) = (abs‘((𝐴 · 𝑎) − 𝑏)))
101100breq1d 4819 . . . 4 (𝑦 = 𝑏 → ((abs‘((𝐴 · 𝑎) − 𝑦)) < (1 / if(𝑎𝐵, 𝐵, 𝑎)) ↔ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎𝐵, 𝐵, 𝑎))))
10298, 101rspc2ev 3476 . . 3 ((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝑎𝐵, 𝐵, 𝑎))) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ (abs‘((𝐴 · 𝑥) − 𝑦)) < (1 / if(𝑥𝐵, 𝐵, 𝑥)))
1032, 73, 91, 102syl3anc 1490 . 2 (((((𝐴 ∈ ℝ+𝐵 ∈ ℕ) ∧ 𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) ∧ 𝑏 ∈ ℕ0) ∧ (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ (abs‘((𝐴 · 𝑥) − 𝑦)) < (1 / if(𝑥𝐵, 𝐵, 𝑥)))
10419, 21ifcld 4288 . . 3 ((𝐴 ∈ ℝ+𝐵 ∈ ℕ) → if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵) ∈ ℕ)
105 irrapxlem3 38066 . . 3 ((𝐴 ∈ ℝ+ ∧ if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵) ∈ ℕ) → ∃𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))∃𝑏 ∈ ℕ0 (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵)))
1065, 104, 105syl2anc 579 . 2 ((𝐴 ∈ ℝ+𝐵 ∈ ℕ) → ∃𝑎 ∈ (1...if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵))∃𝑏 ∈ ℕ0 (abs‘((𝐴 · 𝑎) − 𝑏)) < (1 / if(𝐵 ≤ ((⌊‘(1 / 𝐴)) + 1), ((⌊‘(1 / 𝐴)) + 1), 𝐵)))
107103, 106r19.29vva 3228 1 ((𝐴 ∈ ℝ+𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ (abs‘((𝐴 · 𝑥) − 𝑦)) < (1 / if(𝑥𝐵, 𝐵, 𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wcel 2155  wrex 3056  ifcif 4243   class class class wbr 4809  cfv 6068  (class class class)co 6842  cr 10188  0cc0 10189  1c1 10190   + caddc 10192   · cmul 10194   < clt 10328  cle 10329  cmin 10520  -cneg 10521   / cdiv 10938  cn 11274  0cn0 11538  cz 11624  +crp 12028  ...cfz 12533  cfl 12799  abscabs 14259
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 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
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 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-sup 8555  df-inf 8556  df-card 9016  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-xnn0 11611  df-z 11625  df-uz 11887  df-rp 12029  df-ico 12383  df-fz 12534  df-fl 12801  df-mod 12877  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261
This theorem is referenced by:  irrapxlem5  38068
  Copyright terms: Public domain W3C validator