THEOREM

*******

 

Here, given some of the common rules of basic arithmetic (line 1-14) and the standard definitions of the even numbers

(line 15) and odd numbers (line 16) we formally prove that, for all even numbers, the next number will be an odd number.

 

ALL(a):[a e n => [Even(a) => Odd(a+1)]]  where n = the set of natural numbers

 

 

COROLLARY

*********

 

ALL(a):[a e n => Even(2*a) & Odd(2*a+1)]

 

 

By Dan Christensen

2022-05-26

http://www.dcproof.com

 

 

PROOF

*****

 

Basic Rules of Arithmetic Required  (derivable from Peano's Axioms)

 

Define: 0, 1, 2

 

1     0 e n

      Axiom

 

2     1 e n

      Axiom

 

3     ~1=0

      Axiom

 

4     2 e n

      Axiom

 

5     ~2=0

      Axiom

 

From Definition of +  (addition)

 

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

      Axiom

 

Properties of +

 

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

      Axiom

 

From Definition of *  (multiplication)

 

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

      Axiom

 

9     ~EXIST(a):[a e n & 2*a=1]

      Axiom

 

From Definition of - (subtraction)

 

10   ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a=c+b => a-b=c]]

      Axiom

 

11   ALL(a):ALL(b):[a e n & b e n => [b<a => a-b e n]]

      Axiom

 

Define: <

 

12   ALL(a):ALL(b):[a e n & b e n => [a<b <=> EXIST(c):[c e n & ~c=0 & a+c=b]]]

      Axiom

 

Properties of <

 

13   ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~a=0 => [a*b<a*c => b<c]]

      Axiom

 

14   ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [c<b => a*(b-c)=a*b-a*c]]

      Axiom

 

Define: Even

 

15   ALL(a):[a e n => [Even(a) <=> EXIST(b):[b e n & a=2*b]]]

      Axiom

 

Define: Odd

 

