THEOREM

*******

 

ALL(a):[a e n => [~a=0 => 0^a=0]]

 

By Dan Christensen

October 2013

 

(This proof was written with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com )

 

 

BASIC PRINCIPLES OF ARITHMETIC USED

***********************************

 

n is a set (the set of natural numbers)

 

1     Set(n)

      Axiom

 

+ is a binary function on n

 

2     ALL(a):ALL(b):[a e n & b e n => a+b e n]

      Axiom

 

* is a binary function on n

 

3     ALL(a):ALL(b):[a e n & b e n => a*b e n]

      Axiom

 

4     0 e n

      Axiom

 

5     1 e n

      Axiom

 

6     ALL(a):[a e n => a*0=0]

      Axiom

 

Existence of a predecessor

 

7     ALL(a):[a e n => [~a=0 => EXIST(b):[b e n & b+1=a]]]

      Axiom

 

 

Define: ^  (0^0 is an uspecified natural number)

*********

 

8     ALL(a):ALL(b):[a e n & b e n => a^b e n]

     & ALL(a):[a e n => [~a=0 => a^0=1]]

     & ALL(a):ALL(b):[a e n & b e n => a^(b+1)=a^b*a]

      Premise

 

9     ALL(a):ALL(b):[a e n & b e n => a^b e n]

      Split, 8

 

10    ALL(a):[a e n => [~a=0 => a^0=1]]

      Split, 8

 

11    ALL(a):ALL(b):[a e n & b e n => a^(b+1)=a^b*a]

      Split, 8

 

    

     PROOF

     *****

    

     Prove: ALL(a):[a e n => [~a=0 => 0^a=0]]

    

     Suppose...

 

      12    y e n

            Premise

 

         

          Prove: ~y=0 => 0^y=0

         

          Suppose...

 

            13    ~y=0

                  Premise

 

            14    0^y=0^y

                  Reflex

 

          Apply Existence of Predecessor

 

            15    y e n => [~y=0 => EXIST(b):[b e n & b+1=y]]

                  U Spec, 7

 

            16    ~y=0 => EXIST(b):[b e n & b+1=y]

                  Detach, 15, 12

 

            17    EXIST(b):[b e n & b+1=y]

                  Detach, 16, 13

 

            18    z e n & z+1=y

                  E Spec, 17

 

          Define: z  (the predecessor of y)

 

            19    z e n

                  Split, 18

 

            20    z+1=y

                  Split, 18

 

            21    0^y=0^(z+1)

                  Substitute, 20, 14

 

          Apply definition of ^

 

            22    ALL(b):[0 e n & b e n => 0^(b+1)=0^b*0]

                  U Spec, 11

 

            23    0 e n & z e n => 0^(z+1)=0^z*0

                  U Spec, 22

 

            24    0 e n & z e n

                  Join, 4, 19

 

            25    0^(z+1)=0^z*0

                  Detach, 23, 24

 

            26    0^y=0^z*0

                  Substitute, 25, 21

 

            27    0^z e n => 0^z*0=0

                  U Spec, 6

 

          Apply definition of ^

 

            28    ALL(b):[0 e n & b e n => 0^b e n]

                  U Spec, 9

 

            29    0 e n & z e n => 0^z e n

                  U Spec, 28

 

            30    0^z e n

                  Detach, 29, 24

 

            31    0^z*0=0

                  Detach, 27, 30

 

            32    0^y=0

                  Substitute, 31, 26

 

     As Required:

 

      33    ~y=0 => 0^y=0

            4 Conclusion, 13

 

As Required:

 

34    ALL(a):[a e n => [~a=0 => 0^a=0]]

      4 Conclusion, 12