---

Step * of Lemma reducible-nat

∀n:ℤ. reducible(n) ⇒ (∃n1:ℕ. (n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))) supposing 2 ≤ n
BY
{ (Auto THEN D -1 THEN ExRepD) }

1
1. n : ℤ@i
2. 2 ≤ n
3. b : ℤ-o@i
4. c : ℤ-o@i
5. ¬(b ~ 1)@i
6. ¬(c ~ 1)@i
7. n = (b * c) ∈ ℤ@i
⊢ ∃n1:ℕ. (n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))

---

Latex:

---

Latex:
\mforall{}n:\mBbbZ{}.  reducible(n)  {}\mRightarrow{}  (\mexists{}n1:\mBbbN{}.  (n1  <  n  \mwedge{}  (2  \mleq{}  n1)  \mwedge{}  (n1  |  n)))  supposing  2  \mleq{}  n


By

---

Latex:
(Auto  THEN  D  -1  THEN  ExRepD)

---

Home Index