image[DIV, x] rules

Johan G. F. Belinfante and Ming Li
2007 January  27

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

summary

Rewrite rules are derived for the conditions equal[omega, image[DIV, x]] and member[x, image[DIV, y]].

member[x, image[DIV, y]] rules

Observation: The number x is a multiple of some member of y  if and only if some divisor of  x  belongs to y.

disjoint[image[inverse[DIV], set[x]], y]

When the divisors of a natural number are known, this rule can be turned around.  For example, the set of divisors of 0 is the set of all natural numbers.  Accordingly, one has:

Map[not, 
      SubstTest[disjoint, image[inverse[DIV], set[w]], x, 
        w -> 0]]

Comment.  An application of AssertTest suffices to derive this rewrite rule.

member[0, image[DIV, x]] // AssertTest

member[0, image[DIV, x_]] := 
      not[equal[0, intersection[omega, x]]]

The only divisor of  1  is itself.  Therefore, one has:

Map[not, 
      SubstTest[disjoint, image[inverse[DIV], set[w]], x, 
        w -> set[0]]]

Here again, one could also derive the same result using AssertTest.

member[set[0], image[DIV, x]] // AssertTest

member[set[0], image[DIV, x_]] := member[set[0], x]

Since 2 is a prime, its only divisors are 1 and 2.  (Comment. In this case AssertTest does not suffice.)

SubstTest[member, t, 
        complement[P[complement[image[inverse[DIV], set[y]]]]], 
        y -> succ[set[0]]] /. 
      t -> intersection[omega, x]

member[succ[set[0]], image[DIV, x_]] := 
      or[member[set[0], x], member[succ[set[0]], x]]

Lemma.  Since 3 is a prime, its only divisors are 1 and 3.  This can be made into a rewrite rule.

equal[image[inverse[DIV], set[succ[succ[set[0]]]]], 
      set[set[0], succ[succ[set[0]]]]]

image[inverse[DIV], set[succ[succ[set[0]]]]] := 
      set[set[0], succ[succ[set[0]]]]

Theorem.  The number 3 is a multiple of some member of x if and only if either 1 or 3 belongs to x.

SubstTest[member, t, 
        complement[P[complement[image[inverse[DIV], set[y]]]]], 
        y -> succ[succ[set[0]]]] /. 
      t -> intersection[omega, x]

member[succ[succ[set[0]]], image[DIV, x_]] := 
      or[member[set[0], x], member[succ[succ[set[0]]], x]]

More generally:  a prime x is a multiple of some member of y if and only if either 1 or x belongs to y.

SubstTest[implies, 
          and[equal[z, image[inverse[DIV], set[x]]], disjoint[y, z]], 
          not[member[x, image[DIV, y]]], z -> set[set[0], x]] // 
        Reverse // MapNotNot

or[member[x_, y_], member[set[0], y_], not[member[x_, PRIMES]], 
        not[member[x_, image[DIV, y_]]]] := True

equal[omega, image[DIV, x]]

Lemma.

SubstTest[implies, subclass[u, v], 
        subclass[image[w, u], image[w, v]], {u ->  set[set[0]] , 
          v -> x, w -> DIV}] // Reverse

(% /. x -> x_) /. Equal -> SetDelayed

Theorem.

SubstTest[and, implies[p, subclass[u, v]], 
      subclass[v, u], {p -> member[set[0], x], u -> omega, 
        v -> image[DIV, x]}]

(% /. x -> x_) /. Equal -> SetDelayed

Lemma.

SubstTest[implies, and[member[u, v], equal[v, w]], 
        member[u, w], 
{u -> set[0], v -> omega, 
          w -> image[DIV, x]}] // Reverse

(% /. x -> x_) /. Equal -> SetDelayed

Theorem.

equiv[equal[omega, image[DIV, x]], member[set[0], x]]

equal[omega, image[DIV, x_]] := member[set[0], x]

Corollary.

SubstTest[and, subclass[u, v], 
        subclass[v, u], {u -> omega, v -> image[DIV, x]}] // 
      Reverse

subclass[omega, image[DIV, x_]] := member[set[0], x]

variable-free formulations

Theorem.

image[inverse[IMAGE[DIV]], set[omega]] // Normality

image[inverse[IMAGE[DIV]], set[omega]] := 
      complement[P[complement[set[set[0]]]]]

Corollary

image[inverse[VERTSECT[DIV]], set[omega]] // Normality

image[inverse[VERTSECT[DIV]], set[omega]] := set[set[0]]