Step * 2 1 of Lemma decidable__proper_divisor

.....assertion..... 
1. {2...}
2. ¬(n ≤ 5)
3. : ℕ
4. (iroot(4;n) 1) ∈ ℕ
⊢ (m m) 1 < n ∧ n < (m m) m
BY
(InstLemma `iroot-property` [⌜4⌝;⌜n⌝]⋅ THEN Auto) }

1
1. {2...}
2. ¬(n ≤ 5)
3. : ℕ
4. (iroot(4;n) 1) ∈ ℕ
5. iroot(4;n)^4 ≤ n
6. n < (iroot(4;n) 1)^4
⊢ (m m) 1 < n

2
1. {2...}
2. ¬(n ≤ 5)
3. : ℕ
4. (iroot(4;n) 1) ∈ ℕ
5. iroot(4;n)^4 ≤ n
6. n < (iroot(4;n) 1)^4
7. (m m) 1 < n
⊢ n < (m m) m


Latex:


Latex:
.....assertion..... 
1.  n  :  \{2...\}
2.  \mneg{}(n  \mleq{}  5)
3.  m  :  \mBbbN{}
4.  m  =  (iroot(4;n)  +  1)
\mvdash{}  (m  *  m)  +  1  <  n  \mwedge{}  n  <  (m  *  m)  *  m  *  m


By


Latex:
(InstLemma  `iroot-property`  [\mkleeneopen{}4\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)




Home Index