Step
*
1
2
3
1
of Lemma
qroot
.....assertion.....
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. (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)
⊢ |a| = if p <z 0 then -a else a fi ∈ ℤ
BY
{ ((RWO "absval_unfold" 0 THENA Auto) THEN HypSubst' 16 0 THEN AutoBoolCase⌜s⌝⋅ THEN RepeatFor 2 (AutoSplit)) }
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. x : ℕ
20. y : ℕ+
21. |a| * y^k < (x * b)^k
22. (x * b)^k ≤ ((|a| + 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. ↑s
26. -1 < p * 2 * c
27. p < 0
⊢ (p * 2 * c) = (-(p * 2 * c)) ∈ ℤ
2
1. k : {2...}
2. n : ℕ+
3. p : ℤ
4. ¬p < 0
5. q : ℤ
6. 0 < q
7. ¬(q = 0 ∈ ℚ)
8. ¬↑qeq(q;0)
9. (0 ≤ (p/q)) ∨ (↑isOdd(k))
10. s : 𝔹
11. s = (q =z 1) ∧b (n =z 1)
12. b : ℕ+
13. b = if s then 2 else q * n fi ∈ ℕ+
14. c : ℕ+
15. ¬-1 < p * 2 * c
16. c = b^(k - 1) ∈ ℕ+
17. a : ℤ
18. a = if s then p * 2 * c else p * n * c fi ∈ ℤ
19. d : ℕ+
20. d = (if s then 2 * c else c fi - 1) ∈ ℕ+
21. x : ℕ
22. y : ℕ+
23. |a| * y^k < (x * b)^k
24. (x * b)^k ≤ ((|a| + d) * y^k)
25. (0 ≤ (p/q)) ⇒ (0 ≤ (x/y))
26. (0 ≤ (p/q)) ⇐ 0 ≤ (x/y)
27. ↑s
⊢ (-(p * 2 * c)) = (p * 2 * c) ∈ ℤ
3
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
11. ff = (q =z 1) ∧b (n =z 1)
12. b : ℕ+
13. b = (q * n) ∈ ℕ+
14. c : ℕ+
15. c = b^(k - 1) ∈ ℕ+
16. a : ℤ
17. a = (p * n * c) ∈ ℤ
18. d : ℕ+
19. d = (c - 1) ∈ ℕ+
20. x : ℕ
21. y : ℕ+
22. |a| * y^k < (x * b)^k
23. (x * b)^k ≤ ((|a| + d) * y^k)
24. (0 ≤ (p/q)) ⇒ (0 ≤ (if p <z 0 then -x else x fi /y))
25. (0 ≤ (p/q)) ⇐ 0 ≤ (if p <z 0 then -x else x fi /y)
26. -1 < p * n * c
27. p < 0
⊢ (p * n * c) = (-(p * n * c)) ∈ ℤ
4
1. k : {2...}
2. n : ℕ+
3. p : ℤ
4. ¬p < 0
5. q : ℤ
6. 0 < q
7. ¬(q = 0 ∈ ℚ)
8. ¬↑qeq(q;0)
9. (0 ≤ (p/q)) ∨ (↑isOdd(k))
10. s : 𝔹
11. ¬↑s
12. ff = (q =z 1) ∧b (n =z 1)
13. b : ℕ+
14. b = (q * n) ∈ ℕ+
15. c : ℕ+
16. ¬-1 < p * n * c
17. c = b^(k - 1) ∈ ℕ+
18. a : ℤ
19. a = (p * n * c) ∈ ℤ
20. d : ℕ+
21. d = (c - 1) ∈ ℕ+
22. x : ℕ
23. y : ℕ+
24. |a| * y^k < (x * b)^k
25. (x * b)^k ≤ ((|a| + d) * y^k)
26. (0 ≤ (p/q)) ⇒ (0 ≤ (x/y))
27. (0 ≤ (p/q)) ⇐ 0 ≤ (x/y)
⊢ (-(p * n * c)) = (p * n * c) ∈ ℤ
Latex:
Latex:
.....assertion.....
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. (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)
\mvdash{} |a| = if p <z 0 then -a else a fi
By
Latex:
((RWO "absval\_unfold" 0 THENA Auto)
THEN HypSubst' 16 0
THEN AutoBoolCase\mkleeneopen{}s\mkleeneclose{}\mcdot{}
THEN RepeatFor 2 (AutoSplit))
Home
Index