---

Step * 2 1 2 1 of Lemma decidable__proper_divisor


1. n : {2...}
2. ¬(n ≤ 5)
3. m : ℕ
4. m = (iroot(4;n) + 1) ∈ ℕ
5. iroot(4;n)^4 ≤ n
6. n < m^4
7. (m * m) + 1 < n
⊢ n < (m * m) * m * m
BY
{ (Unfold `exp` -2 THEN RepeatFor 3 (((RWO "primrec-unroll" (-2) THENA Auto) THEN Reduce (-2)))) }

1
1. n : {2...}
2. ¬(n ≤ 5)
3. m : ℕ
4. m = (iroot(4;n) + 1) ∈ ℕ
5. iroot(4;n)^4 ≤ n
6. n < m * m * m * m * 1
7. (m * m) + 1 < n
⊢ n < (m * m) * m * m

---

Latex:

---

Latex:

1.  n  :  \{2...\}
2.  \mneg{}(n  \mleq{}  5)
3.  m  :  \mBbbN{}
4.  m  =  (iroot(4;n)  +  1)
5.  iroot(4;n)\^{}4  \mleq{}  n
6.  n  <  m\^{}4
7.  (m  *  m)  +  1  <  n
\mvdash{}  n  <  (m  *  m)  *  m  *  m


By

---

Latex:
(Unfold  `exp`  -2  THEN  RepeatFor  3  (((RWO  "primrec-unroll"  (-2)  THENA  Auto)  THEN  Reduce  (-2))))

---

Home Index