---

Step * 1 2 3 1 4 of Lemma qroot


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) ∈ ℤ
BY
{ (InstLemma `mul_preserves_le` [⌜0⌝;⌜p⌝;⌜n * c⌝]⋅ THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  k  :  \{2...\}
2.  n  :  \mBbbN{}\msupplus{}
3.  p  :  \mBbbZ{}
4.  \mneg{}p  <  0
5.  q  :  \mBbbZ{}
6.  0  <  q
7.  \mneg{}(q  =  0)
8.  \mneg{}\muparrow{}qeq(q;0)
9.  (0  \mleq{}  (p/q))  \mvee{}  (\muparrow{}isOdd(k))
10.  s  :  \mBbbB{}
11.  \mneg{}\muparrow{}s
12.  ff  =  (q  =\msubz{}  1)  \mwedge{}\msubb{}  (n  =\msubz{}  1)
13.  b  :  \mBbbN{}\msupplus{}
14.  b  =  (q  *  n)
15.  c  :  \mBbbN{}\msupplus{}
16.  \mneg{}-1  <  p  *  n  *  c
17.  c  =  b\^{}(k  -  1)
18.  a  :  \mBbbZ{}
19.  a  =  (p  *  n  *  c)
20.  d  :  \mBbbN{}\msupplus{}
21.  d  =  (c  -  1)
22.  x  :  \mBbbN{}
23.  y  :  \mBbbN{}\msupplus{}
24.  |a|  *  y\^{}k  <  (x  *  b)\^{}k
25.  (x  *  b)\^{}k  \mleq{}  ((|a|  +  d)  *  y\^{}k)
26.  (0  \mleq{}  (p/q))  {}\mRightarrow{}  (0  \mleq{}  (x/y))
27.  (0  \mleq{}  (p/q))  \mLeftarrow{}{}  0  \mleq{}  (x/y)
\mvdash{}  (-(p  *  n  *  c))  =  (p  *  n  *  c)


By

---

Latex:
(InstLemma  `mul\_preserves\_le`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}n  *  c\mkleeneclose{}]\mcdot{}  THEN  Auto')\mcdot{}

---

Home Index