Step
*
1
1
of Lemma
regular-upto-iff
1. k : ℕ+
2. b : ℕ+
3. x : ℕ+ ⟶ ℤ
4. ∀i,j:ℕ+b + 1. (|(i * (x j)) - j * (x i)| ≤ ((2 * k) * (i + j)))
5. n : ℕ+b + 1
6. m : ℕ+b + 1
⊢ let j = seq-min-upper(k;b;x) in
let z = (r((x j) + (2 * k))/r((2 * k) * j)) in
(((r((x n) - 2 * k)/r((2 * k) * n)) ≤ z) ∧ (z ≤ (r((x n) + (2 * k))/r((2 * k) * n))))
∧ ((r((x m) - 2 * k)/r((2 * k) * m)) ≤ z)
∧ (z ≤ (r((x m) + (2 * k))/r((2 * k) * m)))
BY
{ ((InstLemma `seq-min-upper-property` [⌜k⌝;⌜b⌝;⌜x⌝]⋅ THENA Auto)
THEN MoveToConcl (-1)
THEN (GenConcl ⌜seq-min-upper(k;b;x) = j ∈ ℕ+b + 1⌝⋅
THENA (Auto THEN InstLemma `seq-min-upper-le` [⌜k⌝;⌜b⌝;⌜x⌝]⋅ THEN Auto)
)
THEN (D 0 THENA Auto)
THEN (InstHyp [⌜n⌝] (-1)⋅ THENA Auto)
THEN (D -2 With ⌜m⌝ THENA Auto)
THEN RepUR ``let`` 0
THEN RWO "rleq-int-fractions" 0
THEN Auto) }
1
1. k : ℕ+
2. b : ℕ+
3. x : ℕ+ ⟶ ℤ
4. ∀i,j:ℕ+b + 1. (|(i * (x j)) - j * (x i)| ≤ ((2 * k) * (i + j)))
5. n : ℕ+b + 1
6. m : ℕ+b + 1
7. j : ℕ+b + 1
8. seq-min-upper(k;b;x) = j ∈ ℕ+b + 1
9. ((n * (x j)) - j * (x n)) ≤ ((2 * k) * (j - n))
10. ((m * (x j)) - j * (x m)) ≤ ((2 * k) * (j - m))
⊢ (((x n) - 2 * k) * (2 * k) * j) ≤ (((x j) + (2 * k)) * (2 * k) * n)
2
1. k : ℕ+
2. b : ℕ+
3. x : ℕ+ ⟶ ℤ
4. ∀i,j:ℕ+b + 1. (|(i * (x j)) - j * (x i)| ≤ ((2 * k) * (i + j)))
5. n : ℕ+b + 1
6. m : ℕ+b + 1
7. j : ℕ+b + 1
8. seq-min-upper(k;b;x) = j ∈ ℕ+b + 1
9. ((n * (x j)) - j * (x n)) ≤ ((2 * k) * (j - n))
10. ((m * (x j)) - j * (x m)) ≤ ((2 * k) * (j - m))
11. (((x n) - 2 * k) * (2 * k) * j) ≤ (((x j) + (2 * k)) * (2 * k) * n)
⊢ (((x j) + (2 * k)) * (2 * k) * n) ≤ (((x n) + (2 * k)) * (2 * k) * j)
3
1. k : ℕ+
2. b : ℕ+
3. x : ℕ+ ⟶ ℤ
4. ∀i,j:ℕ+b + 1. (|(i * (x j)) - j * (x i)| ≤ ((2 * k) * (i + j)))
5. n : ℕ+b + 1
6. m : ℕ+b + 1
7. j : ℕ+b + 1
8. seq-min-upper(k;b;x) = j ∈ ℕ+b + 1
9. ((n * (x j)) - j * (x n)) ≤ ((2 * k) * (j - n))
10. ((m * (x j)) - j * (x m)) ≤ ((2 * k) * (j - m))
11. (((x n) - 2 * k) * (2 * k) * j) ≤ (((x j) + (2 * k)) * (2 * k) * n)
12. (((x j) + (2 * k)) * (2 * k) * n) ≤ (((x n) + (2 * k)) * (2 * k) * j)
⊢ (((x m) - 2 * k) * (2 * k) * j) ≤ (((x j) + (2 * k)) * (2 * k) * m)
4
1. k : ℕ+
2. b : ℕ+
3. x : ℕ+ ⟶ ℤ
4. ∀i,j:ℕ+b + 1. (|(i * (x j)) - j * (x i)| ≤ ((2 * k) * (i + j)))
5. n : ℕ+b + 1
6. m : ℕ+b + 1
7. j : ℕ+b + 1
8. seq-min-upper(k;b;x) = j ∈ ℕ+b + 1
9. ((n * (x j)) - j * (x n)) ≤ ((2 * k) * (j - n))
10. ((m * (x j)) - j * (x m)) ≤ ((2 * k) * (j - m))
11. (((x n) - 2 * k) * (2 * k) * j) ≤ (((x j) + (2 * k)) * (2 * k) * n)
12. (((x j) + (2 * k)) * (2 * k) * n) ≤ (((x n) + (2 * k)) * (2 * k) * j)
13. (((x m) - 2 * k) * (2 * k) * j) ≤ (((x j) + (2 * k)) * (2 * k) * m)
⊢ (((x j) + (2 * k)) * (2 * k) * m) ≤ (((x m) + (2 * k)) * (2 * k) * j)
Latex:
Latex:
1. k : \mBbbN{}\msupplus{}
2. b : \mBbbN{}\msupplus{}
3. x : \mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}
4. \mforall{}i,j:\mBbbN{}\msupplus{}b + 1. (|(i * (x j)) - j * (x i)| \mleq{} ((2 * k) * (i + j)))
5. n : \mBbbN{}\msupplus{}b + 1
6. m : \mBbbN{}\msupplus{}b + 1
\mvdash{} let j = seq-min-upper(k;b;x) in
let z = (r((x j) + (2 * k))/r((2 * k) * j)) in
(((r((x n) - 2 * k)/r((2 * k) * n)) \mleq{} z) \mwedge{} (z \mleq{} (r((x n) + (2 * k))/r((2 * k) * n))))
\mwedge{} ((r((x m) - 2 * k)/r((2 * k) * m)) \mleq{} z)
\mwedge{} (z \mleq{} (r((x m) + (2 * k))/r((2 * k) * m)))
By
Latex:
((InstLemma `seq-min-upper-property` [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{} THENA Auto)
THEN MoveToConcl (-1)
THEN (GenConcl \mkleeneopen{}seq-min-upper(k;b;x) = j\mkleeneclose{}\mcdot{}
THENA (Auto THEN InstLemma `seq-min-upper-le` [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{} THEN Auto)
)
THEN (D 0 THENA Auto)
THEN (InstHyp [\mkleeneopen{}n\mkleeneclose{}] (-1)\mcdot{} THENA Auto)
THEN (D -2 With \mkleeneopen{}m\mkleeneclose{} THENA Auto)
THEN RepUR ``let`` 0
THEN RWO "rleq-int-fractions" 0
THEN Auto)
Home
Index