---

Step * 1 2 2 2 2 1 1 2 of Lemma near-root-rational


1. s : 𝔹
2. ¬↑s
3. q : ℕ+
4. n : ℕ+
5. b : ℕ+
6. k : {2...}
7. c : ℕ+
8. p : ℤ
9. (0 ≤ p) ∨ (↑isOdd(k))
10. ff = (q =z 1) ∧b (n =z 1)
11. b = (q * n) ∈ ℕ+
12. c = (q * n)^(k - 1) ∈ ℕ+
13. a : ℤ
14. a = (p * n * (q * n)^(k - 1)) ∈ ℤ
15. d : ℕ+
16. d = ((q * n)^(k - 1) - 1) ∈ ℕ+
17. x : ℕ
18. y : ℕ+
19. |a| * y^k < (x * q * n)^k
20. (x * q * n)^k ≤ ((|a| + ((q * n)^(k - 1) - 1)) * y^k)
21. (0 ≤ p) ⇒ (0 ≤ if p <z 0 then -x else x fi )
22. (0 ≤ p) ⇐ 0 ≤ if p <z 0 then -x else x fi 
23. |a| = if p <z 0 then -a else a fi  ∈ ℤ
⊢ ((q * n)^(k - 1) - 1) * n < 1 * (q * n) * (q * n)^(k - 1)
BY
{ (GenConclAtAddr [1;1;1]⋅
   THEN ((InstLemma `mul_preserves_lt` [⌜v - 1⌝;⌜q * v⌝;⌜n⌝]⋅ THEN Auto)
         THEN InstLemma `mul_preserves_le` [⌜1⌝;⌜q⌝;⌜v⌝]⋅
         THEN Auto)⋅
   ) }

---

Latex:

---

Latex:

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


By

---

Latex:
(GenConclAtAddr  [1;1;1]\mcdot{}
  THEN  ((InstLemma  `mul\_preserves\_lt`  [\mkleeneopen{}v  -  1\mkleeneclose{};\mkleeneopen{}q  *  v\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)
              THEN  InstLemma  `mul\_preserves\_le`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}
              THEN  Auto)\mcdot{}
  )

---

Home Index