16   ALL(a):[Odd(a) <=> ~Even(a)]

      Axiom

 

   

    LEMMA

   

    Prove: ALL(a):[a e n => ~EXIST(b):[b e n & 2*a+1=2*b]]

   

    Suppose...

 

      17   x e n

            Premise

 

        

         Prove: ~EXIST(b):[b e n & 2*x+1=2*b]

        

         Suppose to the contrary...

 

            18   y e n & 2*x+1=2*y

                  Premise

 

            19   y e n

                  Split, 18

 

            20   2*x+1=2*y

                  Split, 18

 

         Prove: 2*y=2*x+1  by commutativity

        

         Apply definition of *

 

            21   ALL(b):[2 e n & b e n => 2*b e n]

                  U Spec, 8

 

            22   2 e n & x e n => 2*x e n

                  U Spec, 21

 

            23   2 e n & x e n

                  Join, 4, 17

 

            24   2*x e n

                  Detach, 22, 23

 

            25   2 e n & y e n => 2*y e n

                  U Spec, 21

 

            26   2 e n & y e n

                  Join, 4, 19

 

            27   2*y e n

                  Detach, 25, 26

 

            28   ALL(b):ALL(c):[2*y e n & b e n & c e n => [2*y=c+b => 2*y-b=c]]

                  U Spec, 10, 27

 

            29   ALL(c):[2*y e n & 2*x e n & c e n => [2*y=c+2*x => 2*y-2*x=c]]

                  U Spec, 28, 24

 

            30   2*y e n & 2*x e n & 1 e n => [2*y=1+2*x => 2*y-2*x=1]

                  U Spec, 29

 

            31   2*y e n & 2*x e n

                  Join, 27, 24

 

            32   2*y e n & 2*x e n & 1 e n

                  Join, 31, 2

 

            33   2*y=1+2*x => 2*y-2*x=1

                  Detach, 30, 32

 

         As Required:

 

            34   2*y=2*x+1

                  Sym, 20

 

         Apply commutativity of +

 

            35   ALL(b):[2*x e n & b e n => 2*x+b=b+2*x]

                  U Spec, 7, 24

 

            36   2*x e n & 1 e n => 2*x+1=1+2*x

                  U Spec, 35

 

            37   2*x e n & 1 e n

                  Join, 24, 2

 

            38   2*x+1=1+2*x

                  Detach, 36, 37

 

         As Required:

 

            39   2*y=1+2*x

                  Substitute, 38, 34

 

            40   2*y-2*x=1

                  Detach, 33, 39

 

         Apply property of <

 

            41   ALL(b):ALL(c):[2 e n & b e n & c e n => [c<b => 2*(b-c)=2*b-2*c]]

                  U Spec, 14

 

            42   ALL(c):[2 e n & y e n & c e n => [c<y => 2*(y-c)=2*y-2*c]]

                  U Spec, 41

 

            43   2 e n & y e n & x e n => [x<y => 2*(y-x)=2*y-2*x]

                  U Spec, 42

 

            44   2 e n & y e n

                  Join, 4, 19

 

            45   2 e n & y e n & x e n

                  Join, 44, 17

 

            46   x<y => 2*(y-x)=2*y-2*x

                  Detach, 43, 45

 

         Prove: x<y

        

         Apply definition of <

 

            47   ALL(b):[2*x e n & b e n => [2*x<b <=> EXIST(c):[c e n & ~c=0 & 2*x+c=b]]]

                  U Spec, 12, 24

 

            48   2*x e n & 2*y e n => [2*x<2*y <=> EXIST(c):[c e n & ~c=0 & 2*x+c=2*y]]

                  U Spec, 47, 27

 

            49   2*x e n & 2*y e n

                  Join, 24, 27

 

            50   2*x<2*y <=> EXIST(c):[c e n & ~c=0 & 2*x+c=2*y]

                  Detach, 48, 49

 

            51   [2*x<2*y => EXIST(c):[c e n & ~c=0 & 2*x+c=2*y]]

             & [EXIST(c):[c e n & ~c=0 & 2*x+c=2*y] => 2*x<2*y]

                  Iff-And, 50

 

            52   EXIST(c):[c e n & ~c=0 & 2*x+c=2*y] => 2*x<2*y

                  Split, 51

 

            53   1 e n & ~1=0

                  Join, 2, 3

 

            54   1 e n & ~1=0 & 2*x+1=2*y

                  Join, 53, 20

 

            55   EXIST(c):[c e n & ~c=0 & 2*x+c=2*y]

                  E Gen, 54

 

            56   2*x<2*y

                  Detach, 52, 55

 

        Apply property of <

 

            57   ALL(b):ALL(c):[2 e n & b e n & c e n & ~2=0 => [2*b<2*c => b<c]]

                  U Spec, 13

 

            58   ALL(c):[2 e n & x e n & c e n & ~2=0 => [2*x<2*c => x<c]]

                  U Spec, 57

 

            59   2 e n & x e n & y e n & ~2=0 => [2*x<2*y => x<y]

                  U Spec, 58

 

            60   2 e n & x e n

                  Join, 4, 17

 

            61   2 e n & x e n & y e n

                  Join, 60, 19

 

            62   2 e n & x e n & y e n & ~2=0

                  Join, 61, 5

 

            63   2*x<2*y => x<y

                  Detach, 59, 62

 

         As Required:

 

            64   x<y

                  Detach, 63, 56

 

            65   2*(y-x)=2*y-2*x

                  Detach, 46, 64

 

            66   2*(y-x)=1

                  Substitute, 65, 40

 

         Apply property of -

 

            67   ALL(b):[y e n & b e n => [b<y => y-b e n]]

                  U Spec, 11

 

            68   y e n & x e n => [x<y => y-x e n]

                  U Spec, 67

 

            69   y e n & x e n

                  Join, 19, 17

 

            70   x<y => y-x e n

                  Detach, 68, 69

 

            71   y-x e n

                  Detach, 70, 64

 

            72   y-x e n & 2*(y-x)=1

                  Join, 71, 66

 

            73   EXIST(a):[a e n & 2*a=1]

                  E Gen, 72

 

            74   EXIST(a):[a e n & 2*a=1]

             & ~EXIST(a):[a e n & 2*a=1]

                  Join, 73, 9

 

    As Required:

 

      75   ~EXIST(b):[b e n & 2*x+1=2*b]

            4 Conclusion, 18

 

 

LEMMA

 

As Required:

 

