---

Step * 2 2 1 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. c : ℤ
10. n = (x * c) ∈ ℤ
⊢ False
BY
{ ((CaseNat 1 `n' THENL [(HypSubst' (-1) (-2) THEN D -2 THEN Auto); PromoteHyp (-1) 2])
   THEN (CaseNat 2 `n' THENL [(HypSubst' (-1) (-2) THEN D -2 THEN Auto); PromoteHyp (-1) 2])
   THEN (CaseNat 3 `n' THENL [HypSubst' (-1) (-2); Auto])⋅)⋅ }

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 ∈ ℤ
⊢ 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.  c  :  \mBbbZ{}
10.  n  =  (x  *  c)
\mvdash{}  False


By

---

Latex:
((CaseNat  1  `n'  THENL  [(HypSubst'  (-1)  (-2)  THEN  D  -2  THEN  Auto);  PromoteHyp  (-1)  2])
  THEN  (CaseNat  2  `n'  THENL  [(HypSubst'  (-1)  (-2)  THEN  D  -2  THEN  Auto);  PromoteHyp  (-1)  2])
  THEN  (CaseNat  3  `n'  THENL  [HypSubst'  (-1)  (-2);  Auto])\mcdot{})\mcdot{}

---

Home Index