Step
*
1
2
3
2
2
2
1
of Lemma
qroot
1. k : {2...}
2. n : ℕ+
3. p : ℤ
4. q : ℤ
5. 0 < q
6. ¬(q = 0 ∈ ℚ)
7. ¬↑qeq(q;0)
8. (0 ≤ (p/q)) ∨ (↑isOdd(k))
9. s : 𝔹
10. s = (q =z 1) ∧b (n =z 1)
11. b : ℕ+
12. b = if s then 2 else q * n fi ∈ ℕ+
13. c : ℕ+
14. c = b^(k - 1) ∈ ℕ+
15. a : ℤ
16. a = if s then p * 2 * c else p * n * c fi ∈ ℤ
17. d : ℕ+
18. d = (if s then 2 * c else c fi - 1) ∈ ℕ+
19. x : ℕ
20. y : ℕ+
21. |a| * y^k < (x * b)^k
22. (x * b)^k ≤ ((|a| + d) * y^k)
23. |a| = if p <z 0 then -a else a fi ∈ ℤ
24. (d/b^k) < (1/n)
⊢ |(if p <z 0 then -x else x fi /y) ↑ k - (a/b^k)| < (1/n)
BY
{ ((RWO "exp-of-mul" (-3) THENA Auto)
THEN (RWO "exp-of-mul" (-4) THENA Auto)
THEN MoveToConcl (-2)
THEN OldAutoSplit
THEN Auto
THEN HypSubst' (-1) (-5)
THEN HypSubst' (-1) (-4)
THEN Thin (-1)
THEN ((RWO "qexp-qdiv" 0 THENA Auto')
THEN ((RWO "qexp-exp" 0 THENA Auto')
THEN Try ((Subst ⌜-x ~ (-1) * x⌝ 0⋅
THEN Auto
THEN (RWO "exp-of-mul" 0 THENA Auto')
THEN (RWO "exp-minusone" 0 THENA Auto')
THEN OldAutoSplit
THEN Try ((SplitOrHyps
THEN Try ((QMul ⌜q⌝ 8⋅ THEN Auto' THEN RWO "qle-int" 8 THEN Auto'))
THEN Unfold `isOdd` 8
THEN RW assert_pushdownC 8
THEN Complete (Auto)))
THEN Thin (-1))⋅)⋅
THEN (RepeatFor 3 (MoveToConcl (-2))
THEN (GenConcl ⌜x^k = X ∈ ℕ⌝⋅ THENA Auto')
THEN (GenConcl ⌜y^k = Z ∈ ℕ+⌝⋅ THENA Auto')
THEN ThinVar `y'
THEN ThinVar `x'
THEN GenConcl ⌜b^k = B ∈ ℕ+⌝⋅⋅
THEN Auto')⋅)⋅
)⋅) }
1
1. k : {2...}
2. n : ℕ+
3. p : ℤ
4. q : ℤ
5. 0 < q
6. ¬(q = 0 ∈ ℚ)
7. ¬↑qeq(q;0)
8. (0 ≤ (p/q)) ∨ (↑isOdd(k))
9. s : 𝔹
10. s = (q =z 1) ∧b (n =z 1)
11. b : ℕ+
12. b = if s then 2 else q * n fi ∈ ℕ+
13. c : ℕ+
14. c = b^(k - 1) ∈ ℕ+
15. a : ℤ
16. a = if s then p * 2 * c else p * n * c fi ∈ ℤ
17. d : ℕ+
18. d = (if s then 2 * c else c fi - 1) ∈ ℕ+
19. p < 0
20. X : ℕ
21. Z : ℕ+
22. B : ℕ+
23. b^k = B ∈ ℕ+
24. (-a) * Z < X * B
25. (X * B) ≤ (((-a) + d) * Z)
26. (d/B) < (1/n)
⊢ |((-1) * X/Z) - (a/B)| < (1/n)
2
1. k : {2...}
2. n : ℕ+
3. p : ℤ
4. q : ℤ
5. 0 < q
6. ¬(q = 0 ∈ ℚ)
7. ¬↑qeq(q;0)
8. (0 ≤ (p/q)) ∨ (↑isOdd(k))
9. s : 𝔹
10. s = (q =z 1) ∧b (n =z 1)
11. b : ℕ+
12. b = if s then 2 else q * n fi ∈ ℕ+
13. c : ℕ+
14. c = b^(k - 1) ∈ ℕ+
15. a : ℤ
16. a = if s then p * 2 * c else p * n * c fi ∈ ℤ
17. d : ℕ+
18. d = (if s then 2 * c else c fi - 1) ∈ ℕ+
19. 0 ≤ p
20. X : ℕ
21. Z : ℕ+
22. B : ℕ+
23. b^k = B ∈ ℕ+
24. a * Z < X * B
25. (X * B) ≤ ((a + d) * Z)
26. (d/B) < (1/n)
⊢ |(X/Z) - (a/B)| < (1/n)
Latex:
Latex:
1. k : \{2...\}
2. n : \mBbbN{}\msupplus{}
3. p : \mBbbZ{}
4. q : \mBbbZ{}
5. 0 < q
6. \mneg{}(q = 0)
7. \mneg{}\muparrow{}qeq(q;0)
8. (0 \mleq{} (p/q)) \mvee{} (\muparrow{}isOdd(k))
9. s : \mBbbB{}
10. s = (q =\msubz{} 1) \mwedge{}\msubb{} (n =\msubz{} 1)
11. b : \mBbbN{}\msupplus{}
12. b = if s then 2 else q * n fi
13. c : \mBbbN{}\msupplus{}
14. c = b\^{}(k - 1)
15. a : \mBbbZ{}
16. a = if s then p * 2 * c else p * n * c fi
17. d : \mBbbN{}\msupplus{}
18. d = (if s then 2 * c else c fi - 1)
19. x : \mBbbN{}
20. y : \mBbbN{}\msupplus{}
21. |a| * y\^{}k < (x * b)\^{}k
22. (x * b)\^{}k \mleq{} ((|a| + d) * y\^{}k)
23. |a| = if p <z 0 then -a else a fi
24. (d/b\^{}k) < (1/n)
\mvdash{} |(if p <z 0 then -x else x fi /y) \muparrow{} k - (a/b\^{}k)| < (1/n)
By
Latex:
((RWO "exp-of-mul" (-3) THENA Auto)
THEN (RWO "exp-of-mul" (-4) THENA Auto)
THEN MoveToConcl (-2)
THEN OldAutoSplit
THEN Auto
THEN HypSubst' (-1) (-5)
THEN HypSubst' (-1) (-4)
THEN Thin (-1)
THEN ((RWO "qexp-qdiv" 0 THENA Auto')
THEN ((RWO "qexp-exp" 0 THENA Auto')
THEN Try ((Subst \mkleeneopen{}-x \msim{} (-1) * x\mkleeneclose{} 0\mcdot{}
THEN Auto
THEN (RWO "exp-of-mul" 0 THENA Auto')
THEN (RWO "exp-minusone" 0 THENA Auto')
THEN OldAutoSplit
THEN Try ((SplitOrHyps
THEN Try ((QMul \mkleeneopen{}q\mkleeneclose{} 8\mcdot{}
THEN Auto'
THEN RWO "qle-int" 8
THEN Auto'))
THEN Unfold `isOdd` 8
THEN RW assert\_pushdownC 8
THEN Complete (Auto)))
THEN Thin (-1))\mcdot{})\mcdot{}
THEN (RepeatFor 3 (MoveToConcl (-2))
THEN (GenConcl \mkleeneopen{}x\^{}k = X\mkleeneclose{}\mcdot{} THENA Auto')
THEN (GenConcl \mkleeneopen{}y\^{}k = Z\mkleeneclose{}\mcdot{} THENA Auto')
THEN ThinVar `y'
THEN ThinVar `x'
THEN GenConcl \mkleeneopen{}b\^{}k = B\mkleeneclose{}\mcdot{}\mcdot{}
THEN Auto')\mcdot{})\mcdot{}
)\mcdot{})
Home
Index