---

Step * 2 2 1 of Lemma proper-divisor_wf


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

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

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(xxx(Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)xxx  THEN  D  (-1)\mcdot{}  THEN  Auto)xxx

---

Home Index