---

Step * of Lemma proper-divisor-aux_wf

No Annotations
∀[n:ℕ+]. ∀[m:ℕ].
  (proper-divisor-aux(n;m;m;1;m) ∈ Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])) supposing 
     (m * m < n and 
     n < (m * m) * m * m)
BY
{ TACTIC:(Auto
          THEN (Assert 1 < m ∧ (∀i:ℕm. ((0 ≤ (i * m)) ∧ (i * m) + m < n)) BY
                      (Auto
                       THEN Try ((InstLemma `mul_bounds_1a` [⌜i⌝;⌜m⌝]⋅
                                  THEN Auto'
                                  THEN InstLemma `mul_preserves_le` [⌜i⌝;⌜m - 1⌝;⌜m⌝]⋅
                                  THEN Auto'))
                       THEN (CaseNat
                             0 `m'⋅
                             THENL [(HypSubst' (-1) 3 THEN Reduce 3 THEN Auto)
                                   ; (CaseNat 1 `m' THENL [(HypSubst' (-1) 3 THEN Reduce 3 THEN Auto); Auto])]
                       )⋅))
          THEN Assert ⌜∀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)))))))⌝⋅) }

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

2
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)))))))
⊢ proper-divisor-aux(n;m;m;1;m) ∈ Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[m:\mBbbN{}].
    (proper-divisor-aux(n;m;m;1;m)  \mmember{}  Dec(\mexists{}n1:\mBbbZ{}  [(n1  <  n  \mwedge{}  (2  \mleq{}  n1)  \mwedge{}  (n1  |  n))]))  supposing 
          (m  *  m  <  n  and 
          n  <  (m  *  m)  *  m  *  m)


By

---

Latex:
TACTIC:(Auto
                THEN  (Assert  1  <  m  \mwedge{}  (\mforall{}i:\mBbbN{}m.  ((0  \mleq{}  (i  *  m))  \mwedge{}  (i  *  m)  +  m  <  n))  BY
                                        (Auto
                                          THEN  Try  ((InstLemma  `mul\_bounds\_1a`  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}
                                                                THEN  Auto'
                                                                THEN  InstLemma  `mul\_preserves\_le`  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}m  -  1\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}
                                                                THEN  Auto'))
                                          THEN  (CaseNat
                                                      0  `m'\mcdot{}
                                                      THENL  [(HypSubst'  (-1)  3  THEN  Reduce  3  THEN  Auto)
                                                                  ;  (CaseNat  1  `m'
                                                                        THENL  [(HypSubst'  (-1)  3  THEN  Reduce  3  THEN  Auto);  Auto]
                                                                  )]
                                          )\mcdot{}))
                THEN  Assert  \mkleeneopen{}\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)))))))\mkleeneclose{}
                \mcdot{})

---

Home Index