show: AR => pow(3, 2) = 9

0H: AR

1 > 0    //cnj out from AR

1 Î N    //cnj out AR

(x Î N => x Î R)(x)    //cnj out AR

1 Î N => 1 Î R    //gen out

1 Î R    //cnd out

((x Î R & y Î R & z Î R & x > y) => x + z > y + z)(x, y, z)    //cnj out AR

(1 Î R & 0 Î R & 1 Î R & 1 > 0) => 1 + 1 > 0 + 1    //gen out

0 Î R    //cnj out AR

1 Î R & 0 Î R    //cnj in

1 Î R & 0 Î R & 1 Î R    //cnj in

1 Î R & 0 Î R & 1 Î R & 1 > 0    //cnj in

1 + 1 > 0 + 1    //cnd out

1 + 1 = 2    //cnj out AR

2 > 0 + 1    //=

(x Î R => 0 + x = x)(x)    //cnj out AR

1 Î R => 0 + 1 = 1    //gen out

1 Î R    //rep

0 + 1 = 1    //cnd out

2 > 1    //=

((x Î N & y Î N) => x + y Î N)(x)    //cnj out AR

(1 Î N & 1 Î N) => 1 + 1 Î N    //gen out

1 Î N & 1 Î N    //cnj in

1 + 1 Î N    //cnd out

1 + 1 = 2    //rep

2 Î N    //=

(2 Î N & 1 Î N) => 2 + 1 Î N    //gen out

2 Î N & 1 Î N    //cnd in

2 + 1 Î N    //cnd out

3 = 2 + 1    //cnj out AR

3 Î N    //=

(x Î N => x Î R)(x)    //rep

2 Î N => 2 Î R    //gen out

2 Î N    //rep

2 Î R    //cnd out

3 Î N => 3 Î R    //gen out

3 Î N    //rep

3 Î R    //cnd out

(x Î R => - x Î R)(x)    //cnj out AR

1 Î R => - 1 Î R    //gen out

1 Î R    //rep

- 1 Î R    //cnd out

((x Î R & y Î R) => x - y = x + -y)(x, y)    //cnj out AR

(2 is R & 1 Î R) => 2 - 1 = 2 + -1    //gen out

2 Î R & 1 Î R    //cnj in

2 - 1 = 2 + -1    //cnd out

2 - 1 = (2) + -1    //pren in

2 = 1 + 1    //rep

2 - 1 = (1 + 1) + -1    //=

//cnj out AR

((x Î R & y Î R & z Î R) => (x + y) + z = x + (y + z))(x, y, z)

(1 Î R & 1 Î R & -1 Î R) => (1 + 1) + -1 = 1 + (1 + -1)    //gen out

1 Î R & 1 Î R    //cnj in

1 Î R & 1 Î R & -1 Î R    //cnj in

(1 + 1) + -1 = 1 + (1 + -1)    //cnd out

(x Î R => x + - x = 0)(x)    //cnj out AR

1 Î R => 1 + -1 = 0    //gen out

1 is R    //rep

1 + -1 = 0    //cnd out

(1 + 1) + -1 = 1 + (1 + -1)    //rep

(1 + 1) + -1 = 1 + (0)    //=

(1 + 1) + -1 = 1 + 0    //prn out

(x Î R => x + 0 = x)(x)    //cnj out AR

1 Î R => 1 + 0 = 1    //gen out

1 Î R    //rep

1 + 0 = 1    //rep

(1 + 1) + -1 = 1 + 0    //rep

(1 + 1) + -1 = 1    //=

2 - 1 = (1 + 1) + -1    //rep

2 - 1 = 1    //=

((x Î R & y Î R & z Î R & x > y) => x + z > y + z)(x, y, z)    //rep

(2 Î R & 1 Î R & 1 Î R & 2 > 1) => 2 + 1 > 1 + 1    //gen out

2 Î R & 1 Î R    //cnj in

2 Î R & 1 Î R & 1 Î R    //cnj in

2 Î R & 1 Î R & 1 Î R & 2 > 1    //cnj in

2 + 1 > 1 + 1    //cnd out

3 = 2 + 1    //cnj out AR

3 > 1 + 1    //=

2 = 1 + 1    //cnj out AR

3 > 2    //=

((x Î R & y Î R) => x - y = x + -y)(x, y)    //rep

(3 Î R & 1 Î R) => 3 - 1 = 3 + -1    //gen out

3 Î R & 1 Î R    //cnj in

3 - 1 = 3 + -1    //cnd out

3 = 2 + 1    //rep

3 - 1 = (3) + -1    //pren in

