---

Step * 2 3 1 1 2 of Lemma proper-divisor_wf


1. n : ℕ+
2. 5 ≤ n
3. 16 ≤ n
4. 81 ≤ n
5. (iroot(4;n)^4 ≤ n) ∧ n < (iroot(4;n) + 1)^4
6. ¬(iroot(4;n) ≤ 2)
⊢ proper-divisor-aux(n;iroot(4;n) + 1;iroot(4;n) + 1;1;iroot(4;n) + 1) ∈ Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])
BY
{ xxx((Assert 2 < iroot(4;n) BY
             Auto)
      THEN MoveToConcl (-1)
      THEN MoveToConcl (-2)
      THEN GenConclAtAddr [1;1;1;1]
      THEN All Thin
      THEN RenameVar `m' (-1)
      THEN Auto)xxx }

1
1. n : ℕ+
2. m : ℕ
3. m^4 ≤ n
4. n < (m + 1)^4
5. 2 < m
⊢ n < ((m + 1) * (m + 1)) * (m + 1) * (m + 1)

2
1. n : ℕ+
2. m : ℕ
3. m^4 ≤ n
4. n < (m + 1)^4
5. 2 < m
⊢ (m + 1) * (m + 1) < n

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  5  \mleq{}  n
3.  16  \mleq{}  n
4.  81  \mleq{}  n
5.  (iroot(4;n)\^{}4  \mleq{}  n)  \mwedge{}  n  <  (iroot(4;n)  +  1)\^{}4
6.  \mneg{}(iroot(4;n)  \mleq{}  2)
\mvdash{}  proper-divisor-aux(n;iroot(4;n)  +  1;iroot(4;n)  +  1;1;iroot(4;n)  +  1)  \mmember{}  Dec(\mexists{}n1:\mBbbZ{}  [(n1  <  n
                                                                                                                                                                      \mwedge{}  (2  \mleq{}  n1)
                                                                                                                                                                      \mwedge{}  (n1  |  n))])


By

---

Latex:
xxx((Assert  2  <  iroot(4;n)  BY
                      Auto)
        THEN  MoveToConcl  (-1)
        THEN  MoveToConcl  (-2)
        THEN  GenConclAtAddr  [1;1;1;1]
        THEN  All  Thin
        THEN  RenameVar  `m'  (-1)
        THEN  Auto)xxx

---

Home Index