---

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


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

---

Latex:

---

Latex:

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


By

---

Latex:
(Subst'  \mkleeneopen{}n  =  1\mkleeneclose{}  0\mcdot{}  THEN  Auto'  THEN  Eliminate  \mkleeneopen{}s\mkleeneclose{}\mcdot{}  THEN  RW  assert\_pushdownC  (-1)  THEN  Auto)\mcdot{}

---

Home Index