Metamath Proof Explorer

Theorem irrapxlem4

Description: Lemma for irrapx1 . Eliminate ranges, use positivity of the input to force positivity of the output by increasing B as needed. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion irrapxlem4 ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( abs ‘ ( ( 𝐴 · 𝑥 ) − 𝑦 ) ) < ( 1 / if ( 𝑥 ≤ 𝐵 , 𝐵 , 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 elfznn ⊢ ( 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) → 𝑎 ∈ ℕ )
2 1 ad3antlr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 𝑎 ∈ ℕ )
3 nn0z ⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℤ )
4 3 ad2antlr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 𝑏 ∈ ℤ )
5 simpl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) → 𝐴 ∈ ℝ+ )
6 5 ad3antrrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 𝐴 ∈ ℝ+ )
7 6 rpred ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 𝐴 ∈ ℝ )
8 2 nnred ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 𝑎 ∈ ℝ )
9 7 8 remulcld ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( 𝐴 · 𝑎 ) ∈ ℝ )
10 nn0re ⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℝ )
11 10 ad2antlr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 𝑏 ∈ ℝ )
12 9 11 resubcld ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( ( 𝐴 · 𝑎 ) − 𝑏 ) ∈ ℝ )
13 12 recnd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( ( 𝐴 · 𝑎 ) − 𝑏 ) ∈ ℂ )
14 13 abscld ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) ∈ ℝ )
15 5 rpreccld ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) → ( 1 / 𝐴 ) ∈ ℝ+ )
16 15 rprege0d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) → ( ( 1 / 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝐴 ) ) )
17 flge0nn0 ⊢ ( ( ( 1 / 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝐴 ) ) → ( ⌊ ‘ ( 1 / 𝐴 ) ) ∈ ℕ0 )
18 nn0p1nn ⊢ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ∈ ℕ )
19 16 17 18 3syl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) → ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ∈ ℕ )
20 19 ad3antrrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ∈ ℕ )
21 simpr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℕ )
22 21 ad3antrrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 𝐵 ∈ ℕ )
23 20 22 ifcld ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ∈ ℕ )
24 23 nnrecred ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ∈ ℝ )
25 0red ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 0 ∈ ℝ )
26 9 25 resubcld ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( ( 𝐴 · 𝑎 ) − 0 ) ∈ ℝ )
27 simpr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) )
28 20 nnrecred ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( 1 / ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ) ∈ ℝ )
29 22 nnred ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 𝐵 ∈ ℝ )
30 6 rprecred ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( 1 / 𝐴 ) ∈ ℝ )
31 30 flcld ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( ⌊ ‘ ( 1 / 𝐴 ) ) ∈ ℤ )
32 31 zred ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( ⌊ ‘ ( 1 / 𝐴 ) ) ∈ ℝ )
33 peano2re ⊢ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) ∈ ℝ → ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ∈ ℝ )
34 32 33 syl ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ∈ ℝ )
35 max2 ⊢ ( ( 𝐵 ∈ ℝ ∧ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ∈ ℝ ) → ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ≤ if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) )
36 29 34 35 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ≤ if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) )
37 20 nngt0d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 0 < ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) )
38 23 nnred ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ∈ ℝ )
39 23 nngt0d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 0 < if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) )
40 lerec ⊢ ( ( ( ( ( ⌊ ‘ ( 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 ) ) ) )
41 34 37 38 39 40 syl22anc ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 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 ) ) ) )
42 36 41 mpbid ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 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 ⊢ ( ( 1 / 𝐴 ) ∈ ℝ → ( 1 / 𝐴 ) ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) )
44 30 43 syl ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( 1 / 𝐴 ) ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) )
45 20 nncnd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ∈ ℂ )
46 20 nnne0d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ≠ 0 )
47 45 46 recrecd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( 1 / ( 1 / ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ) ) = ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) )
48 44 47 breqtrrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( 1 / 𝐴 ) ≤ ( 1 / ( 1 / ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ) ) )
49 34 37 recgt0d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 0 < ( 1 / ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ) )
50 6 rpgt0d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 0 < 𝐴 )
51 lerec ⊢ ( ( ( ( 1 / ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ) ∈ ℝ ∧ 0 < ( 1 / ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ) ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( ( 1 / ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ) ≤ 𝐴 ↔ ( 1 / 𝐴 ) ≤ ( 1 / ( 1 / ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ) ) ) )
52 28 49 7 50 51 syl22anc ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( ( 1 / ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ) ≤ 𝐴 ↔ ( 1 / 𝐴 ) ≤ ( 1 / ( 1 / ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ) ) ) )
53 48 52 mpbird ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( 1 / ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ) ≤ 𝐴 )
54 24 28 7 42 53 letrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ≤ 𝐴 )
55 7 recnd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 𝐴 ∈ ℂ )
56 55 mulid1d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( 𝐴 · 1 ) = 𝐴 )
57 2 nnge1d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 1 ≤ 𝑎 )
58 1red ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 1 ∈ ℝ )
59 58 8 6 lemul2d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( 1 ≤ 𝑎 ↔ ( 𝐴 · 1 ) ≤ ( 𝐴 · 𝑎 ) ) )
60 57 59 mpbid ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( 𝐴 · 1 ) ≤ ( 𝐴 · 𝑎 ) )
61 56 60 eqbrtrrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 𝐴 ≤ ( 𝐴 · 𝑎 ) )
62 9 recnd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( 𝐴 · 𝑎 ) ∈ ℂ )
63 62 subid1d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( ( 𝐴 · 𝑎 ) − 0 ) = ( 𝐴 · 𝑎 ) )
64 61 63 breqtrrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 𝐴 ≤ ( ( 𝐴 · 𝑎 ) − 0 ) )
65 24 7 26 54 64 letrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ≤ ( ( 𝐴 · 𝑎 ) − 0 ) )
66 14 24 26 27 65 ltletrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( ( 𝐴 · 𝑎 ) − 0 ) )
67 12 26 absltd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( ( 𝐴 · 𝑎 ) − 0 ) ↔ ( - ( ( 𝐴 · 𝑎 ) − 0 ) < ( ( 𝐴 · 𝑎 ) − 𝑏 ) ∧ ( ( 𝐴 · 𝑎 ) − 𝑏 ) < ( ( 𝐴 · 𝑎 ) − 0 ) ) ) )
68 66 67 mpbid ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( - ( ( 𝐴 · 𝑎 ) − 0 ) < ( ( 𝐴 · 𝑎 ) − 𝑏 ) ∧ ( ( 𝐴 · 𝑎 ) − 𝑏 ) < ( ( 𝐴 · 𝑎 ) − 0 ) ) )
69 68 simprd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( ( 𝐴 · 𝑎 ) − 𝑏 ) < ( ( 𝐴 · 𝑎 ) − 0 ) )
70 25 11 9 ltsub2d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( 0 < 𝑏 ↔ ( ( 𝐴 · 𝑎 ) − 𝑏 ) < ( ( 𝐴 · 𝑎 ) − 0 ) ) )
71 69 70 mpbird ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 0 < 𝑏 )
72 elnnz ⊢ ( 𝑏 ∈ ℕ ↔ ( 𝑏 ∈ ℤ ∧ 0 < 𝑏 ) )
73 4 71 72 sylanbrc ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 𝑏 ∈ ℕ )
74 22 2 ifcld ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → if ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) ∈ ℕ )
75 74 nnrecred ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( 1 / if ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) ) ∈ ℝ )
76 elfzle2 ⊢ ( 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) → 𝑎 ≤ if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) )
77 76 ad3antlr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 𝑎 ≤ if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) )
78 max1 ⊢ ( ( 𝐵 ∈ ℝ ∧ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ∈ ℝ ) → 𝐵 ≤ if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) )
79 29 34 78 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 𝐵 ≤ if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) )
80 maxle ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ∈ ℝ ) → ( if ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) ≤ if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ↔ ( 𝑎 ≤ if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ∧ 𝐵 ≤ if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) )
81 8 29 38 80 syl3anc ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 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 ) , 𝐵 ) ) ) )
82 77 79 81 mpbir2and ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → if ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) ≤ if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) )
83 29 8 ifcld ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → if ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) ∈ ℝ )
84 22 nngt0d ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 0 < 𝐵 )
85 max2 ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ≤ if ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) )
86 8 29 85 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 𝐵 ≤ if ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) )
87 25 29 83 84 86 ltletrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → 0 < if ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) )
88 lerec ⊢ ( ( ( 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 ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) ) ) )
89 83 87 38 39 88 syl22anc ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 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 ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) ) ) )
90 82 89 mpbid ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ≤ ( 1 / if ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) ) )
91 14 24 75 27 90 ltletrd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) ) )
92 oveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 𝑎 ) )
93 92 fvoveq1d ⊢ ( 𝑥 = 𝑎 → ( abs ‘ ( ( 𝐴 · 𝑥 ) − 𝑦 ) ) = ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑦 ) ) )
94 breq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ≤ 𝐵 ↔ 𝑎 ≤ 𝐵 ) )
95 id ⊢ ( 𝑥 = 𝑎 → 𝑥 = 𝑎 )
96 94 95 ifbieq2d ⊢ ( 𝑥 = 𝑎 → if ( 𝑥 ≤ 𝐵 , 𝐵 , 𝑥 ) = if ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) )
97 96 oveq2d ⊢ ( 𝑥 = 𝑎 → ( 1 / if ( 𝑥 ≤ 𝐵 , 𝐵 , 𝑥 ) ) = ( 1 / if ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) ) )
98 93 97 breq12d ⊢ ( 𝑥 = 𝑎 → ( ( abs ‘ ( ( 𝐴 · 𝑥 ) − 𝑦 ) ) < ( 1 / if ( 𝑥 ≤ 𝐵 , 𝐵 , 𝑥 ) ) ↔ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑦 ) ) < ( 1 / if ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) ) ) )
99 oveq2 ⊢ ( 𝑦 = 𝑏 → ( ( 𝐴 · 𝑎 ) − 𝑦 ) = ( ( 𝐴 · 𝑎 ) − 𝑏 ) )
100 99 fveq2d ⊢ ( 𝑦 = 𝑏 → ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑦 ) ) = ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) )
101 100 breq1d ⊢ ( 𝑦 = 𝑏 → ( ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑦 ) ) < ( 1 / if ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) ) ↔ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) ) ) )
102 98 101 rspc2ev ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝑎 ≤ 𝐵 , 𝐵 , 𝑎 ) ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( abs ‘ ( ( 𝐴 · 𝑥 ) − 𝑦 ) ) < ( 1 / if ( 𝑥 ≤ 𝐵 , 𝐵 , 𝑥 ) ) )
103 2 73 91 102 syl3anc ⊢ ( ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) ∧ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) ∧ 𝑏 ∈ ℕ0 ) ∧ ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( abs ‘ ( ( 𝐴 · 𝑥 ) − 𝑦 ) ) < ( 1 / if ( 𝑥 ≤ 𝐵 , 𝐵 , 𝑥 ) ) )
104 19 21 ifcld ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) → if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ∈ ℕ )
105 irrapxlem3 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ∈ ℕ ) → ∃ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ∃ 𝑏 ∈ ℕ0 ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) )
106 5 104 105 syl2anc ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) → ∃ 𝑎 ∈ ( 1 ... if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) ∃ 𝑏 ∈ ℕ0 ( abs ‘ ( ( 𝐴 · 𝑎 ) − 𝑏 ) ) < ( 1 / if ( 𝐵 ≤ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) , 𝐵 ) ) )
107 103 106 r19.29vva ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( abs ‘ ( ( 𝐴 · 𝑥 ) − 𝑦 ) ) < ( 1 / if ( 𝑥 ≤ 𝐵 , 𝐵 , 𝑥 ) ) )