76   ALL(a):[a e n => ~EXIST(b):[b e n & 2*a+1=2*b]]

      4 Conclusion, 17

 

   

    Prove: ALL(a):[a e n => [Even(a) => Odd(a+1)]]

   

    Suppose...

 

      77   x e n

            Premise

 

         Prove: Even(x) => Odd(x+1)

        

         Suppose...

 

            78   Even(x)

                  Premise

 

         Apply definition of Even

 

            79   x e n => [Even(x) <=> EXIST(b):[b e n & x=2*b]]

                  U Spec, 15

 

            80   Even(x) <=> EXIST(b):[b e n & x=2*b]

                  Detach, 79, 77

 

            81   [Even(x) => EXIST(b):[b e n & x=2*b]]

             & [EXIST(b):[b e n & x=2*b] => Even(x)]

                  Iff-And, 80

 

            82   Even(x) => EXIST(b):[b e n & x=2*b]

                  Split, 81

 

            83   EXIST(b):[b e n & x=2*b]

                  Detach, 82, 78

 

            84   y e n & x=2*y

                  E Spec, 83

 

            85   y e n

                  Split, 84

 

            86   x=2*y

                  Split, 84

 

            87   ALL(b):[x e n & b e n => x+b e n]

                  U Spec, 6

 

            88   x e n & 1 e n => x+1 e n

                  U Spec, 87

 

            89   x e n & 1 e n

                  Join, 77, 2

 

            90   x+1 e n

                  Detach, 88, 89

 

            91   Odd(x+1) <=> ~Even(x+1)

                  U Spec, 16, 90

 

            92   [Odd(x+1) => ~Even(x+1)] & [~Even(x+1) => Odd(x+1)]

                  Iff-And, 91

 

         Sufficient: For Odd(x+1)

 

            93   ~Even(x+1) => Odd(x+1)

                  Split, 92

 

            

             Prove: ~Even(x+1)

            

             Suppose to the contrary...

 

                  94   Even(x+1)

                        Premise

 

             Apply definition of Even

 

                  95   x+1 e n => [Even(x+1) <=> EXIST(b):[b e n & x+1=2*b]]

                        U Spec, 15, 90

 

                  96   Even(x+1) <=> EXIST(b):[b e n & x+1=2*b]

                        Detach, 95, 90

 

                  97   [Even(x+1) => EXIST(b):[b e n & x+1=2*b]]

                 & [EXIST(b):[b e n & x+1=2*b] => Even(x+1)]

                        Iff-And, 96

 

                  98   Even(x+1) => EXIST(b):[b e n & x+1=2*b]

                        Split, 97

 

                  99   EXIST(b):[b e n & x+1=2*b]

                        Detach, 98, 94

 

             Apply lemma

 

                  100  y e n => ~EXIST(b):[b e n & 2*y+1=2*b]

                        U Spec, 76

 

                  101  ~EXIST(b):[b e n & 2*y+1=2*b]

                        Detach, 100, 85

 

                  102  EXIST(b):[b e n & 2*y+1=2*b]

                        Substitute, 86, 99

 

                  103  EXIST(b):[b e n & 2*y+1=2*b]

                 & ~EXIST(b):[b e n & 2*y+1=2*b]

                        Join, 102, 101

 

         As Required:

 

            104  ~Even(x+1)

                  4 Conclusion, 94

 

            105  Odd(x+1)

                  Detach, 93, 104

 

    As Required:

 

      106  Even(x) => Odd(x+1)

            4 Conclusion, 78

 

 

THEOREM

 

As Required:

 

107  ALL(a):[a e n => [Even(a) => Odd(a+1)]]

      4 Conclusion, 77

 

   

    Prove: ALL(a):[a e n => Even(2*a) & Odd(2*a+1)]

   

    Suppose...

 

      108  x e n

            Premise

 

      109  ALL(b):[2 e n & b e n => 2*b e n]

            U Spec, 8

 

      110  2 e n & x e n => 2*x e n

            U Spec, 109

 

      111  2 e n & x e n

            Join, 4, 108

 

      112  2*x e n

            Detach, 110, 111

 

      113  2*x e n => [Even(2*x) <=> EXIST(b):[b e n & 2*x=2*b]]

            U Spec, 15, 112

 

      114  Even(2*x) <=> EXIST(b):[b e n & 2*x=2*b]

            Detach, 113, 112

 

      115  [Even(2*x) => EXIST(b):[b e n & 2*x=2*b]]

         & [EXIST(b):[b e n & 2*x=2*b] => Even(2*x)]

            Iff-And, 114

 

    Sufficient: For Even(2*x)

 

      116  EXIST(b):[b e n & 2*x=2*b] => Even(2*x)

            Split, 115

 

      117  2*x=2*x

            Reflex, 112

 

      118  x e n & 2*x=2*x

            Join, 108, 117

 

      119  EXIST(b):[b e n & 2*x=2*b]

            E Gen, 118

 

      120  Even(2*x)

            Detach, 116, 119

 

    Apply theorem

 

      121  2*x e n => [Even(2*x) => Odd(2*x+1)]

            U Spec, 107, 112

 

      122  Even(2*x) => Odd(2*x+1)

            Detach, 121, 112

 

      123  Odd(2*x+1)

            Detach, 122, 120

 

      124  Even(2*x) & Odd(2*x+1)

            Join, 120, 123

 

 

COROLLARY

 

As Required:

 

125  ALL(a):[a e n => Even(2*a) & Odd(2*a+1)]

      4 Conclusion, 108