THEOREM

*******

 

EXIST(pow):[ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow(a,b) e n]

& pow(0,1)=0

& ALL(a):[a e n => pow(a,2)=a*a]

& ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow(a,b+1)=pow(a,b)*a]]

 

Equivalently...

 

EXIST(pow):[ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow(a,b) e n]

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

& pow(0,1)=0

& ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow(a,b+1)=pow(a,b)*a]]

 

 

This machine-verified formal proof was written with the aid of

the author's DC Proof 2.0 software available at http://www.dcproof.com

 

 

Alternative function axiom used here:

 

1     ALL(f):ALL(a):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e f => (c1,c2) e a & d e b]

     & ALL(c1):ALL(c2):[(c1,c2) e a => EXIST(d):[d e b & (c1,c2,d) e f]]

     & ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e f & (c1,c2,d2) e f => d1=d2]

     => ALL(c1):ALL(c2):ALL(d):[d=f(c1,c2) <=> (c1,c2,d) e f]]

      Axiom

 

 

AXIOMS / DEFINITIONS USED

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

 

n is a set (the set of natural numbers)

 

2     Set(n)

      Axiom

 

3     0 e n

      Axiom

 

4     ALL(a):[a e n => ~a+1=0]

      Axiom

 

5     ALL(a):[Set(a) & ALL(b):[b e a => b e n]

     => [0 e a & ALL(b):[b e a => b+1 e a]

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

      Axiom

 

+ is a binary function on n

 

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

      Axiom

 

* is a binary function on n

 

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

      Axiom

 

8     1 e n

      Axiom

 

9     ~1=0

      Axiom

 

10    2 e n

      Axiom

 

11    2=1+1

      Axiom

 

12    ~2=0

      Axiom

 

Adding 0

 

13    ALL(a):[a e n => a+0=a]

      Axiom

 

Multiplying by 0

 

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

      Axiom

 

Multiplying by 1

 

15    ALL(a):[a e n => a*1=a]

      Axiom

 

+ is commutative

 

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

      Axiom

 

* is commutative

 

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

      Axiom

 

Right-cancelability of *

 

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

      Axiom

 

 

PREVIOUS RESULT

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

 

Infinitely many pow functions                  PROOF

 

19    ALL(x0):[x0 e n

     => EXIST(pow):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]

     & pow(0,0)=x0

     & ALL(a):[a e n => pow(a,2)=a*a]

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

      Axiom

 

PROOF

*****

 

Apply previous result

 

20    0 e n

     => EXIST(pow):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]

     & pow(0,0)=0

     & ALL(a):[a e n => pow(a,2)=a*a]

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

      U Spec, 19

 

21    EXIST(pow):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]

     & pow(0,0)=0

     & ALL(a):[a e n => pow(a,2)=a*a]

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

      Detach, 20, 3

 

Define: pow  (with pow(0,0)=0)

***********

 

22    ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]

     & pow(0,0)=0

     & ALL(a):[a e n => pow(a,2)=a*a]

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

      E Spec, 21

 

 

Define: pow  (with pow(0,0)=0)

***********

 

23    ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]

      Split, 22

 

24    pow(0,0)=0

      Split, 22

 

25    ALL(a):[a e n => pow(a,2)=a*a]

      Split, 22

 

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

      Split, 22

 

27    ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]

      Cart Prod

 

28    ALL(a2):[Set(n) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e a2]]]

      U Spec, 27

 

29    Set(n) & Set(n) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]

      U Spec, 28

 

30    Set(n) & Set(n)

      Join, 2, 2

 

31    EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]

      Detach, 29, 30

 

32    Set'(n2) & ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]

      E Spec, 31

 

 

Define: n2

**********

 

33    Set'(n2)

      Split, 32

 

34    ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]

      Split, 32

 

35    ALL(a1):ALL(a2):ALL(a3):[Set(a1) & Set(a2) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e a1 & c2 e a2 & c3 e a3]]]

      Cart Prod

 

36    ALL(a2):ALL(a3):[Set(n) & Set(a2) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e a2 & c3 e a3]]]

      U Spec, 35

 

37    ALL(a3):[Set(n) & Set(n) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e a3]]]

      U Spec, 36

 

38    Set(n) & Set(n) & Set(n) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e n]]

      U Spec, 37

 

39    Set(n) & Set(n)

      Join, 2, 2

 

40    Set(n) & Set(n) & Set(n)

      Join, 39, 2

 

41    EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e n]]

      Detach, 38, 40

 

42    Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]

      E Spec, 41

 

 

Define: n3

**********

 

43    Set''(n3)

      Split, 42

 

44    ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]

      Split, 42

 

45    EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e n2 & ~[a=0 & b=0]]]

      Subset, 33

 

46    Set'(n2') & ALL(a):ALL(b):[(a,b) e n2' <=> (a,b) e n2 & ~[a=0 & b=0]]

      E Spec, 45

 

 

Define: n2'

***********

 

47    Set'(n2')

      Split, 46

 

