Step
*
1
1
1
1
2
of Lemma
proper-divisor-aux_wf
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 ∈ ℤ)
12. y : gcd(n;iseg_product((m * (m - b)) + 1;m * ((m - b) + 1))) = 1 ∈ ℤ@i
13. divisor-test(n;(m * (m - b)) + 1;m * ((m - b) + 1))
= (inr y )
∈ ({n1:ℤ| n1 < n ∧ (2 ≤ n1) ∧ (n1 | n)}  ∨ (gcd(n;iseg_product((m * (m - b)) + 1;m * ((m - b) + 1))) = 1 ∈ ℤ))
⊢ eval j' = m * ((m - b - 1) + 1) 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)
BY
{ (Enough to prove ((∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])
                     ∨ (¬(∃i:{m - b - 1..m-}. (↑isl(divisor-test(n;(i * m) + 1;(i * m) + m))))))
                     ⊆r (∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))] + ((∃i:{m - b..m-}
                                                                     (↑isl(divisor-test(n;(i * m) + 1;(i * m) + m))))
                                                                  ⟶ False))
    Because 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 ∈ ℤ)
12. y : gcd(n;iseg_product((m * (m - b)) + 1;m * ((m - b) + 1))) = 1 ∈ ℤ@i
13. divisor-test(n;(m * (m - b)) + 1;m * ((m - b) + 1))
= (inr y )
∈ ({n1:ℤ| n1 < n ∧ (2 ≤ n1) ∧ (n1 | n)}  ∨ (gcd(n;iseg_product((m * (m - b)) + 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))))))
    ⊆r (∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))] + ((∃i:{m - b..m-}. (↑isl(divisor-test(n;(i * m) + 1;(i * m) + m))))
                                                 ⟶ False))
Latex:
Latex:
1.  n  :  \mBbbN{}\msupplus{}
2.  m  :  \mBbbN{}
3.  n  <  (m  *  m)  *  m  *  m
4.  m  *  m  <  n
5.  1  <  m
6.  \mforall{}i:\mBbbN{}m.  ((0  \mleq{}  (i  *  m))  \mwedge{}  (i  *  m)  +  m  <  n)
7.  b  :  \mBbbZ{}
8.  0  <  b
9.  ((b  -  1)  \mleq{}  m)
{}\mRightarrow{}  (proper-divisor-aux(n;m;b  -  1;(m  *  (m  -  b  -  1))  +  1;m  *  ((m  -  b  -  1)  +  1))  \mmember{}  (\mexists{}n1:\mBbbZ{}  [(n1  <  n
                                                                                                                                                                              \mwedge{}  (2  \mleq{}  n1)
                                                                                                                                                                              \mwedge{}  (n1  |  n))])
        \mvee{}  (\mneg{}(\mexists{}i:\{m  -  b  -  1..m\msupminus{}\}.  (\muparrow{}isl(divisor-test(n;(i  *  m)  +  1;(i  *  m)  +  m))))))
10.  b  \mleq{}  m
11.  \mneg{}(b  =  0)
12.  y  :  gcd(n;iseg\_product((m  *  (m  -  b))  +  1;m  *  ((m  -  b)  +  1)))  =  1@i
13.  divisor-test(n;(m  *  (m  -  b))  +  1;m  *  ((m  -  b)  +  1))  =  (inr  y  )
\mvdash{}  eval  j'  =  m  *  ((m  -  b  -  1)  +  1)  in
    eval  i'  =  (m  *  (m  -  b  -  1))  +  1  in
    eval  b'  =  b  -  1  in
        proper-divisor-aux(n;m;b';i';j')
    \mmember{}  \mexists{}n1:\mBbbZ{}  [(n1  <  n  \mwedge{}  (2  \mleq{}  n1)  \mwedge{}  (n1  |  n))]  +  ((\mexists{}i:\{m  -  b..m\msupminus{}\}
                                                                                                (\muparrow{}isl(divisor-test(n;(i  *  m)  +  1;(i  *  m)  +  m))))
                                                                                          {}\mrightarrow{}  False)
By
Latex:
(Enough  to  prove  ((\mexists{}n1:\mBbbZ{}  [(n1  <  n  \mwedge{}  (2  \mleq{}  n1)  \mwedge{}  (n1  |  n))])
                                      \mvee{}  (\mneg{}(\mexists{}i:\{m  -  b  -  1..m\msupminus{}\}.  (\muparrow{}isl(divisor-test(n;(i  *  m)  +  1;(i  *  m)  +  m))))))
                                      \msubseteq{}r  (\mexists{}n1:\mBbbZ{}  [(n1  <  n  \mwedge{}  (2  \mleq{}  n1)  \mwedge{}  (n1  |  n))]  +  ((\mexists{}i:\{m  -  b..m\msupminus{}\}
                                                                                                                                      (\muparrow{}isl(divisor-test(n;(i  *  m)
                                                                                                                                      +  1;(i  *  m)  +  m))))  {}\mrightarrow{}  False))
    Because  Auto)
Home
Index