Step
*
1
2
1
of Lemma
rmul-rinv1
1. x : ℝ
2. a : {2...}
3. mu-ge(λn.4 <z |x n|;1) = a ∈ {1...}
4. 4 < |x a|
5. ∀[i:ℕ+a]. (¬4 < |x i|)
6. ∀m:ℕ+. ((a ≤ m)
⇒ (m ≤ (a * |x m|)))
7. a * a ∈ ℕ
8. reg-seq-inv(reg-seq-adjust(a;x)) ∈ {f:ℕ+ ⟶ ℤ| 4 * ((4 * a * a) + 1)-regular-seq(f)}
⊢ bdd-diff(reg-seq-mul(x;accelerate(4 * ((4 * a * a) + 1);reg-seq-inv(reg-seq-adjust(a;x))));r1)
BY
{ ((RWO "reg-seq-mul-comm" 0 THENA Auto) THEN (RWO "accelerate-bdd-diff" 0 THEN Try (Complete (Auto)))⋅) }
1
1. x : ℝ
2. a : {2...}
3. mu-ge(λn.4 <z |x n|;1) = a ∈ {1...}
4. 4 < |x a|
5. ∀[i:ℕ+a]. (¬4 < |x i|)
6. ∀m:ℕ+. ((a ≤ m)
⇒ (m ≤ (a * |x m|)))
7. a * a ∈ ℕ
8. reg-seq-inv(reg-seq-adjust(a;x)) ∈ {f:ℕ+ ⟶ ℤ| 4 * ((4 * a * a) + 1)-regular-seq(f)}
⊢ bdd-diff(reg-seq-mul(reg-seq-inv(reg-seq-adjust(a;x));x);r1)
Latex:
Latex:
1. x : \mBbbR{}
2. a : \{2...\}
3. mu-ge(\mlambda{}n.4 <z |x n|;1) = a
4. 4 < |x a|
5. \mforall{}[i:\mBbbN{}\msupplus{}a]. (\mneg{}4 < |x i|)
6. \mforall{}m:\mBbbN{}\msupplus{}. ((a \mleq{} m) {}\mRightarrow{} (m \mleq{} (a * |x m|)))
7. a * a \mmember{} \mBbbN{}
8. reg-seq-inv(reg-seq-adjust(a;x)) \mmember{} \{f:\mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}| 4 * ((4 * a * a) + 1)-regular-seq(f)\}
\mvdash{} bdd-diff(reg-seq-mul(x;accelerate(4 * ((4 * a * a) + 1);reg-seq-inv(reg-seq-adjust(a;x))));r1)
By
Latex:
((RWO "reg-seq-mul-comm" 0 THENA Auto)
THEN (RWO "accelerate-bdd-diff" 0 THEN Try (Complete (Auto)))\mcdot{}
)
Home
Index