Step
*
2
2
2
1
1
1
1
of Lemma
iroot-lemma
1. a : ℕ
2. n : ℕ+
3. b : ℕ+
4. k : ℕ+
5. a + k ∈ ℕ+
6. M : ℕ+
7. a + k < M^n
8. y : ℕ+
9. (n * b * M^(n - 1)) ≤ (k * y)
10. (a + k) * y^n ∈ ℕ+
11. (M * y) ≤ iroot(n;(a + k) * y^n)
12. (M^n * y^n) ≤ ((a + k) * y^n)
⊢ iroot(n;(a + k) * y^n) < M * y
BY
{ (InstLemma `mul_preserves_lt` [⌜a + k⌝;⌜M^n⌝;⌜y^n⌝]⋅ THEN Auto) }
Latex:
Latex:
1. a : \mBbbN{}
2. n : \mBbbN{}\msupplus{}
3. b : \mBbbN{}\msupplus{}
4. k : \mBbbN{}\msupplus{}
5. a + k \mmember{} \mBbbN{}\msupplus{}
6. M : \mBbbN{}\msupplus{}
7. a + k < M\^{}n
8. y : \mBbbN{}\msupplus{}
9. (n * b * M\^{}(n - 1)) \mleq{} (k * y)
10. (a + k) * y\^{}n \mmember{} \mBbbN{}\msupplus{}
11. (M * y) \mleq{} iroot(n;(a + k) * y\^{}n)
12. (M\^{}n * y\^{}n) \mleq{} ((a + k) * y\^{}n)
\mvdash{} iroot(n;(a + k) * y\^{}n) < M * y
By
Latex:
(InstLemma `mul\_preserves\_lt` [\mkleeneopen{}a + k\mkleeneclose{};\mkleeneopen{}M\^{}n\mkleeneclose{};\mkleeneopen{}y\^{}n\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index