monotonicity properties of exponentiation

Johan G. F. Belinfante
2007 January 18

SetDirectory["l:"]; << goedel89.13a; << tools.m

summary

In this notebook it is shown that for natural numbers, if m ≤ n, then  (m^p) ≤  (n^p), The converse holds if the power p is not zero,  If the base b is not zero and if  m ≤ n, then  (b^m) ≤  (b^n).  The converse holds if  b > 1.  The proofs use only cardinality arguments and the laws of exponents, and do not require the use of induction.  A key observation is that one can reduce inequalities to equations.  Note that the inequality m ≤ n holds if and only if one can write n as m plus some natural number, and that mumber is in fact n – m.

equal[nat[x], natadd[nat[y], natsub[nat[x], nat[y]]]]

fixed power

The monotonicity rule for fixed powers can be deduced most simply using a cardinality argument.

SubstTest[implies, subclass[fin[u], fin[v]], 
          subclass[card[fin[u]], 
            card[fin[v]]], {u -> map[nat[z], nat[y]], 
            v -> map[nat[z], nat[x]]}] // Reverse // 
      MapNotNot

or[member[nat[x_], nat[y_]], 
        not[member[natexp[nat[x_], nat[z_]], natexp[nat[y_], nat[z_]]]]] := 
      True

Conversely, one can show that if p is not zero and m < n, then  (m^p) < (n^p).  The proof also does not require the use of induction.  A lemma about mapping classes is needed:

SubstTest[and, subclass[u, v], 
      subclass[v, u], {u -> map[x, y], v -> map[x, z]}]

equal[map[x_, y_], map[x_, z_]] := 
      or[equal[0, x], equal[y, z], not[member[x, V]]]

Lemma.

SubstTest[implies, 
          and[subclass[u, v], member[v, FINITE], equal[card[u], card[v]]], 
          equal[u, v], {u -> map[nat[z], nat[x]], 
            v -> map[nat[z], nat[y]]}] // Reverse // 
      MapNotNot

(% /. {x -> x_, y -> y_, z -> z_}) /. 
      Equal -> SetDelayed

The rule of trichotomy is also needed to obtain the converse theorem:

Map[not, 
        SubstTest[and, implies[and[p1, p2], p3], implies[p1, p4], 
          implies[p4, p5], implies[and[p3, p5], p6], 
          not[implies[and[p1, p2], p6]], {p1 -> member[nat[x], nat[y]], 
            p2 -> not[equal[0, nat[z]]], 
            p3 -> 
              not[equal[natexp[nat[x], nat[z]], 
                  natexp[nat[y], nat[z]]]], 
p4 -> 
              not[member[nat[y], nat[x]]], 
            p5 -> not[
                member[natexp[nat[y], nat[z]], natexp[nat[x], nat[z]]]], 
            p6 -> member[natexp[nat[x], nat[z]], natexp[nat[y], nat[z]]]}]] // 
      Reverse

or[equal[0, nat[z_]], 
        member[natexp[nat[x_], nat[z_]], natexp[nat[y_], nat[z_]]], 
        not[member[nat[x_], nat[y_]]]] := True

fixed base b = 2

The special case that  m ≤ n implies  (2^m) ≤  (2^n) can also be deduced using a cardinality argument.

SubstTest[implies, subclass[fin[u], fin[v]], 
        subclass[card[fin[u]], card[fin[v]]], {u -> P[nat[y]], 
          v -> P[nat[x]]}] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Again, one can obtain a converse as follows.

SubstTest[implies, 
        and[subclass[u, v], member[v, FINITE], equal[card[u], card[v]]], 
        equal[u, v], {u -> P[nat[x]], v -> P[nat[y]]}] // 
      Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p1, p3], implies[p3, p4], 
          implies[and[p2, p4], p5], 
          not[implies[p1, p5]], {p1 -> member[nat[x], nat[y]], 
            p2 -> 
              not[equal[natexp[succ[set[0]], nat[x]], 
                  natexp[succ[set[0]], 
                    nat[y]]]], 
p3 -> 
              not[member[nat[y], nat[x]]], 
            p4 -> not[
                member[natexp[succ[set[0]], nat[y]], 
                  natexp[succ[set[0]], nat[x]]]], 
            p5 -> member[natexp[succ[set[0]], nat[x]], 
                natexp[succ[set[0]], nat[y]]]}]] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

These two results can be combined into a single rewrite rule.

equiv[
      member[natexp[succ[set[0]], nat[x]], natexp[succ[set[0]], nat[y]]], 
      member[nat[x], nat[y]]]

member[natexp[succ[set[0]], nat[x_]], natexp[succ[set[0]], nat[y_]]] := 
      member[nat[x], nat[y]]

general case of a fixed base

Theorem. If  m ≤ n, then  (b^m) |  (b^n).

SubstTest[implies, equal[nat[x], natadd[nat[w], nat[y]]], 
        member[pair[natexp[nat[z], nat[y]], natexp[nat[z], nat[x]]], DIV], 
        w -> natsub[nat[x], nat[y]]] // Reverse

or[member[nat[x_], nat[y_]], 
        member[pair[natexp[nat[z_], nat[y_]], natexp[nat[z_], nat[x_]]], 
          DIV]] := True

Lemma.

or[not[member[x, y]], not[member[pair[y, x], DIV]]] // 
      NotNotTest