3 - 1 = (2 + 1) + -1    //=

((x Î R & y Î R & z Î R) => (x + y) + z = x + (y + z))(x, y, z)    //rep

(2 Î R & 1 Î R & -1 Î R) => (2 + 1) + -1 = 2 + (1 + -1)    //gen out

2 Î R & 1 Î R    //cnj in

2 Î R & 1 Î R & -1 Î R    //cnj in

(2 + 1) + -1 = 2 + (1 + -1)    //cnd out

1 + -1 = 0    //rep

(2 + 1) + -1 = 2 + (0)    //=

(2 + 1) + -1 = 2 + 0    //pren out

(x Î R => x + 0 = x)(x)    //rep

2 Î R => 2 + 0 = 2    //gen out

2 Î R    //rep

2 + 0 = 2    //cnd out

(2 + 1) + -1 = (2 + 0)    //pren in

(2 + 1) + -1 = (2)    //=

(2 + 1) + -1 = 2    //pren out

3 - 1 = [(2 + 1) + -1]    //pren in

3 - 1 = [2]    //=

3 - 1 = 2    //pren out

3 = 1 + 2    //cnj out AR

((x Î R & y Î R) => x + y = y + x)(x, y)    //cnj out AR

(3 Î R & 3 Î R) => 3 + 3 = 3 + 3    //gen out

3 Î R & 3 Î R    //rep

3 + 3 = 3 + 3    //cnd out

3 + 3 = 3 + (3)    //pren in

3 + 3 = 3 + (1 + 2)    //=

((x Î R & y Î R & z Î R) => (x + y) + z = x + (y + z))(x, y, z)    //rep