48    ALL(a):ALL(b):[(a,b) e n2' <=> (a,b) e n2 & ~[a=0 & b=0]]

      Split, 46

 

49    EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub

     <=> (a,b,c) e n3 & [(a,b) e n2' & c=pow(a,b)]]]

      Subset, 43

 

50    Set''(pow') & ALL(a):ALL(b):ALL(c):[(a,b,c) e pow'

     <=> (a,b,c) e n3 & [(a,b) e n2' & c=pow(a,b)]]

      E Spec, 49

 

 

Define: pow'

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

 

51    Set''(pow')

      Split, 50

 

52    ALL(a):ALL(b):ALL(c):[(a,b,c) e pow'

     <=> (a,b,c) e n3 & [(a,b) e n2' & c=pow(a,b)]]

      Split, 50

 

53    ALL(a):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow' => (c1,c2) e a & d e b]

     & ALL(c1):ALL(c2):[(c1,c2) e a => EXIST(d):[d e b & (c1,c2,d) e pow']]

     & ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow' & (c1,c2,d2) e pow' => d1=d2]

     => ALL(c1):ALL(c2):ALL(d):[d=pow'(c1,c2) <=> (c1,c2,d) e pow']]

      U Spec, 1

 

54    ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow' => (c1,c2) e n2' & d e b]

     & ALL(c1):ALL(c2):[(c1,c2) e n2' => EXIST(d):[d e b & (c1,c2,d) e pow']]

     & ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow' & (c1,c2,d2) e pow' => d1=d2]

     => ALL(c1):ALL(c2):ALL(d):[d=pow'(c1,c2) <=> (c1,c2,d) e pow']]

      U Spec, 53

 

Sufficient: For functionality of pow'

 

55    ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow' => (c1,c2) e n2' & d e n]

     & ALL(c1):ALL(c2):[(c1,c2) e n2' => EXIST(d):[d e n & (c1,c2,d) e pow']]

     & ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow' & (c1,c2,d2) e pow' => d1=d2]

     => ALL(c1):ALL(c2):ALL(d):[d=pow'(c1,c2) <=> (c1,c2,d) e pow']

      U Spec, 54

 

     Prove: ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e f => (c1,c2) e a & d e b]

    

     Suppose...

 

      56    (x,y,z) e pow'

            Premise

 

      57    ALL(b):ALL(c):[(x,b,c) e pow'

          <=> (x,b,c) e n3 & [(x,b) e n2' & c=pow(x,b)]]

            U Spec, 52

 

      58    ALL(c):[(x,y,c) e pow'

          <=> (x,y,c) e n3 & [(x,y) e n2' & c=pow(x,y)]]

            U Spec, 57

 

      59    (x,y,z) e pow'

          <=> (x,y,z) e n3 & [(x,y) e n2' & z=pow(x,y)]

            U Spec, 58

 

      60    [(x,y,z) e pow' => (x,y,z) e n3 & [(x,y) e n2' & z=pow(x,y)]]

          & [(x,y,z) e n3 & [(x,y) e n2' & z=pow(x,y)] => (x,y,z) e pow']

            Iff-And, 59

 

      61    (x,y,z) e pow' => (x,y,z) e n3 & [(x,y) e n2' & z=pow(x,y)]

            Split, 60

 

      62    (x,y,z) e n3 & [(x,y) e n2' & z=pow(x,y)] => (x,y,z) e pow'

            Split, 60

 

      63    (x,y,z) e n3 & [(x,y) e n2' & z=pow(x,y)]

            Detach, 61, 56

 

      64    (x,y,z) e n3

            Split, 63

 

      65    (x,y) e n2' & z=pow(x,y)

            Split, 63

 

      66    (x,y) e n2'

            Split, 65

 

      67    z=pow(x,y)

            Split, 65

 

      68    ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

            U Spec, 44

 

      69    ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]

            U Spec, 68

 

      70    (x,y,z) e n3 <=> x e n & y e n & z e n

            U Spec, 69

 

      71    [(x,y,z) e n3 => x e n & y e n & z e n]

          & [x e n & y e n & z e n => (x,y,z) e n3]

            Iff-And, 70

 

      72    (x,y,z) e n3 => x e n & y e n & z e n

            Split, 71

 

      73    x e n & y e n & z e n => (x,y,z) e n3

            Split, 71

 

      74    x e n & y e n & z e n

            Detach, 72, 64

 

      75    x e n

            Split, 74

 

      76    y e n

            Split, 74

 

      77    z e n

            Split, 74

 

      78    (x,y) e n2' & z e n

            Join, 66, 77

 

Functionality: Part 1

 

79    ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow' => (c1,c2) e n2' & d e n]

      4 Conclusion, 56

 

    

     Suppose...

 

      80    (x,y) e n2'

            Premise

 

      81    ALL(b):ALL(c):[(x,b,c) e pow'

          <=> (x,b,c) e n3 & [(x,b) e n2' & c=pow(x,b)]]

            U Spec, 52

 

      82    ALL(c):[(x,y,c) e pow'

          <=> (x,y,c) e n3 & [(x,y) e n2' & c=pow(x,y)]]

            U Spec, 81

 

      83    (x,y,pow(x,y)) e pow'

          <=> (x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)]

            U Spec, 82

 

      84    [(x,y,pow(x,y)) e pow' => (x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)]]

          & [(x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)] => (x,y,pow(x,y)) e pow']

            Iff-And, 83

 

      85    (x,y,pow(x,y)) e pow' => (x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)]

            Split, 84

 

     Sufficient: (x,y,pow(x,y)) e pow'

 

      86    (x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)] => (x,y,pow(x,y)) e pow'

            Split, 84

 

      87    ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

            U Spec, 44

 

      88    ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]

            U Spec, 87

 

      89    (x,y,pow(x,y)) e n3 <=> x e n & y e n & pow(x,y) e n

            U Spec, 88

 

      90    [(x,y,pow(x,y)) e n3 => x e n & y e n & pow(x,y) e n]

          & [x e n & y e n & pow(x,y) e n => (x,y,pow(x,y)) e n3]

            Iff-And, 89

 

      91    (x,y,pow(x,y)) e n3 => x e n & y e n & pow(x,y) e n

            Split, 90

 

      92    x e n & y e n & pow(x,y) e n => (x,y,pow(x,y)) e n3

            Split, 90

 

      93    ALL(b):[x e n & b e n => pow(x,b) e n]

            U Spec, 23

 

      94    x e n & y e n => pow(x,y) e n

            U Spec, 93

 

      95    ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]

            U Spec, 48

 

      96    (x,y) e n2' <=> (x,y) e n2 & ~[x=0 & y=0]

            U Spec, 95

 

      97    [(x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]]

          & [(x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2']

            Iff-And, 96

 

      98    (x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]

            Split, 97

 

      99    (x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2'

            Split, 97

 

      100  (x,y) e n2 & ~[x=0 & y=0]

            Detach, 98, 80

 

      101  (x,y) e n2

            Split, 100

 

      102  ~[x=0 & y=0]

            Split, 100

 

      103  ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

            U Spec, 34

 

      104  (x,y) e n2 <=> x e n & y e n

            U Spec, 103

 

      105  [(x,y) e n2 => x e n & y e n]

          & [x e n & y e n => (x,y) e n2]

            Iff-And, 104

 

      106  (x,y) e n2 => x e n & y e n

            Split, 105

 

      107  x e n & y e n => (x,y) e n2

            Split, 105

 

      108  x e n & y e n

            Detach, 106, 101

 

      109  x e n

            Split, 108

 

      110  y e n

            Split, 108

 

      111  pow(x,y) e n

            Detach, 94, 108

 

      112  x e n & y e n & pow(x,y) e n

            Join, 108, 111

 

      113  (x,y,pow(x,y)) e n3

            Detach, 92, 112

 

      114  pow(x,y)=pow(x,y)

            Reflex

 

      115  (x,y) e n2' & pow(x,y)=pow(x,y)

            Join, 80, 114

 

      116  (x,y,pow(x,y)) e n3

          & [(x,y) e n2' & pow(x,y)=pow(x,y)]

            Join, 113, 115

 

      117  (x,y,pow(x,y)) e pow'

            Detach, 86, 116

 

      118  (x,y) e n2' & pow(x,y)=pow(x,y)

            Join, 80, 114

 

      119  (x,y,pow(x,y)) e n3

          & [(x,y) e n2' & pow(x,y)=pow(x,y)]

            Join, 113, 118

 

      120  (x,y,pow(x,y)) e pow'

            Detach, 86, 119

 

      121  pow(x,y) e n & (x,y,pow(x,y)) e pow'

            Join, 111, 120

 

      122  EXIST(d):[d e n & (x,y,d) e pow']

            E Gen, 121

 

Functionality: Part 2

 

123  ALL(c1):ALL(c2):[(c1,c2) e n2' => EXIST(d):[d e n & (c1,c2,d) e pow']]

      4 Conclusion, 80

 

      124  (x,y,z1) e pow' & (x,y,z2) e pow'

            Premise

 

      125  (x,y,z1) e pow'

            Split, 124

 

      126  (x,y,z2) e pow'

            Split, 124

 

      127  ALL(b):ALL(c):[(x,b,c) e pow'

          <=> (x,b,c) e n3 & [(x,b) e n2' & c=pow(x,b)]]

            U Spec, 52

 

      128  ALL(c):[(x,y,c) e pow'

          <=> (x,y,c) e n3 & [(x,y) e n2' & c=pow(x,y)]]

            U Spec, 127

 

      129  (x,y,z1) e pow'

          <=> (x,y,z1) e n3 & [(x,y) e n2' & z1=pow(x,y)]

            U Spec, 128

 

      130  [(x,y,z1) e pow' => (x,y,z1) e n3 & [(x,y) e n2' & z1=pow(x,y)]]

          & [(x,y,z1) e n3 & [(x,y) e n2' & z1=pow(x,y)] => (x,y,z1) e pow']

            Iff-And, 129

 

      131  (x,y,z1) e pow' => (x,y,z1) e n3 & [(x,y) e n2' & z1=pow(x,y)]

            Split, 130

 

      132  (x,y,z1) e n3 & [(x,y) e n2' & z1=pow(x,y)] => (x,y,z1) e pow'

            Split, 130

 

      133  (x,y,z1) e n3 & [(x,y) e n2' & z1=pow(x,y)]

            Detach, 131, 125

 

      134  (x,y,z1) e n3

            Split, 133

 

      135  (x,y) e n2' & z1=pow(x,y)

            Split, 133

 

      136  (x,y) e n2'

            Split, 135

 

      137  z1=pow(x,y)

            Split, 135

 

      138  (x,y,z2) e pow'

          <=> (x,y,z2) e n3 & [(x,y) e n2' & z2=pow(x,y)]

            U Spec, 128

 

      139  [(x,y,z2) e pow' => (x,y,z2) e n3 & [(x,y) e n2' & z2=pow(x,y)]]

          & [(x,y,z2) e n3 & [(x,y) e n2' & z2=pow(x,y)] => (x,y,z2) e pow']

            Iff-And, 138

 

      140  (x,y,z2) e pow' => (x,y,z2) e n3 & [(x,y) e n2' & z2=pow(x,y)]

            Split, 139

 

      141  (x,y,z2) e n3 & [(x,y) e n2' & z2=pow(x,y)] => (x,y,z2) e pow'

            Split, 139

 

      142  (x,y,z2) e n3 & [(x,y) e n2' & z2=pow(x,y)]

            Detach, 140, 126

 

      143  (x,y,z2) e n3

            Split, 142

 

      144  (x,y) e n2' & z2=pow(x,y)

            Split, 142

 

      145  (x,y) e n2'

            Split, 144

 

      146  z2=pow(x,y)

            Split, 144

 

      147  z1=z2

            Substitute, 146, 137

 

Functionality: Part 3

 

148  ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow' & (c1,c2,d2) e pow' => d1=d2]

      4 Conclusion, 124

 

149  ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow' => (c1,c2) e n2' & d e n]

     & ALL(c1):ALL(c2):[(c1,c2) e n2' => EXIST(d):[d e n & (c1,c2,d) e pow']]

      Join, 79, 123

 

150  ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow' => (c1,c2) e n2' & d e n]

     & ALL(c1):ALL(c2):[(c1,c2) e n2' => EXIST(d):[d e n & (c1,c2,d) e pow']]

     & ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow' & (c1,c2,d2) e pow' => d1=d2]

      Join, 149, 148

 

 

As Required: pow' is a function

 

151  ALL(c1):ALL(c2):ALL(d):[d=pow'(c1,c2) <=> (c1,c2,d) e pow']

      Detach, 55, 150

 

      152  (x,y) e n2'

            Premise

 

      153  ALL(c2):[(x,c2) e n2' => EXIST(d):[d e n & (x,c2,d) e pow']]

            U Spec, 123

 

      154  (x,y) e n2' => EXIST(d):[d e n & (x,y,d) e pow']

            U Spec, 153

 

      155  EXIST(d):[d e n & (x,y,d) e pow']

            Detach, 154, 152

 

      156  z e n & (x,y,z) e pow'

            E Spec, 155

 

      157  z e n

            Split, 156

 

      158  (x,y,z) e pow'

            Split, 156

 

      159  ALL(c2):ALL(d):[d=pow'(x,c2) <=> (x,c2,d) e pow']

            U Spec, 151

 

      160  ALL(d):[d=pow'(x,y) <=> (x,y,d) e pow']

            U Spec, 159

 

      161  z=pow'(x,y) <=> (x,y,z) e pow'

            U Spec, 160

 

      162  [z=pow'(x,y) => (x,y,z) e pow']

          & [(x,y,z) e pow' => z=pow'(x,y)]

            Iff-And, 161

 

      163  z=pow'(x,y) => (x,y,z) e pow'

            Split, 162

 

      164  (x,y,z) e pow' => z=pow'(x,y)

            Split, 162

 

      165  z=pow'(x,y)

            Detach, 164, 158

 

      166  pow'(x,y) e n

            Substitute, 165, 157

 

As Required:

 

167  ALL(a):ALL(b):[(a,b) e n2' => pow'(a,b) e n]

      4 Conclusion, 152

 

      168  (x,y) e n2'

            Premise

 

      169  ALL(b):ALL(c):[(x,b,c) e pow'

          <=> (x,b,c) e n3 & [(x,b) e n2' & c=pow(x,b)]]

            U Spec, 52

 

      170  ALL(c):[(x,y,c) e pow'

          <=> (x,y,c) e n3 & [(x,y) e n2' & c=pow(x,y)]]

            U Spec, 169

 

      171  (x,y,pow(x,y)) e pow'

          <=> (x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)]

            U Spec, 170

 

      172  [(x,y,pow(x,y)) e pow' => (x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)]]

          & [(x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)] => (x,y,pow(x,y)) e pow']

            Iff-And, 171

 

      173  (x,y,pow(x,y)) e pow' => (x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)]

            Split, 172

 

     Sufficient: (x,y,pow(x,y)) e pow'

 

      174  (x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)] => (x,y,pow(x,y)) e pow'

            Split, 172

 

      175  ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

            U Spec, 44

 

      176  ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]

            U Spec, 175

 

      177  (x,y,pow(x,y)) e n3 <=> x e n & y e n & pow(x,y) e n

            U Spec, 176

 

      178  [(x,y,pow(x,y)) e n3 => x e n & y e n & pow(x,y) e n]

          & [x e n & y e n & pow(x,y) e n => (x,y,pow(x,y)) e n3]

            Iff-And, 177

 

      179  (x,y,pow(x,y)) e n3 => x e n & y e n & pow(x,y) e n

            Split, 178

 

      180  x e n & y e n & pow(x,y) e n => (x,y,pow(x,y)) e n3

            Split, 178

 

      181  ALL(b):[x e n & b e n => pow(x,b) e n]

            U Spec, 23

 

      182  x e n & y e n => pow(x,y) e n

            U Spec, 181

 

      183  ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]

            U Spec, 48

 

      184  (x,y) e n2' <=> (x,y) e n2 & ~[x=0 & y=0]

            U Spec, 183

 

      185  [(x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]]

          & [(x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2']

            Iff-And, 184

 

      186  (x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]

            Split, 185

 

      187  (x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2'

            Split, 185

 

      188  (x,y) e n2 & ~[x=0 & y=0]

            Detach, 186, 168

 

      189  (x,y) e n2

            Split, 188

 

      190  ~[x=0 & y=0]

            Split, 188

 

      191  ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

            U Spec, 34

 

      192  (x,y) e n2 <=> x e n & y e n

            U Spec, 191

 

      193  [(x,y) e n2 => x e n & y e n]

          & [x e n & y e n => (x,y) e n2]

            Iff-And, 192

 

      194  (x,y) e n2 => x e n & y e n

            Split, 193

 

      195  x e n & y e n => (x,y) e n2

            Split, 193

 

      196  x e n & y e n

            Detach, 194, 189

 

      197  pow(x,y) e n

            Detach, 182, 196

 

      198  x e n & y e n & pow(x,y) e n

            Join, 196, 197

 

      199  (x,y,pow(x,y)) e n3

            Detach, 180, 198

 

      200  pow(x,y)=pow(x,y)

            Reflex

 

      201  (x,y) e n2' & pow(x,y)=pow(x,y)

            Join, 168, 200

 

      202  (x,y,pow(x,y)) e n3

          & [(x,y) e n2' & pow(x,y)=pow(x,y)]

            Join, 199, 201

 

      203  (x,y,pow(x,y)) e pow'

            Detach, 174, 202

 

      204  ALL(c2):ALL(d):[d=pow'(x,c2) <=> (x,c2,d) e pow']

            U Spec, 151

 

      205  ALL(d):[d=pow'(x,y) <=> (x,y,d) e pow']

            U Spec, 204

 

      206  pow(x,y)=pow'(x,y) <=> (x,y,pow(x,y)) e pow'

            U Spec, 205

 

      207  [pow(x,y)=pow'(x,y) => (x,y,pow(x,y)) e pow']

          & [(x,y,pow(x,y)) e pow' => pow(x,y)=pow'(x,y)]

            Iff-And, 206

 

      208  pow(x,y)=pow'(x,y) => (x,y,pow(x,y)) e pow'

            Split, 207

 

      209  (x,y,pow(x,y)) e pow' => pow(x,y)=pow'(x,y)

            Split, 207

 

      210  pow(x,y)=pow'(x,y)

            Detach, 209, 203

 

      211  pow'(x,y)=pow(x,y)

            Sym, 210

 

As Required:

 

212  ALL(a):ALL(b):[(a,b) e n2' => pow'(a,b)=pow(a,b)]

      4 Conclusion, 168

 

      213  x e n

            Premise

 

      214  x e n => pow(x,2)=x*x

            U Spec, 25

 

      215  pow(x,2)=x*x

            Detach, 214, 213

 

      216  ALL(b):[(x,b) e n2' => pow'(x,b)=pow(x,b)]

            U Spec, 212

 

      217  (x,2) e n2' => pow'(x,2)=pow(x,2)

            U Spec, 216

 

      218  ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]

            U Spec, 48

 

      219  (x,2) e n2' <=> (x,2) e n2 & ~[x=0 & 2=0]

            U Spec, 218

 

      220  [(x,2) e n2' => (x,2) e n2 & ~[x=0 & 2=0]]

          & [(x,2) e n2 & ~[x=0 & 2=0] => (x,2) e n2']

            Iff-And, 219

 

      221  (x,2) e n2' => (x,2) e n2 & ~[x=0 & 2=0]

            Split, 220

 

      222  (x,2) e n2 & ~[x=0 & 2=0] => (x,2) e n2'

            Split, 220

 

      223  ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

            U Spec, 34

 

      224  (x,2) e n2 <=> x e n & 2 e n

            U Spec, 223

 

      225  [(x,2) e n2 => x e n & 2 e n]

          & [x e n & 2 e n => (x,2) e n2]

            Iff-And, 224

 

      226  (x,2) e n2 => x e n & 2 e n

            Split, 225

 

      227  x e n & 2 e n => (x,2) e n2

            Split, 225

 

      228  x e n & 2 e n

            Join, 213, 10

 

      229  (x,2) e n2

            Detach, 227, 228

 

            230  x=0 & 2=0

                  Premise

 

            231  x=0

                  Split, 230

 

            232  2=0

                  Split, 230

 

            233  2=0 & ~2=0

                  Join, 232, 12

 

      234  ~[x=0 & 2=0]

            4 Conclusion, 230

 

      235  (x,2) e n2 & ~[x=0 & 2=0]

            Join, 229, 234

 

      236  (x,2) e n2'

            Detach, 222, 235

 

      237  pow'(x,2)=pow(x,2)

            Detach, 217, 236

 

      238  pow'(x,2)=x*x

            Substitute, 215, 237

 

As Required:

 

239  ALL(a):[a e n => pow'(a,2)=a*a]

      4 Conclusion, 213

 

      240  (x,y) e n2'

            Premise

 

      241  ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]

            U Spec, 48

 

      242  (x,y) e n2' <=> (x,y) e n2 & ~[x=0 & y=0]

            U Spec, 241

 

      243  [(x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]]

          & [(x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2']

            Iff-And, 242

 

      244  (x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]

            Split, 243

 

      245  (x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2'

            Split, 243

 

      246  (x,y) e n2 & ~[x=0 & y=0]

            Detach, 244, 240

 

      247  (x,y) e n2

            Split, 246

 

      248  ~[x=0 & y=0]

            Split, 246

 

      249  ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

            U Spec, 34

 

      250  (x,y) e n2 <=> x e n & y e n

            U Spec, 249

 

      251  [(x,y) e n2 => x e n & y e n]

          & [x e n & y e n => (x,y) e n2]

            Iff-And, 250

 

      252  (x,y) e n2 => x e n & y e n

            Split, 251

 

      253  x e n & y e n => (x,y) e n2

            Split, 251

 

      254  x e n & y e n

            Detach, 252, 247

 

      255  ALL(b):[x e n & b e n => pow(x,b+1)=pow(x,b)*x]

            U Spec, 26

 

      256  x e n

            Split, 254

 

      257  y e n

            Split, 254

 

      258  x e n & y e n => pow(x,y+1)=pow(x,y)*x

            U Spec, 255

 

      259  pow(x,y+1)=pow(x,y)*x

            Detach, 258, 254

 

      260  ALL(b):[(x,b) e n2' => pow'(x,b)=pow(x,b)]

            U Spec, 212

 

      261  (x,y+1) e n2' => pow'(x,y+1)=pow(x,y+1)

            U Spec, 260

 

      262  ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]

            U Spec, 48

 

      263  (x,y+1) e n2' <=> (x,y+1) e n2 & ~[x=0 & y+1=0]

            U Spec, 262

 

      264  [(x,y+1) e n2' => (x,y+1) e n2 & ~[x=0 & y+1=0]]

          & [(x,y+1) e n2 & ~[x=0 & y+1=0] => (x,y+1) e n2']

            Iff-And, 263

 

      265  (x,y+1) e n2' => (x,y+1) e n2 & ~[x=0 & y+1=0]

            Split, 264

 

      266  (x,y+1) e n2 & ~[x=0 & y+1=0] => (x,y+1) e n2'

            Split, 264

 

      267  ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

            U Spec, 34

 

      268  (x,y+1) e n2 <=> x e n & y+1 e n

            U Spec, 267

 

      269  [(x,y+1) e n2 => x e n & y+1 e n]

          & [x e n & y+1 e n => (x,y+1) e n2]

            Iff-And, 268

 

      270  (x,y+1) e n2 => x e n & y+1 e n

            Split, 269

 

      271  x e n & y+1 e n => (x,y+1) e n2

            Split, 269

 

      272  ALL(b):[y e n & b e n => y+b e n]

            U Spec, 6

 

      273  y e n & 1 e n => y+1 e n

            U Spec, 272

 

      274  y e n & 1 e n

            Join, 257, 8

 

      275  y+1 e n

            Detach, 273, 274

 

      276  x e n & y+1 e n

            Join, 256, 275

 

      277  (x,y+1) e n2

            Detach, 271, 276

 

            278  x=0 & y+1=0

                  Premise

 

            279  x=0

                  Split, 278

 

            280  y+1=0

                  Split, 278

 

            281  y e n => ~y+1=0

                  U Spec, 4

 

            282  ~y+1=0

                  Detach, 281, 257

 

            283  y+1=0 & ~y+1=0

                  Join, 280, 282

 

      284  ~[x=0 & y+1=0]

            4 Conclusion, 278

 

      285  (x,y+1) e n2 & ~[x=0 & y+1=0]

            Join, 277, 284

 

      286  (x,y+1) e n2'

            Detach, 266, 285

 

      287  pow'(x,y+1)=pow(x,y+1)

            Detach, 261, 286

 

      288  ALL(b):[(x,b) e n2' => pow'(x,b)=pow(x,b)]

            U Spec, 212

 

      289  (x,y) e n2' => pow'(x,y)=pow(x,y)

            U Spec, 288

 

      290  pow'(x,y)=pow(x,y)

            Detach, 289, 240

 

      291  pow'(x,y+1)=pow(x,y)*x

            Substitute, 287, 259

 

      292  pow'(x,y+1)=pow'(x,y)*x

            Substitute, 290, 291

 

As Required:

 

293  ALL(a):ALL(b):[(a,b) e n2' => pow'(a,b+1)=pow'(a,b)*a]

      4 Conclusion, 240

 

      294  x e n & y e n & ~[x=0 & y=0]

            Premise

 

      295  x e n

            Split, 294

 

      296  y e n

            Split, 294

 

      297  ~[x=0 & y=0]

            Split, 294

 

      298  ALL(b):[(x,b) e n2' => pow'(x,b) e n]

            U Spec, 167

 

      299  (x,y) e n2' => pow'(x,y) e n

            U Spec, 298

 

      300  ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]

            U Spec, 48

 

      301  (x,y) e n2' <=> (x,y) e n2 & ~[x=0 & y=0]

            U Spec, 300

 

      302  [(x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]]

          & [(x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2']

            Iff-And, 301

 

      303  (x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]

            Split, 302

 

      304  (x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2'

            Split, 302

 

      305  ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

            U Spec, 34

 

      306  (x,y) e n2 <=> x e n & y e n

            U Spec, 305

 

      307  [(x,y) e n2 => x e n & y e n]

          & [x e n & y e n => (x,y) e n2]

            Iff-And, 306

 

      308  (x,y) e n2 => x e n & y e n

            Split, 307

 

      309  x e n & y e n => (x,y) e n2

            Split, 307

 

      310  x e n & y e n

            Join, 295, 296

 

      311  (x,y) e n2

            Detach, 309, 310

 

      312  (x,y) e n2 & ~[x=0 & y=0]

            Join, 311, 297

 

      313  (x,y) e n2'

            Detach, 304, 312

 

      314  pow'(x,y) e n

            Detach, 299, 313

 

As Required:

 

315  ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow'(a,b) e n]

      4 Conclusion, 294

 

    

     Suppose...

 

      316  x e n & y e n & ~[x=0 & y=0]

            Premise

 

      317  x e n

            Split, 316

 

      318  y e n

            Split, 316

 

      319  ~[x=0 & y=0]

            Split, 316

 

      320  ALL(b):[(x,b) e n2' => pow'(x,b+1)=pow'(x,b)*x]

            U Spec, 293

 

      321  (x,y) e n2' => pow'(x,y+1)=pow'(x,y)*x

            U Spec, 320

 

      322  ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]

            U Spec, 48

 

      323  (x,y) e n2' <=> (x,y) e n2 & ~[x=0 & y=0]

            U Spec, 322

 

      324  [(x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]]

          & [(x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2']

            Iff-And, 323

 

      325  (x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]

            Split, 324

 

      326  (x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2'

            Split, 324

 

      327  ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

            U Spec, 34

 

      328  (x,y) e n2 <=> x e n & y e n

            U Spec, 327

 

      329  [(x,y) e n2 => x e n & y e n]

          & [x e n & y e n => (x,y) e n2]

            Iff-And, 328

 

      330  (x,y) e n2 => x e n & y e n

            Split, 329

 

      331  x e n & y e n => (x,y) e n2

            Split, 329

 

      332  x e n & y e n

            Join, 317, 318

 

      333  (x,y) e n2

            Detach, 331, 332

 

      334  (x,y) e n2 & ~[x=0 & y=0]

            Join, 333, 319

 

      335  (x,y) e n2'

            Detach, 326, 334

 

      336  pow'(x,y+1)=pow'(x,y)*x

            Detach, 321, 335

 

As Required:

 

337  ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0]

     => pow'(a,b+1)=pow'(a,b)*a]

      4 Conclusion, 316

 

 

Prove: pow'(0,1)=0

 

Apply definition of pow

 

338  ALL(b):[0 e n & b e n => pow(0,b+1)=pow(0,b)*0]

      U Spec, 26

 

339  0 e n & 0 e n => pow(0,0+1)=pow(0,0)*0

      U Spec, 338

 

340  0 e n & 0 e n

      Join, 3, 3

 

341  pow(0,0+1)=pow(0,0)*0

      Detach, 339, 340

 

342  1 e n => 1+0=1

      U Spec, 13

 

343  1+0=1

      Detach, 342, 8

 

344  ALL(b):[0 e n & b e n => 0+b=b+0]

      U Spec, 16

 

345  0 e n & 1 e n => 0+1=1+0

      U Spec, 344

 

346  0 e n & 1 e n

      Join, 3, 8

 

347  0+1=1+0

      Detach, 345, 346

 

348  0+1=1

      Substitute, 347, 343

 

349  pow(0,1)=pow(0,0)*0

      Substitute, 348, 341

 

350  pow(0,1)=0*0

      Substitute, 24, 349

 

351  0 e n => 0*0=0

      U Spec, 14

 

352  0*0=0

      Detach, 351, 3

 

353  pow(0,1)=0

      Substitute, 352, 350

 

354  ALL(b):[(0,b) e n2' => pow'(0,b)=pow(0,b)]

      U Spec, 212

 

355  (0,1) e n2' => pow'(0,1)=pow(0,1)

      U Spec, 354

 

356  ALL(b):[(0,b) e n2' <=> (0,b) e n2 & ~[0=0 & b=0]]

      U Spec, 48

 

357  (0,1) e n2' <=> (0,1) e n2 & ~[0=0 & 1=0]

      U Spec, 356

 

358  [(0,1) e n2' => (0,1) e n2 & ~[0=0 & 1=0]]

     & [(0,1) e n2 & ~[0=0 & 1=0] => (0,1) e n2']

      Iff-And, 357

 

359  (0,1) e n2' => (0,1) e n2 & ~[0=0 & 1=0]

      Split, 358

 

360  (0,1) e n2 & ~[0=0 & 1=0] => (0,1) e n2'

      Split, 358

 

361  ALL(c2):[(0,c2) e n2 <=> 0 e n & c2 e n]

      U Spec, 34

 

362  (0,1) e n2 <=> 0 e n & 1 e n

      U Spec, 361

 

363  [(0,1) e n2 => 0 e n & 1 e n]

     & [0 e n & 1 e n => (0,1) e n2]

      Iff-And, 362

 

364  (0,1) e n2 => 0 e n & 1 e n

      Split, 363

 

365  0 e n & 1 e n => (0,1) e n2

      Split, 363

 

366  0 e n & 1 e n

      Join, 3, 8

 

367  (0,1) e n2

      Detach, 365, 366

 

      368  0=0 & 1=0

            Premise

 

      369  0=0

            Split, 368

 

      370  1=0

            Split, 368

 

      371  1=0 & ~1=0

            Join, 370, 9

 

372  ~[0=0 & 1=0]

      4 Conclusion, 368

 

373  (0,1) e n2 & ~[0=0 & 1=0]

      Join, 367, 372

 

374  (0,1) e n2'

      Detach, 360, 373

 

375  pow'(0,1)=pow(0,1)

      Detach, 355, 374

 

As Required:

 

376  pow'(0,1)=0

      Substitute, 375, 353

 

      377  x e n & ~x=0

            Premise

 

      378  x e n

            Split, 377

 

      379  ~x=0

            Split, 377

 

      380  x e n => pow'(x,2)=x*x

            U Spec, 239

 

      381  pow'(x,2)=x*x

            Detach, 380, 378

 

      382  ALL(b):[x e n & b e n & ~[x=0 & b=0]

          => pow'(x,b+1)=pow'(x,b)*x]

            U Spec, 337

 

      383  x e n & 1 e n & ~[x=0 & 1=0]

          => pow'(x,1+1)=pow'(x,1)*x

            U Spec, 382

 

            384  x=0 & 1=0

                  Premise

 

            385  x=0

                  Split, 384

 

            386  1=0

                  Split, 384

 

            387  1=0 & ~1=0

                  Join, 386, 9

 

      388  ~[x=0 & 1=0]

            4 Conclusion, 384

 

      389  x e n & 1 e n

            Join, 378, 8

 

      390  x e n & 1 e n & ~[x=0 & 1=0]

            Join, 389, 388

 

      391  pow'(x,1+1)=pow'(x,1)*x

            Detach, 383, 390

 

      392  pow'(x,2)=pow'(x,1)*x

            Substitute, 11, 391

 

      393  x*x=pow'(x,1)*x

            Substitute, 381, 392

 

      394  pow'(x,1)*x=x*x

            Sym, 393

 

      395  ALL(b):ALL(c):[pow'(x,1) e n & b e n & c e n & ~b=0 => [pow'(x,1)*b=c*b => pow'(x,1)=c]]

            U Spec, 18

 

      396  ALL(c):[pow'(x,1) e n & x e n & c e n & ~x=0 => [pow'(x,1)*x=c*x => pow'(x,1)=c]]

            U Spec, 395

 

      397  pow'(x,1) e n & x e n & x e n & ~x=0 => [pow'(x,1)*x=x*x => pow'(x,1)=x]

            U Spec, 396

 

      398  ALL(b):[(x,b) e n2' => pow'(x,b) e n]

            U Spec, 167

 

      399  (x,1) e n2' => pow'(x,1) e n

            U Spec, 398

 

      400  ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]

            U Spec, 48

 

      401  (x,1) e n2' <=> (x,1) e n2 & ~[x=0 & 1=0]

            U Spec, 400

 

      402  [(x,1) e n2' => (x,1) e n2 & ~[x=0 & 1=0]]

          & [(x,1) e n2 & ~[x=0 & 1=0] => (x,1) e n2']

            Iff-And, 401

 

      403  (x,1) e n2' => (x,1) e n2 & ~[x=0 & 1=0]

            Split, 402

 

      404  (x,1) e n2 & ~[x=0 & 1=0] => (x,1) e n2'

            Split, 402

 

      405  ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

            U Spec, 34

 

      406  (x,1) e n2 <=> x e n & 1 e n

            U Spec, 405

 

      407  [(x,1) e n2 => x e n & 1 e n]

          & [x e n & 1 e n => (x,1) e n2]

            Iff-And, 406

 

      408  (x,1) e n2 => x e n & 1 e n

            Split, 407

 

      409  x e n & 1 e n => (x,1) e n2

            Split, 407

 

      410  x e n & 1 e n

            Join, 378, 8

 

      411  (x,1) e n2

            Detach, 409, 410

 

            412  x=0 & 1=0

                  Premise

 

            413  x=0

                  Split, 412

 

            414  1=0

                  Split, 412

 

            415  1=0 & ~1=0

                  Join, 414, 9

 

      416  ~[x=0 & 1=0]

            4 Conclusion, 412

 

      417  (x,1) e n2 & ~[x=0 & 1=0]

            Join, 411, 416

 

      418  (x,1) e n2'

            Detach, 404, 417

 

      419  pow'(x,1) e n

            Detach, 399, 418

 

      420  pow'(x,1) e n & x e n

            Join, 419, 378

 

      421  pow'(x,1) e n & x e n & x e n

            Join, 420, 378

 

      422  pow'(x,1) e n & x e n & x e n & ~x=0

            Join, 421, 379

 

      423  pow'(x,1)*x=x*x => pow'(x,1)=x

            Detach, 397, 422

 

      424  pow'(x,1)=x

            Detach, 423, 394

 

      425  ALL(b):[x e n & b e n & ~[x=0 & b=0]

          => pow'(x,b+1)=pow'(x,b)*x]

            U Spec, 337

 

      426  x e n & 0 e n & ~[x=0 & 0=0]

          => pow'(x,0+1)=pow'(x,0)*x

            U Spec, 425

 

            427  x=0 & 0=0

                  Premise

 

            428  x=0

                  Split, 427

 

            429  0=0

                  Split, 427

 

            430  x=0 & ~x=0

                  Join, 428, 379

 

      431  ~[x=0 & 0=0]

            4 Conclusion, 427

 

      432  x e n & 0 e n

            Join, 378, 3

 

      433  x e n & 0 e n & ~[x=0 & 0=0]

            Join, 432, 431

 

      434  pow'(x,0+1)=pow'(x,0)*x

            Detach, 426, 433

 

      435  pow'(x,1)=pow'(x,0)*x

            Substitute, 348, 434

 

      436  x=pow'(x,0)*x

            Substitute, 424, 435

 

      437  pow'(x,0)*x=x

            Sym, 436

 

      438  x e n => x*1=x

            U Spec, 15

 

      439  x*1=x

            Detach, 438, 378

 

      440  ALL(b):[x e n & b e n => x*b=b*x]

            U Spec, 17

 

      441  x e n & 1 e n => x*1=1*x

            U Spec, 440

 

      442  x e n & 1 e n

            Join, 378, 8

 

      443  x*1=1*x

            Detach, 441, 442

 

      444  1*x=x

            Substitute, 443, 439

 

      445  pow'(x,0)*x=1*x

            Substitute, 444, 437

 

      446  ALL(b):ALL(c):[pow'(x,0) e n & b e n & c e n & ~b=0 => [pow'(x,0)*b=c*b => pow'(x,0)=c]]

            U Spec, 18

 

      447  ALL(c):[pow'(x,0) e n & x e n & c e n & ~x=0 => [pow'(x,0)*x=c*x => pow'(x,0)=c]]

            U Spec, 446

 

      448  pow'(x,0) e n & x e n & 1 e n & ~x=0 => [pow'(x,0)*x=1*x => pow'(x,0)=1]

            U Spec, 447

 

      449  ALL(b):[(x,b) e n2' => pow'(x,b) e n]

            U Spec, 167

 

      450  (x,0) e n2' => pow'(x,0) e n

            U Spec, 449

 

      451  ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]

            U Spec, 48

 

      452  (x,0) e n2' <=> (x,0) e n2 & ~[x=0 & 0=0]

            U Spec, 451

 

      453  [(x,0) e n2' => (x,0) e n2 & ~[x=0 & 0=0]]

          & [(x,0) e n2 & ~[x=0 & 0=0] => (x,0) e n2']

            Iff-And, 452

 

      454  (x,0) e n2' => (x,0) e n2 & ~[x=0 & 0=0]

            Split, 453

 

      455  (x,0) e n2 & ~[x=0 & 0=0] => (x,0) e n2'

            Split, 453

 

      456  ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

            U Spec, 34

 

      457  (x,0) e n2 <=> x e n & 0 e n

            U Spec, 456

 

      458  [(x,0) e n2 => x e n & 0 e n]

          & [x e n & 0 e n => (x,0) e n2]

            Iff-And, 457

 

      459  (x,0) e n2 => x e n & 0 e n

            Split, 458

 

      460  x e n & 0 e n => (x,0) e n2

            Split, 458

 

      461  x e n & 0 e n

            Join, 378, 3

 

      462  (x,0) e n2

            Detach, 460, 461

 

      463  (x,0) e n2 & ~[x=0 & 0=0]

            Join, 462, 431

 

      464  (x,0) e n2'

            Detach, 455, 463

 

      465  pow'(x,0) e n

            Detach, 450, 464

 

      466  pow'(x,0) e n & x e n

            Join, 465, 378

 

      467  pow'(x,0) e n & x e n & 1 e n

            Join, 466, 8

 

      468  pow'(x,0) e n & x e n & 1 e n & ~x=0

            Join, 467, 379

 

      469  pow'(x,0)*x=1*x => pow'(x,0)=1

            Detach, 448, 468

 

      470  pow'(x,0)=1

            Detach, 469, 445

 

As Required:

 

471  ALL(a):[a e n & ~a=0 => pow'(a,0)=1]

      4 Conclusion, 377

 

472  ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow'(a,b) e n]

     & pow'(0,1)=0

      Join, 315, 376

 

473  ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow'(a,b) e n]

     & pow'(0,1)=0

     & ALL(a):[a e n => pow'(a,2)=a*a]

      Join, 472, 239

 

474  ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow'(a,b) e n]

     & pow'(0,1)=0

     & ALL(a):[a e n => pow'(a,2)=a*a]

     & ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0]

     => pow'(a,b+1)=pow'(a,b)*a]

      Join, 473, 337

 

As Required:   (with pow(a,2))

 

475  EXIST(pow):[ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow(a,b) e n]

     & pow(0,1)=0

     & ALL(a):[a e n => pow(a,2)=a*a]

     & ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0]

     => pow(a,b+1)=pow(a,b)*a]]

      E Gen, 474

 

476  ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow'(a,b) e n]

     & ALL(a):[a e n & ~a=0 => pow'(a,0)=1]

      Join, 315, 471

 

477  ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow'(a,b) e n]

     & ALL(a):[a e n & ~a=0 => pow'(a,0)=1]

     & pow'(0,1)=0

      Join, 476, 376

 

478  ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow'(a,b) e n]

     & ALL(a):[a e n & ~a=0 => pow'(a,0)=1]

     & pow'(0,1)=0

     & ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0]

     => pow'(a,b+1)=pow'(a,b)*a]

      Join, 477, 337

 

Equivalently and much easier to work with...

 

As Required:   (with pow(a,0))

 

479  EXIST(pow):[ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow(a,b) e n]

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

     & pow(0,1)=0

     & ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0]

     => pow(a,b+1)=pow(a,b)*a]]

      E Gen, 478