or[not[member[x_, y_]], not[member[pair[y_, x_], DIV]]] := 
      or[equal[0, y], not[equal[0, x]], not[member[y, omega]]]

Corollary.  If  b is not zero and if  m ≤ n, then  (b^m) ≤  (b^n).

Map[not, 
        SubstTest[and, implies[p2, p3], implies[and[p1, p3], p4], 
          not[implies[and[p1, p2], p4]], {p1 -> not[empty[nat[x]]], 
            p2 -> subclass[nat[z], nat[y]], 
            p3 -> member[
                pair[natexp[nat[x], nat[z]], natexp[nat[x], nat[y]]], 
                DIV], 
p4 -> 
              subclass[natexp[nat[x], nat[z]], natexp[nat[x], nat[y]]]}]] // 
      Reverse

or[equal[0, nat[x_]], member[nat[y_], nat[z_]], 
        not[member[natexp[nat[x_], nat[y_]], natexp[nat[x_], nat[z_]]]]] := 
      True

Corollary.

SubstTest[or, equal[0, nat[w]], member[nat[x], nat[y]], 
        not[member[natexp[nat[w], nat[x]], natexp[nat[w], nat[y]]]], 
        w -> succ[nat[z]]] // Reverse

or[member[nat[x_], nat[y_]], 
        not[member[natexp[succ[nat[z_]], nat[x_]], 
            natexp[succ[nat[z_]], nat[y_]]]]] := True

converse

For the converse, one needs to exclude the case b =1.  It will be shown that if  b > 1 and m < n then  (b^m) <  (b^n).  This proof again does not require the use of induction.  This is known: if  b > 0 and m ≤ n, then  (b^m) ≤  (b^n).  What we want is an implication going in the opposite direction.  To begin, just replace x with its successor.  This yields:

SubstTest[implies, 
        and[not[equal[0, nat[w]]], subclass[nat[t], nat[y]]], 
        subclass[natexp[nat[w], nat[t]], natexp[nat[w], nat[y]]], 
        t -> succ[nat[x]]] // Reverse

(% /. {w -> w_, x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Lemma.

equiv[and[member[set[0], nat[w]], not[equal[0, nat[w]]]], 
      member[set[0], nat[w]]]

and[member[set[0], nat[w_]], not[equal[0, nat[w_]]]] := 
      member[set[0], nat[w]]

Theorem.  If  b > 1 then  (b^m) <  (b^(m + 1)), and conversely.

SubstTest[member, nat[t], natmul[nat[t], nat[w]], 
          t -> natexp[nat[w], nat[x]]] // MapNotNot // Reverse

member[natexp[nat[w_], nat[x_]], 
        natmul[nat[w_], natexp[nat[w_], nat[x_]]]] := 
      member[set[0], nat[w]]

A form of the transitive law is needed: if  (b^m) <  (b^(m + 1)) and  (b^(m + 1)) ≤  (b^n), then  (b^m) < (b^n).

SubstTest[implies, 
        and[member[nat[t], nat[u]], subclass[nat[u], nat[v]]], 
        member[nat[t], 
          nat[v]], 
{t -> natexp[nat[w], nat[x]], 
          u -> natexp[nat[w], succ[nat[x]]], 
          v -> natexp[nat[w], nat[y]]}] // Reverse

(% /. {w -> w_, x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Main theorem.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[and[p1, p4], p5], 
          implies[and[p2, p3], p4], 
          not[implies[and[p1, p3], p5]], {p1 -> member[set[0], nat[w]], 
            p2 -> not[equal[0, nat[w]]], 
            p3 -> member[nat[x], nat[y]], 
            p4 -> not[
                member[natexp[nat[w], nat[y]], 
                  natmul[nat[w], 
                    natexp[nat[w], nat[x]]]]], 
p5 -> 
              member[natexp[nat[w], nat[x]], natexp[nat[w], nat[y]]]}]] // 
      Reverse

or[member[natexp[nat[w_], nat[x_]], natexp[nat[w_], nat[y_]]], 
        not[member[nat[x_], nat[y_]]], not[member[set[0], nat[w_]]]] := 
      True

The hypothesis member[set[0],nat[w]] can be replaced with a double succ wrapper.  A natural number is greater than 1 if and only if it is the successor of the successor of some number.

SubstTest[implies, and[member[set[0], nat[t]], member[nat[x], nat[y]]], 
        member[natexp[nat[t], nat[x]], natexp[nat[t], nat[y]]], 
        t -> succ[succ[nat[w]]]] // Reverse

(% /. {w -> w_, x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

The converse also holds:

SubstTest[implies, 
        member[natexp[succ[nat[t]], nat[x]], natexp[succ[nat[t]], nat[y]]], 
        member[nat[x], nat[y]], t -> succ[nat[w]]] // Reverse

(% /. {w -> w_, x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Combining the two directions, one finds:

equiv[
      member[natexp[succ[succ[nat[w]]], nat[x]], 
        natexp[succ[succ[nat[w]]], nat[y]]], 
      member[nat[x], nat[y]]]

member[natexp[succ[succ[nat[w_]]], nat[x_]], 
        natexp[succ[succ[nat[w_]]], nat[y_]]] := 
      member[nat[x], nat[y]]

Comment.  The special case w = 0 was derived previously using a cardinality argument.