---

Step * 2 1 of Lemma proper-divisor-aux_wf


1. n : ℕ+
2. m : ℕ
3. n < (m * m) * m * m
4. m * m < n
5. 1 < m ∧ (∀i:ℕm. ((0 ≤ (i * m)) ∧ (i * m) + m < n))
6. ∀b:ℕ
     ((b ≤ m)
     ⇒ (proper-divisor-aux(n;m;b;(m * (m - b)) + 1;m * ((m - b) + 1)) ∈ (∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])
         ∨ (¬(∃i:{m - b..m-}. (↑isl(divisor-test(n;(i * m) + 1;(i * m) + m)))))))
7. proper-divisor-aux(n;m;m;1;m) ∈ (∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])
   ∨ (¬(∃i:ℕm. (↑isl(divisor-test(n;(i * m) + 1;(i * m) + m)))))
8. proper-divisor-aux(n;m;m;1;m)
= proper-divisor-aux(n;m;m;1;m)
∈ ((∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))]) ∨ (¬(∃i:ℕm. (↑isl(divisor-test(n;(i * m) + 1;(i * m) + m))))))
⊢ ((∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))]) ∨ (¬(∃i:ℕm. (↑isl(divisor-test(n;(i * m) + 1;(i * m) + m)))))) ⊆r Dec(∃n1:ℤ
    [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])
BY
{ (RepUR ``or decidable`` 0
   THEN GenConclAtAddr [1;1]
   THEN Auto
   THEN Try (OnMaybeHyp 6 (\h. (InstHyp [⌜i⌝] h⋅ THEN Complete (Auto')))⋅)) }

1
1. n : ℕ+
2. m : ℕ
3. n < (m * m) * m * m
4. m * m < n
5. 1 < m
6. ∀i:ℕm. ((0 ≤ (i * m)) ∧ (i * m) + m < n)
7. ∀b:ℕ
     ((b ≤ m)
     ⇒ (proper-divisor-aux(n;m;b;(m * (m - b)) + 1;m * ((m - b) + 1)) ∈ (∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])
         ∨ (¬(∃i:{m - b..m-}. (↑isl(divisor-test(n;(i * m) + 1;(i * m) + m)))))))
8. proper-divisor-aux(n;m;m;1;m) ∈ (∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])
   ∨ (¬(∃i:ℕm. (↑isl(divisor-test(n;(i * m) + 1;(i * m) + m)))))
9. proper-divisor-aux(n;m;m;1;m)
= proper-divisor-aux(n;m;m;1;m)
∈ ((∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))]) ∨ (¬(∃i:ℕm. (↑isl(divisor-test(n;(i * m) + 1;(i * m) + m))))))
10. v : ℙ@i'
11. (∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))]) = v ∈ ℙ
⊢ (v + (¬(∃i:ℕm. (↑isl(divisor-test(n;(i * m) + 1;(i * m) + m)))))) ⊆r (v + (¬v))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  m  :  \mBbbN{}
3.  n  <  (m  *  m)  *  m  *  m
4.  m  *  m  <  n
5.  1  <  m  \mwedge{}  (\mforall{}i:\mBbbN{}m.  ((0  \mleq{}  (i  *  m))  \mwedge{}  (i  *  m)  +  m  <  n))
6.  \mforall{}b:\mBbbN{}
          ((b  \mleq{}  m)
          {}\mRightarrow{}  (proper-divisor-aux(n;m;b;(m  *  (m  -  b))  +  1;m  *  ((m  -  b)  +  1))  \mmember{}  (\mexists{}n1:\mBbbZ{}  [(n1  <  n
                                                                                                                                                                \mwedge{}  (2  \mleq{}  n1)
                                                                                                                                                                \mwedge{}  (n1  |  n))])
                  \mvee{}  (\mneg{}(\mexists{}i:\{m  -  b..m\msupminus{}\}.  (\muparrow{}isl(divisor-test(n;(i  *  m)  +  1;(i  *  m)  +  m)))))))
7.  proper-divisor-aux(n;m;m;1;m)  \mmember{}  (\mexists{}n1:\mBbbZ{}  [(n1  <  n  \mwedge{}  (2  \mleq{}  n1)  \mwedge{}  (n1  |  n))])
      \mvee{}  (\mneg{}(\mexists{}i:\mBbbN{}m.  (\muparrow{}isl(divisor-test(n;(i  *  m)  +  1;(i  *  m)  +  m)))))
8.  proper-divisor-aux(n;m;m;1;m)  =  proper-divisor-aux(n;m;m;1;m)
\mvdash{}  ((\mexists{}n1:\mBbbZ{}  [(n1  <  n  \mwedge{}  (2  \mleq{}  n1)  \mwedge{}  (n1  |  n))])
        \mvee{}  (\mneg{}(\mexists{}i:\mBbbN{}m.  (\muparrow{}isl(divisor-test(n;(i  *  m)  +  1;(i  *  m)  +  m))))))  \msubseteq{}r  Dec(\mexists{}n1:\mBbbZ{}  [(n1  <  n
                                                                                                                                                                \mwedge{}  (2  \mleq{}  n1)
                                                                                                                                                                \mwedge{}  (n1  |  n))])


By

---

Latex:
(RepUR  ``or  decidable``  0
  THEN  GenConclAtAddr  [1;1]
  THEN  Auto
  THEN  Try  (OnMaybeHyp  6  (\mbackslash{}h.  (InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  h\mcdot{}  THEN  Complete  (Auto')))\mcdot{}))

---

Home Index