---

Step * 1 of Lemma proper-divisor-aux_wf

.....assertion..... 
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))
⊢ ∀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)))))))
BY
{ (InductionOnNat
   THEN Auto
   THEN RecUnfold `proper-divisor-aux` 0
   THEN RepUR ``or not implies`` 0
   THEN Try (OldAutoSplit)
   THEN Try (Complete ((Auto THEN D -1 THEN 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 : ℤ
8. 0 < b
9. ((b - 1) ≤ m)
⇒ (proper-divisor-aux(n;m;b - 1;(m * (m - b - 1)) + 1;m * ((m - b - 1) + 1)) ∈ (∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])
    ∨ (¬(∃i:{m - b - 1..m-}. (↑isl(divisor-test(n;(i * m) + 1;(i * m) + m))))))
10. b ≤ m
11. ¬(b = 0 ∈ ℤ)
⊢ case divisor-test(n;(m * (m - b)) + 1;m * ((m - b) + 1))
   of inl(x) =>
   inl x
   | inr(x) =>
   eval j' = (m * ((m - b) + 1)) + m in
   eval i' = (m * ((m - b) + 1)) + 1 in
   eval b' = b - 1 in
     proper-divisor-aux(n;m;b';i';j') ∈ ∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))] + ((∃i:{m - b..m-}
                                                                                    (↑isl(divisor-test(n;(i * m) + 1;(i
                                                                                    * m)
                                                                                    + m)))) ⟶ False)

---

Latex:

---

Latex:
.....assertion..... 
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))
\mvdash{}  \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)))))))


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  RecUnfold  `proper-divisor-aux`  0
  THEN  RepUR  ``or  not  implies``  0
  THEN  Try  (OldAutoSplit)
  THEN  Try  (Complete  ((Auto  THEN  D  -1  THEN  Auto'))))

---

Home Index