---

Step * 2 3 1 of Lemma proper-divisor_wf


1. n : ℕ+
2. 5 ≤ n
3. 16 ≤ n
⊢ if n <z 81 then proper-divisor-aux(n;3;3;1;3) else eval m = iroot(4;n) + 1 in proper-divisor-aux(n;m;m;1;m) fi 
  ∈ Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])
BY
{ ((OldAutoSplit⋅ THEN (CallByValueReduce 0 THENA Auto)) THEN (InstLemma `iroot-property` [⌜4⌝;⌜n⌝]⋅ THENA Auto)) }

1
1. n : ℕ+
2. 5 ≤ n
3. 16 ≤ n
4. 81 ≤ n
5. (iroot(4;n)^4 ≤ n) ∧ n < (iroot(4;n) + 1)^4
⊢ 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))])

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  5  \mleq{}  n
3.  16  \mleq{}  n
\mvdash{}  if  n  <z  81
    then  proper-divisor-aux(n;3;3;1;3)
    else  eval  m  =  iroot(4;n)  +  1  in
              proper-divisor-aux(n;m;m;1;m)
    fi    \mmember{}  Dec(\mexists{}n1:\mBbbZ{}  [(n1  <  n  \mwedge{}  (2  \mleq{}  n1)  \mwedge{}  (n1  |  n))])


By

---

Latex:
((OldAutoSplit\mcdot{}  THEN  (CallByValueReduce  0  THENA  Auto))
  THEN  (InstLemma  `iroot-property`  [\mkleeneopen{}4\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index