---

Step * 2 2 1 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 ∈ ℤ
14. x | 3
⊢ False
BY
{ ((Subst ⌜x ~ 2⌝ (-1)⋅ THEN Auto) THEN (FLemma `divides_iff_div_exact` [-1] THENA Auto) THEN Reduce (-1) THEN Auto)⋅ }

---

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
14.  x  |  3
\mvdash{}  False


By

---

Latex:
((Subst  \mkleeneopen{}x  \msim{}  2\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)
  THEN  (FLemma  `divides\_iff\_div\_exact`  [-1]  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Auto)\mcdot{}

---

Home Index