Step * 1 1 1 1 1 of Lemma proper-divisor-aux_wf


1. : ℕ+
2. : ℕ
3. n < (m m) m
4. m < n
5. 1 < m
6. ∀i:ℕm. ((0 ≤ (i m)) ∧ (i m) m < n)
7. : ℤ
8. 0 < b
9. ((b 1) ≤ m)
 (proper-divisor-aux(n;m;b 1;(m (m 1)) 1;m ((m 1) 1)) ∈ (∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 n))])
    ∨ (∃i:{m 1..m-}. (↑isl(divisor-test(n;(i m) 1;(i m) m))))))
10. b ≤ m
11. ¬(b 0 ∈ ℤ)
12. {n1:ℤn1 < n ∧ (2 ≤ n1) ∧ (n1 n)} @i
13. divisor-test(n;(m (m b)) 1;m ((m b) 1))
(inl x)
∈ ({n1:ℤn1 < n ∧ (2 ≤ n1) ∧ (n1 n)}  ∨ (gcd(n;iseg_product((m (m b)) 1;m ((m b) 1))) 1 ∈ ℤ))
⊢ inl x ∈ ∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 n))] ((∃i:{m b..m-}. (↑isl(divisor-test(n;(i m) 1;(i m) m))))
                                                   ⟶ False)
BY
TACTIC:(TACTIC:MemCD THEN Auto THEN InstHyp [⌜i⌝6⋅ THEN Auto') }


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.  x  :  \{n1:\mBbbZ{}|  n1  <  n  \mwedge{}  (2  \mleq{}  n1)  \mwedge{}  (n1  |  n)\}  @i
13.  divisor-test(n;(m  *  (m  -  b))  +  1;m  *  ((m  -  b)  +  1))  =  (inl  x)
\mvdash{}  inl  x  \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:
TACTIC:(TACTIC:MemCD  THEN  Auto  THEN  InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  6\mcdot{}  THEN  Auto')




Home Index