Step
*
1
2
3
2
1
1
of Lemma
qroot
1. b : ℕ+
2. k : {2...}
3. s : 𝔹
4. p : ℤ
5. c : ℕ+
6. n : ℕ+
7. q : ℤ
8. 0 < q
9. ¬(q = 0 ∈ ℚ)
10. ¬↑qeq(q;0)
11. (0 ≤ (p/q)) ∨ (↑isOdd(k))
12. s = (q =z 1) ∧b (n =z 1)
13. b = if s then 2 else q * n fi ∈ ℕ+
14. c = b^(k - 1) ∈ ℕ+
15. a : ℤ
16. a = if s then p * 2 * b^(k - 1) else p * n * b^(k - 1) fi ∈ ℤ
17. d : ℕ+
18. d = (if s then 2 * b^(k - 1) else b^(k - 1) fi - 1) ∈ ℕ+
19. x : ℕ
20. y : ℕ+
21. |if s then p * 2 * b^(k - 1) else p * n * b^(k - 1) fi | * y^k < (x * b)^k
22. (x * b)^k ≤ ((|if s then p * 2 * b^(k - 1) else p * n * b^(k - 1) fi | + d) * y^k)
23. (0 ≤ (p/q)) ⇒ (0 ≤ (if p <z 0 then -x else x fi /y))
24. (0 ≤ (p/q)) ⇐ 0 ≤ (if p <z 0 then -x else x fi /y)
25. |if s then p * 2 * b^(k - 1) else p * n * b^(k - 1) fi |
= if p <z 0 then -if s then p * 2 * b^(k - 1) else p * n * b^(k - 1) fi
if s then p * 2 * b^(k - 1)
else p * n * b^(k - 1)
fi
∈ ℤ
26. ↑s
⊢ (p/q) = (p * 2 * b^(k - 1)/b^k) ∈ ℚ
BY
{ (QMul ⌜b^k⌝ 0⋅ THEN Auto)⋅ }
1
.....wf.....
1. b : ℕ+
2. k : {2...}
3. s : 𝔹
4. p : ℤ
5. c : ℕ+
6. n : ℕ+
7. q : ℤ
8. 0 < q
9. ¬(q = 0 ∈ ℚ)
10. ¬↑qeq(q;0)
11. (0 ≤ (p/q)) ∨ (↑isOdd(k))
12. s = (q =z 1) ∧b (n =z 1)
13. b = if s then 2 else q * n fi ∈ ℕ+
14. c = b^(k - 1) ∈ ℕ+
15. a : ℤ
16. a = if s then p * 2 * b^(k - 1) else p * n * b^(k - 1) fi ∈ ℤ
17. d : ℕ+
18. d = (if s then 2 * b^(k - 1) else b^(k - 1) fi - 1) ∈ ℕ+
19. x : ℕ
20. y : ℕ+
21. |if s then p * 2 * b^(k - 1) else p * n * b^(k - 1) fi | * y^k < (x * b)^k
22. (x * b)^k ≤ ((|if s then p * 2 * b^(k - 1) else p * n * b^(k - 1) fi | + d) * y^k)
23. (0 ≤ (p/q)) ⇒ (0 ≤ (if p <z 0 then -x else x fi /y))
24. (0 ≤ (p/q)) ⇐ 0 ≤ (if p <z 0 then -x else x fi /y)
25. |if s then p * 2 * b^(k - 1) else p * n * b^(k - 1) fi |
= if p <z 0 then -if s then p * 2 * b^(k - 1) else p * n * b^(k - 1) fi
if s then p * 2 * b^(k - 1)
else p * n * b^(k - 1)
fi
∈ ℤ
26. ↑s
⊢ 2 * b^(k - 1) ∈ ℤ
2
1. b : ℕ+
2. k : {2...}
3. s : 𝔹
4. p : ℤ
5. c : ℕ+
6. n : ℕ+
7. q : ℤ
8. 0 < q
9. ¬(q = 0 ∈ ℚ)
10. ¬↑qeq(q;0)
11. (0 ≤ (p/q)) ∨ (↑isOdd(k))
12. s = (q =z 1) ∧b (n =z 1)
13. b = if s then 2 else q * n fi ∈ ℕ+
14. c = b^(k - 1) ∈ ℕ+
15. a : ℤ
16. a = if s then p * 2 * b^(k - 1) else p * n * b^(k - 1) fi ∈ ℤ
17. d : ℕ+
18. d = (if s then 2 * b^(k - 1) else b^(k - 1) fi - 1) ∈ ℕ+
19. x : ℕ
20. y : ℕ+
21. |if s then p * 2 * b^(k - 1) else p * n * b^(k - 1) fi | * y^k < (x * b)^k
22. (x * b)^k ≤ ((|if s then p * 2 * b^(k - 1) else p * n * b^(k - 1) fi | + d) * y^k)
23. (0 ≤ (p/q)) ⇒ (0 ≤ (if p <z 0 then -x else x fi /y))
24. (0 ≤ (p/q)) ⇐ 0 ≤ (if p <z 0 then -x else x fi /y)
25. |if s then p * 2 * b^(k - 1) else p * n * b^(k - 1) fi |
= if p <z 0 then -if s then p * 2 * b^(k - 1) else p * n * b^(k - 1) fi
if s then p * 2 * b^(k - 1)
else p * n * b^(k - 1)
fi
∈ ℤ
26. ↑s
⊢ (b^k * (p/q)) = (2 * b^(k - 1) * p) ∈ ℚ
Latex:
Latex:
1. b : \mBbbN{}\msupplus{}
2. k : \{2...\}
3. s : \mBbbB{}
4. p : \mBbbZ{}
5. c : \mBbbN{}\msupplus{}
6. n : \mBbbN{}\msupplus{}
7. q : \mBbbZ{}
8. 0 < q
9. \mneg{}(q = 0)
10. \mneg{}\muparrow{}qeq(q;0)
11. (0 \mleq{} (p/q)) \mvee{} (\muparrow{}isOdd(k))
12. s = (q =\msubz{} 1) \mwedge{}\msubb{} (n =\msubz{} 1)
13. b = if s then 2 else q * n fi
14. c = b\^{}(k - 1)
15. a : \mBbbZ{}
16. a = if s then p * 2 * b\^{}(k - 1) else p * n * b\^{}(k - 1) fi
17. d : \mBbbN{}\msupplus{}
18. d = (if s then 2 * b\^{}(k - 1) else b\^{}(k - 1) fi - 1)
19. x : \mBbbN{}
20. y : \mBbbN{}\msupplus{}
21. |if s then p * 2 * b\^{}(k - 1) else p * n * b\^{}(k - 1) fi | * y\^{}k < (x * b)\^{}k
22. (x * b)\^{}k \mleq{} ((|if s then p * 2 * b\^{}(k - 1) else p * n * b\^{}(k - 1) fi | + d) * y\^{}k)
23. (0 \mleq{} (p/q)) {}\mRightarrow{} (0 \mleq{} (if p <z 0 then -x else x fi /y))
24. (0 \mleq{} (p/q)) \mLeftarrow{}{} 0 \mleq{} (if p <z 0 then -x else x fi /y)
25. |if s then p * 2 * b\^{}(k - 1) else p * n * b\^{}(k - 1) fi |
= if p <z 0 then -if s then p * 2 * b\^{}(k - 1) else p * n * b\^{}(k - 1) fi
if s then p * 2 * b\^{}(k - 1)
else p * n * b\^{}(k - 1)
fi
26. \muparrow{}s
\mvdash{} (p/q) = (p * 2 * b\^{}(k - 1)/b\^{}k)
By
Latex:
(QMul \mkleeneopen{}b\^{}k\mkleeneclose{} 0\mcdot{} THEN Auto)\mcdot{}
Home
Index