((3 Î R & 1 Î R & 2 Î R) => (3 + 1) + 2 = 3 + (1 + 2)    // gen out

3 Î R & 1 Î R    //cnj in

3 Î R & 1 Î R & 2 Î R    //cnj in

(3 + 1) + 2 = 3 + (1 + 2)    //cnd out

3 + 3 = 3 + (1 + 2)    //rep

3 + 3 = (3 + 1) + 2    //=

3 + 1 = 4    //cnj out AR

3 + 3 = (4) + 2    //=

3 + 3 = 4 + 2    //pren out

3 + 3 = 4 + (2)    //pren in

2 = 1 + 1    //rep

3 + 3 = 4 + (1 + 1)    //=

((x Î R & y Î R) => x + y Î R)(x, y)    //cnj out AR

(3 Î R & 1 Î R) => 3 + 1 Î R    //cnd out

3 Î R & 1 Î R    //cnj in

3 + 1 Î R    //cnd out

3 + 1 = 4    //rep

4 Î R    //=

((4 Î R & 1 Î R & 1 Î R) => (4 + 1) + 1 = 4 + (1 + 1)    //gen out

4 Î R & 1 Î R    //cnj in

4 Î R & 1 Î R & 1 Î R    //cnj in

(4 + 1) + 1 = 4 + (1 + 1)    //cnd out

3 + 3 = 4 + (1 + 1)    //rep

3 + 3 = (4 + 1) + 1    //=

5 = 4 + 1    //cnj out AR

3 + 3 = (5) + 1    //=

3 + 3 = 5 + 1    //pren out

6 = 5 + 1    //cnj out AR

3 + 3 = 6    //=

(x Î N => x Î R)(x)    //rep

6 Î N => 6 Î R    //gen out

6 Î N    //cnj out AR

6 Î R    //cnd out

7 Î N => 7 Î R    //gen out

7 Î N    //cnj out AR

7 Î R    //cnd out

((x Î R & y Î R) => x + y = y + x)(x, y)    //rep

(3 Î R & 6 Î R) => 3 + 6 = 6 + 3    //gen out

3 Î R & 6 Î R    //cnj in

3 + 6 = 6 + 3    //cnd out

3 = 1 + 2    //cnj out AR

3 + 6 = 6 + (3)    //pren in

3 + 6 = 6 + (1 + 2)    //=

((x Î R & y Î R & z Î R) => (x + y) + z = x + (y + z))(x, y, z)    //rep

(6 Î R & 1 Î R & 2 Î R) => (6 + 1) + 2 = 6 + (1 + 2)    //gen out

6 Î R & 1 Î R    //cnj out

6 Î R & 1 Î R & 2 Î R    //cnj out

(6 + 1) + 2 = 6 + (1 + 2)    //cnd out

3 + 6 = 6 + (1 + 2)    //rep

3 + 6 = (6 + 1) + 2    //=

7 = 6 + 1    //cnj out AR

3 + 6 = (7) + 2    //=

3 + 6 = 7 + 2    //pren out

3 + 6 = 7 + (2)    //pren in

2 = 1 + 1    //rep

3 + 6 = 7 + (1 + 1)    //=

(7 Î R & 1 Î R & 1 Î R) => (7 + 1) + 1 = 7 + (1 + 1)    //gen out

7 Î R & 1 Î R    //cnj in

7 Î R & 1 Î R & 1 Î R    //cnj in

(7 + 1) + 1 = 7 + (1 + 1)    //cnd out

3 + 6 = 7 + (1 + 1)    //rep

3 + 6 = (7 + 1) + 1    //=

8 = 7 + 1    //cnj out AR

3 + 6 = (8) + 1    //=

3 + 6 = 8 + 1    //pren out

9 = 8 + 1    //cnj out AR

3 + 6 = 9    //=

//--------------------------MN-------------------------------

//cnj out AR

((x Î R & y Î R & z Î R & x > y & y > z) => x > z)(x, y, z)

(3 Î R & 2 Î R & 1 Î R & 3 > 2 & 2 > 1) => 3 > 1    //gen out

3 Î R & 2 Î R    //cnj in

3 Î R & 2 Î R & 1 Î R    //cnj in

3 Î R & 2 Î R & 1 Î R & 3 > 2    //cnj in

3 Î R & 2 Î R & 1 Î R & 3 > 2 & 2 > 1    //cnj in

3 > 1    //cnd out

// & out from AR

((x Î N & y Î N & y >1) => pow(x, y) = x * pow(x, y - 1))(x, y)

(3 Î N & 2 Î N & 2 >1) => pow(3, 2) = 3 * pow(3, 2 - 1)    //gen out

3 Î N    //rep

2 Î N    //rep

2 > 1    //rep

3 Î N & 2 Î N    //cnj in

3 Î N & 2 Î N & 2 >1    //cnj in

pow(3, 2) = 3 * pow(3, 2 - 1)    //cnd out

2 - 1 = 1    //rep

pow(3, 2) = 3 * pow(3, 1)    //=

(x Î N => pow(x, 1) = x)(x)    //cnj out from AR

3 Î N => pow(3, 1) = 3    //gen out

3 Î N    //rep

pow(3, 1) = 3    //cnd out

pow(3, 2) = 3 * pow(3, 1)    //rep

pow(3, 2) = 3 * 3    //=

((x Î N & y Î N) => x * y = mlt(x, y))(x, y)    //cnj out from AR

(3 Î N & 3 Î N) => 3 * 3 = mlt(3, 3)    //gen out

3 Î N & 3 Î N    //cnj in

3 * 3 = mlt(3, 3)    //cnd out

pow(3, 2) = mlt(3, 3)    //=

(x Î N => mlt(x, 1) = x)(x)    //cnj out AR

3 Î N => mlt(3, 1) = 3    //gen out

3 Î N    //rep

mlt(3, 1) = 3    //cnd out

//& out from AR

((x Î N & y Î N & y > 1) => mlt(x, y) = x + mlt(x, y - 1))(x, y)

(3 Î N & 3 Î N & 3 > 1) => mlt(3, 3) = 3 + mlt(3, 3 - 1)    //gen out

3 > 1    //rep

3 Î N & 3 Î N & 3 > 1    //cnj out

mlt(3, 3) = 3 + mlt(3, 3 - 1)    //cnd out

3 - 1 = 2    //rep

mlt(3, 3) = 3 + mlt(3, 2)    //=

(3 Î N & 2 Î N & 2 > 1) => mlt(3, 2) = 3 + mlt(3, 2 - 1)    //gen out

3 Î N & 2 Î N & 2 > 1    //rep

mlt(3, 2) = 3 + mlt(3, 2 - 1)    // cnd out

2 - 1 = 1    //rep

mlt(3, 2) = 3 + mlt(3, 1)    //=

mlt(3, 1) = 3    //rep

mlt(3, 2) = 3 + 3    //=

3 + 3 = 6    // rep

mlt(3, 2) = 6    //=

mlt(3, 3) = 3 + mlt(3, 2)    //rep

mlt(3, 3) = 3 + 6    //=

3 + 6 = 9    //rep

mlt(3, 3) = 9    //=

pow(3, 2) = mlt(3, 3)    //rep

pow(3, 2) = 9    //=

-0H: AR => pow(3, 2) = 9

note: AR is a conjunction of all the axioms of the real numbers. I use AR as a hypothesis.

this exersize demonstrates recursion