---

Step * 2 3 of Lemma proper-divisor_wf


1. n : ℕ+
2. y : Top
3. 5 ≤ n
4. 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
{ Thin 2 }

1
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))])

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  y  :  Top
3.  5  \mleq{}  n
4.  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:
Thin  2

---

Home Index