---

Step * of Lemma decidable__proper_divisor

No Annotations
∀n:{2...}. Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])
BY
{ (Auto THEN (Decide n ≤ 5 THENA Auto)) }

1
1. n : {2...}
2. n ≤ 5
⊢ Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])

2
1. n : {2...}
2. ¬(n ≤ 5)
⊢ Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\{2...\}.  Dec(\mexists{}n1:\mBbbZ{}  [(n1  <  n  \mwedge{}  (2  \mleq{}  n1)  \mwedge{}  (n1  |  n))])


By

---

Latex:
(Auto  THEN  (Decide  n  \mleq{}  5  THENA  Auto))

---

Home Index