Definition 88 · Theorems 422–429
In this section p and q stand for whole numbers, positive, 0 or negative.
Definition 88 (Landau 71). xᵖ is Π[1..p] x for p > 0 (the product of p factors each x). For x ≠ o it is e when p = 0, and e/x^|p| when p < 0.
So xᵖ is defined except when x = o and p ≦ 0. For x ≠ o and p < 0, x^|p| ≠ o by Theorem 421, so the quotient has sense.
A power is a reflexive operation: the operand taken as its own multiplier. The exponent counts how many times. It is a count (or, when negative or 0, a whole derived number), and is not itself raised from the operand.
Theorem 422 (Landau 290). If x ≠ o, then xᵖ ≠ o.
For p > 0, Theorem 421. For p = 0, e ≠ o. For p < 0, xᵖ • x^|p| = e ≠ o, so xᵖ ≠ o by Theorem 353.
Theorem 423 (Landau 291). x¹ = x.
Π[1..1] x = x, by Theorem 409.
Theorem 424 (Landau 292). Let p > 0, or let x ≠ o and y ≠ o. Then (x • y)ᵖ = xᵖ • yᵖ.
Proof: For p > 0, Theorem 414 with ∗ as •. For p = 0, e = e • e. For p < 0, by the first case and Theorem 379,
(x • y)ᵖ = e/(x • y)^|p| = (e • e)/(x^|p| • y^|p|) = (e/x^|p|) • (e/y^|p|) = xᵖ • yᵖ.
Theorem 425 (Landau 293). eᵖ = e.
By Theorem 424, eᵖ • e = eᵖ = (e • e)ᵖ = eᵖ • eᵖ. So eᵖ • (eᵖ − e) = o. Since eᵖ ≠ o (Theorem 422), eᵖ − e = o.
Theorem 426 (Landau 294). Let p > 0 and q > 0, or let x ≠ o. Then xᵖ • x^q = x^(p+q).
Proof: (1) p > 0 and q > 0. By Theorem 413 with ∗ as •, Π[1..p+q] x = Π[1..p] x • Π[1..q] x.
For the rest let x ≠ o.
(2) p = 0 or q = 0. e • x^q = x^q, and likewise.
(3) p > 0 and q < 0. Let r = |q|. Then xᵖ • x^q = xᵖ • (e/x^r) = xᵖ/x^r by Theorem 376. If p > r: xᵖ = x^(p−r) • x^r by (1), so xᵖ/x^r = x^(p−r) by Theorem 373. If p = r: xᵖ/xᵖ = e = x⁰. If p < r: x^r = x^(r−p) • xᵖ by (1), so xᵖ/x^r = (e • xᵖ)/(x^(r−p) • xᵖ) = e/x^(r−p) = x^(p−r), by Theorem 378 and Definition 88. In each case the exponent is p + q.
(4) p < 0 and q > 0. By (3) and Theorem 352.
(5) p < 0 and q < 0. xᵖ • x^q = (e/x^|p|) • (e/x^|q|) = e/(x^|p| • x^|q|) = e/x^(|p|+|q|) = x^(p+q), by Theorem 379 and (1), since |p + q| = |p| + |q|.
Theorem 427 (Landau 295). If x ≠ o, then xᵖ/x^q = x^(p−q).
By Theorem 426, x^(p−q) • x^q = xᵖ, and x^q ≠ o by Theorem 422.
Theorem 428 (Landau 296). If x ≠ o, then e/xᵖ = x^(−p).
e/xᵖ = x⁰/xᵖ = x^(0−p).
Theorem 429 (Landau 297). Let p > 0 and q > 0, or let x ≠ o. Then (xᵖ)^q = x^(p•q).
Proof: (1) x = o, p > 0, q > 0. By Theorem 421, oᵖ = o, o^q = o and o^(p•q) = o.
(2) x ≠ o, so xᵖ ≠ o. For q > 0, by induction on q: (xᵖ)¹ = xᵖ; and if it holds for q, then by Theorem 426, (xᵖ)^(q+1) = (xᵖ)^q • xᵖ = x^(p•q) • xᵖ = x^(p•q+p) = x^(p•(q+1)). For q = 0: (xᵖ)⁰ = e = x⁰. For q < 0: by the first case and Theorem 428, (xᵖ)^q = e/(xᵖ)^|q| = e/x^(p•|q|) = x^(−(p•|q|)) = x^(p•q).