Step
*
1
1
1
1
of Lemma
exp-convex
1. a : ℕ
2. b : ℕ
3. c : ℕ
4. n : ℤ
5. 0 < n
6. |(a * a^n) - b * b^n| ≤ (c * c^n)
7. c < |a - b|
8. c^n < |a^n - b^n|
9. (|a - b| * |a^n - b^n|) ≤ |(imax(a;b) * imax(a^n;b^n)) - imin(a;b) * imin(a^n;b^n)|
⊢ |a^n - b^n| ≤ c^n
BY
{ xxxSubst' |(imax(a;b) * imax(a^n;b^n)) - imin(a;b) * imin(a^n;b^n)| ~ |(a * a^n) - b * b^n| -1xxx }
1
.....equality.....
1. a : ℕ
2. b : ℕ
3. c : ℕ
4. n : ℤ
5. 0 < n
6. |(a * a^n) - b * b^n| ≤ (c * c^n)
7. c < |a - b|
8. c^n < |a^n - b^n|
9. (|a - b| * |a^n - b^n|) ≤ |(imax(a;b) * imax(a^n;b^n)) - imin(a;b) * imin(a^n;b^n)|
⊢ |(imax(a;b) * imax(a^n;b^n)) - imin(a;b) * imin(a^n;b^n)| ~ |(a * a^n) - b * b^n|
2
1. a : ℕ
2. b : ℕ
3. c : ℕ
4. n : ℤ
5. 0 < n
6. |(a * a^n) - b * b^n| ≤ (c * c^n)
7. c < |a - b|
8. c^n < |a^n - b^n|
9. (|a - b| * |a^n - b^n|) ≤ |(a * a^n) - b * b^n|
⊢ |a^n - b^n| ≤ c^n
Latex:
Latex:
1. a : \mBbbN{}
2. b : \mBbbN{}
3. c : \mBbbN{}
4. n : \mBbbZ{}
5. 0 < n
6. |(a * a\^{}n) - b * b\^{}n| \mleq{} (c * c\^{}n)
7. c < |a - b|
8. c\^{}n < |a\^{}n - b\^{}n|
9. (|a - b| * |a\^{}n - b\^{}n|) \mleq{} |(imax(a;b) * imax(a\^{}n;b\^{}n)) - imin(a;b) * imin(a\^{}n;b\^{}n)|
\mvdash{} |a\^{}n - b\^{}n| \mleq{} c\^{}n
By
Latex:
xxxSubst' |(imax(a;b) * imax(a\^{}n;b\^{}n)) - imin(a;b) * imin(a\^{}n;b\^{}n)| \msim{} |(a * a\^{}n) - b * b\^{}n| -1xxx
Home
Index