---

Step * 2 of Lemma decidable__proper_divisor


1. n : {2...}
2. ¬(n ≤ 5)
⊢ Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])
BY
{ ((Evaluate ⌜m = (iroot(4;n) + 1) ∈ ℕ⌝⋅ THENA Auto) THEN Assert ⌜(m * m) + 1 < n ∧ n < (m * m) * m * m⌝⋅) }

1
.....assertion..... 
1. n : {2...}
2. ¬(n ≤ 5)
3. m : ℕ
4. m = (iroot(4;n) + 1) ∈ ℕ
⊢ (m * m) + 1 < n ∧ n < (m * m) * m * m

2
1. n : {2...}
2. ¬(n ≤ 5)
3. m : ℕ
4. m = (iroot(4;n) + 1) ∈ ℕ
5. (m * m) + 1 < n ∧ n < (m * m) * m * m
⊢ Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])

---

Latex:

---

Latex:

1.  n  :  \{2...\}
2.  \mneg{}(n  \mleq{}  5)
\mvdash{}  Dec(\mexists{}n1:\mBbbZ{}  [(n1  <  n  \mwedge{}  (2  \mleq{}  n1)  \mwedge{}  (n1  |  n))])


By

---

Latex:
((Evaluate  \mkleeneopen{}m  =  (iroot(4;n)  +  1)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Assert  \mkleeneopen{}(m  *  m)  +  1  <  n  \mwedge{}  n  <  (m  *  m)  *  m  *  m\mkleeneclose{}\mcdot{})

---

Home Index