---

Step * 2 2 1 1 1 of Lemma proper-divisor_wf


1. n : ℕ+
2. ¬(n = 2 ∈ ℤ)
3. ¬(n = 1 ∈ ℤ)
4. y : Top
5. n < 5
6. ¬(n = 4 ∈ ℤ)
7. ∀n1:ℤ. (n1 < n ∧ (2 ≤ n1) ∧ (n1 | n) ∈ Type)
8. x : ℤ
9. x < n
10. 2 ≤ x
11. c : ℤ
12. 3 = (x * c) ∈ ℤ
13. n = 3 ∈ ℤ
⊢ False
BY
{ xxx(Assert x | 3 BY
            (With ⌜c⌝ (D 0)⋅ THEN Auto))xxx }

1
1. n : ℕ+
2. ¬(n = 2 ∈ ℤ)
3. ¬(n = 1 ∈ ℤ)
4. y : Top
5. n < 5
6. ¬(n = 4 ∈ ℤ)
7. ∀n1:ℤ. (n1 < n ∧ (2 ≤ n1) ∧ (n1 | n) ∈ Type)
8. x : ℤ
9. x < n
10. 2 ≤ x
11. c : ℤ
12. 3 = (x * c) ∈ ℤ
13. n = 3 ∈ ℤ
14. x | 3
⊢ False

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  \mneg{}(n  =  2)
3.  \mneg{}(n  =  1)
4.  y  :  Top
5.  n  <  5
6.  \mneg{}(n  =  4)
7.  \mforall{}n1:\mBbbZ{}.  (n1  <  n  \mwedge{}  (2  \mleq{}  n1)  \mwedge{}  (n1  |  n)  \mmember{}  Type)
8.  x  :  \mBbbZ{}
9.  x  <  n
10.  2  \mleq{}  x
11.  c  :  \mBbbZ{}
12.  3  =  (x  *  c)
13.  n  =  3
\mvdash{}  False


By

---

Latex:
xxx(Assert  x  |  3  BY
                    (With  \mkleeneopen{}c\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))xxx

---

Home Index