---

Step * 2 1 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 < (iroot(4;n) + 1)^4
⊢ (m * m) + 1 < n
BY
{ (SupposeNot THEN Assert ⌜iroot(4;n)^4 ≤ (((iroot(4;n) + 1) * (iroot(4;n) + 1)) + 1)⌝⋅) }

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

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

---

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  <  (iroot(4;n)  +  1)\^{}4
\mvdash{}  (m  *  m)  +  1  <  n


By

---

Latex:
(SupposeNot  THEN  Assert  \mkleeneopen{}iroot(4;n)\^{}4  \mleq{}  (((iroot(4;n)  +  1)  *  (iroot(4;n)  +  1))  +  1)\mkleeneclose{}\mcdot{})

---

Home Index