Step
*
of Lemma
rroot-regularity-lemma
∀[k:{2...}]. ∀[n,m:ℕ+]. ∀[a,b,c,d:ℤ].
(((m ≤ a) ∨ ((a = 0 ∈ ℤ) ∧ (c = 0 ∈ ℤ)))
⇒ ((n ≤ b) ∨ ((b = 0 ∈ ℤ) ∧ (d = 0 ∈ ℤ)))
⇒ (a^k ≤ c)
⇒ c < a + m^k
⇒ (b^k ≤ d)
⇒ d < b + n^k
⇒ (|c - d| ≤ (2^k * (n^k + m^k)))
⇒ (|a - b| ≤ (2 * (n + m))))
BY
{ Assert ⌜∀[k:{2...}]. ∀[n,m:ℕ+]. ∀[a,b,c,d:ℤ].
((a ≤ b)
⇒ ((m ≤ a) ∨ ((a = 0 ∈ ℤ) ∧ (c = 0 ∈ ℤ)))
⇒ ((n ≤ b) ∨ ((b = 0 ∈ ℤ) ∧ (d = 0 ∈ ℤ)))
⇒ (a^k ≤ c)
⇒ c < a + m^k
⇒ (b^k ≤ d)
⇒ d < b + n^k
⇒ (|c - d| ≤ (2^k * (n^k + m^k)))
⇒ (|a - b| ≤ (2 * (n + m))))⌝⋅ }
1
.....assertion.....
∀[k:{2...}]. ∀[n,m:ℕ+]. ∀[a,b,c,d:ℤ].
((a ≤ b)
⇒ ((m ≤ a) ∨ ((a = 0 ∈ ℤ) ∧ (c = 0 ∈ ℤ)))
⇒ ((n ≤ b) ∨ ((b = 0 ∈ ℤ) ∧ (d = 0 ∈ ℤ)))
⇒ (a^k ≤ c)
⇒ c < a + m^k
⇒ (b^k ≤ d)
⇒ d < b + n^k
⇒ (|c - d| ≤ (2^k * (n^k + m^k)))
⇒ (|a - b| ≤ (2 * (n + m))))
2
1. ∀[k:{2...}]. ∀[n,m:ℕ+]. ∀[a,b,c,d:ℤ].
((a ≤ b)
⇒ ((m ≤ a) ∨ ((a = 0 ∈ ℤ) ∧ (c = 0 ∈ ℤ)))
⇒ ((n ≤ b) ∨ ((b = 0 ∈ ℤ) ∧ (d = 0 ∈ ℤ)))
⇒ (a^k ≤ c)
⇒ c < a + m^k
⇒ (b^k ≤ d)
⇒ d < b + n^k
⇒ (|c - d| ≤ (2^k * (n^k + m^k)))
⇒ (|a - b| ≤ (2 * (n + m))))
⊢ ∀[k:{2...}]. ∀[n,m:ℕ+]. ∀[a,b,c,d:ℤ].
(((m ≤ a) ∨ ((a = 0 ∈ ℤ) ∧ (c = 0 ∈ ℤ)))
⇒ ((n ≤ b) ∨ ((b = 0 ∈ ℤ) ∧ (d = 0 ∈ ℤ)))
⇒ (a^k ≤ c)
⇒ c < a + m^k
⇒ (b^k ≤ d)
⇒ d < b + n^k
⇒ (|c - d| ≤ (2^k * (n^k + m^k)))
⇒ (|a - b| ≤ (2 * (n + m))))
Latex:
Latex:
\mforall{}[k:\{2...\}]. \mforall{}[n,m:\mBbbN{}\msupplus{}]. \mforall{}[a,b,c,d:\mBbbZ{}].
(((m \mleq{} a) \mvee{} ((a = 0) \mwedge{} (c = 0)))
{}\mRightarrow{} ((n \mleq{} b) \mvee{} ((b = 0) \mwedge{} (d = 0)))
{}\mRightarrow{} (a\^{}k \mleq{} c)
{}\mRightarrow{} c < a + m\^{}k
{}\mRightarrow{} (b\^{}k \mleq{} d)
{}\mRightarrow{} d < b + n\^{}k
{}\mRightarrow{} (|c - d| \mleq{} (2\^{}k * (n\^{}k + m\^{}k)))
{}\mRightarrow{} (|a - b| \mleq{} (2 * (n + m))))
By
Latex:
Assert \mkleeneopen{}\mforall{}[k:\{2...\}]. \mforall{}[n,m:\mBbbN{}\msupplus{}]. \mforall{}[a,b,c,d:\mBbbZ{}].
((a \mleq{} b)
{}\mRightarrow{} ((m \mleq{} a) \mvee{} ((a = 0) \mwedge{} (c = 0)))
{}\mRightarrow{} ((n \mleq{} b) \mvee{} ((b = 0) \mwedge{} (d = 0)))
{}\mRightarrow{} (a\^{}k \mleq{} c)
{}\mRightarrow{} c < a + m\^{}k
{}\mRightarrow{} (b\^{}k \mleq{} d)
{}\mRightarrow{} d < b + n\^{}k
{}\mRightarrow{} (|c - d| \mleq{} (2\^{}k * (n\^{}k + m\^{}k)))
{}\mRightarrow{} (|a - b| \mleq{} (2 * (n + m))))\mkleeneclose{}\mcdot{}
Home
Index