the integer one divides all integers

Johan G. F. Belinfante
2006 December 18

SetDirectory["l:"];  << goedel88.18a; << tools.m

summary

In this notebook it is shown that every integer is divisible by the integer +1 (= plus[set[0]] = composite[id[omega], SUCC]).  To make sense of what is going on here, one must understand that the integer divisibibility relation INTDIV has been defined as the union of all endomorphisms of INTADD.  At this point, the theoy of multiplication for integers has not yet been developed, and indeed the result derived here is needed for that development.

derivation

By definition, the integer divisibility relation is:

U[binhom[INTADD, INTADD]]

Since the sum of two endomorphisms is another, the integer divisibility relation satisfies a corresponding property:

ImageComp[cross[inverse[DUP], INTADD], inverse[E], 
        image[CROSS, cart[binhom[INTADD, INTADD], binhom[INTADD, INTADD]]]] // 
      Reverse

composite[INTADD, 
        intersection[composite[inverse[FIRST], INTDIV], 
          composite[inverse[SECOND], INTDIV]]] := INTDIV

Corollary.  The set image[INTDIV,set[x]] of integers divisible by x is closed under addition.

ImageComp[composite[INTADD, cross[INTDIV, INTDIV]], DUP, set[x]] // 
      Reverse

image[INTADD, cart[image[INTDIV, set[x_]], image[INTDIV, set[x_]]]] := 
      image[INTDIV, set[x]]

Lemma.

SubstTest[member, pair[x, x], composite[Id, w], 
      w -> INTDIV]

and[member[x_, V], member[pair[x_, x_], INTDIV]] := 
      member[pair[x, x], INTDIV]

Theorem.  Every integer is divible by itself.

(member[x, fix[y]] // AssertTest // Reverse) /. 
      y -> INTDIV

member[pair[x_, x_], INTDIV] := member[x, Z]

A form of induction suitable for integers is applied to the class of integers divisible by one.

SubstTest[implies, 
        and[member[composite[id[omega], SUCC], x], 
          subclass[image[INTADD, cart[x, x]], x], 
          subclass[image[INVERSE, x], x]], subclass[Z, x], 
        x -> image[INTDIV, set[plus[set[0]]]]] // Reverse

% /. Equal -> SetDelayed

Theorem.  Every integer is divisible by +1.

SubstTest[and, subclass[u, v], 
      subclass[v, u], {u -> Z, 
        v -> image[INTDIV, set[composite[id[omega], SUCC]]]}]

image[INTDIV, set[composite[id[omega], SUCC]]] := Z