Step
*
2
2
2
1
2
1
1
1
1
of Lemma
iroot-lemma
.....assertion.....
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. iroot(n;(a + k) * y^n) < M * y
12. (iroot(n;(a + k) * y^n)^n ≤ ((a + k) * y^n)) ∧ (a + k) * y^n < (iroot(n;(a + k) * y^n) + 1)^n
13. ((n * b) * (iroot(n;(a + k) * y^n) + 1)^(n - 1)) ≤ ((n * b) * (M * y)^(n - 1))
⊢ (iroot(n;(a + k) * y^n) + 1)^n ≤ (((iroot(n;(a + k) * y^n) ÷ b) * b)^n
+ (n * b * (iroot(n;(a + k) * y^n) + 1)^(n - 1)))
BY
{ (GenConclAtAddrType ⌜ℕ⌝ [1;1;1]⋅ THEN Auto) }
1
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. iroot(n;(a + k) * y^n) < M * y
12. iroot(n;(a + k) * y^n)^n ≤ ((a + k) * y^n)
13. (a + k) * y^n < (iroot(n;(a + k) * y^n) + 1)^n
14. ((n * b) * (iroot(n;(a + k) * y^n) + 1)^(n - 1)) ≤ ((n * b) * (M * y)^(n - 1))
15. v : ℕ
16. iroot(n;(a + k) * y^n) = v ∈ ℕ
⊢ (v + 1)^n ≤ (((v ÷ b) * b)^n + (n * b * (v + 1)^(n - 1)))
Latex:
Latex:
.....assertion.....
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. iroot(n;(a + k) * y\^{}n) < M * y
12. (iroot(n;(a + k) * y\^{}n)\^{}n \mleq{} ((a + k) * y\^{}n)) \mwedge{} (a + k) * y\^{}n < (iroot(n;(a + k) * y\^{}n) + 1)\^{}n
13. ((n * b) * (iroot(n;(a + k) * y\^{}n) + 1)\^{}(n - 1)) \mleq{} ((n * b) * (M * y)\^{}(n - 1))
\mvdash{} (iroot(n;(a + k) * y\^{}n) + 1)\^{}n \mleq{} (((iroot(n;(a + k) * y\^{}n) \mdiv{} b) * b)\^{}n
+ (n * b * (iroot(n;(a + k) * y\^{}n) + 1)\^{}(n - 1)))
By
Latex:
(GenConclAtAddrType \mkleeneopen{}\mBbbN{}\mkleeneclose{} [1;1;1]\mcdot{} THEN Auto)
Home
Index