Beginning of Section SurrealMul

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.

Primitive. The name mul_SNo is a term of type set → set → set.

In Proofgold the corresponding term root is 48d054... and object id is b14730...

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.

Axiom. (mul_SNo_eq) We take the following as an axiom:

∀x, SNo x → ∀y, SNo y → x * y = SNoCut ({(w 0) * y + x * (w 1) + - (w 0) * (w 1)|w ∈ SNoL x ⨯ SNoL y} ∪ {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|z ∈ SNoR x ⨯ SNoR y}) ({(w 0) * y + x * (w 1) + - (w 0) * (w 1)|w ∈ SNoL x ⨯ SNoR y} ∪ {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|z ∈ SNoR x ⨯ SNoL y})

In Proofgold the corresponding term root is 726bd9... and proposition id is 3525c5...

Axiom. (mul_SNo_eq_2) We take the following as an axiom:

∀x y, SNo x → SNo y → ∀p : prop, (∀L R, (∀u, u ∈ L → (∀q : prop, (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, u = w0 * y + x * w1 + - w0 * w1 → q) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, u = z0 * y + x * z1 + - z0 * z1 → q) → q)) → (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, w0 * y + x * w1 + - w0 * w1 ∈ L) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, z0 * y + x * z1 + - z0 * z1 ∈ L) → (∀u, u ∈ R → (∀q : prop, (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, u = w0 * y + x * z1 + - w0 * z1 → q) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, u = z0 * y + x * w1 + - z0 * w1 → q) → q)) → (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, w0 * y + x * z1 + - w0 * z1 ∈ R) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, z0 * y + x * w1 + - z0 * w1 ∈ R) → x * y = SNoCut L R → p) → p

In Proofgold the corresponding term root is 97f72a... and proposition id is d69cc6...

Axiom. (mul_SNo_prop_1) We take the following as an axiom:

∀x, SNo x → ∀y, SNo y → ∀p : prop, (SNo (x * y) → (∀u ∈ SNoL x, ∀v ∈ SNoL y, u * y + x * v < x * y + u * v) → (∀u ∈ SNoR x, ∀v ∈ SNoR y, u * y + x * v < x * y + u * v) → (∀u ∈ SNoL x, ∀v ∈ SNoR y, x * y + u * v < u * y + x * v) → (∀u ∈ SNoR x, ∀v ∈ SNoL y, x * y + u * v < u * y + x * v) → p) → p

In Proofgold the corresponding term root is 3018e4... and proposition id is 5e4d16...

Axiom. (SNo_mul_SNo) We take the following as an axiom:

∀x y, SNo x → SNo y → SNo (x * y)

In Proofgold the corresponding term root is 7fa2e2... and proposition id is 9fd082...

Axiom. (SNo_mul_SNo_lem) We take the following as an axiom:

∀x y u v, SNo x → SNo y → SNo u → SNo v → SNo (u * y + x * v + - (u * v))

In Proofgold the corresponding term root is 632e95... and proposition id is 3a9abb...

Axiom. (SNo_mul_SNo_3) We take the following as an axiom:

∀x y z, SNo x → SNo y → SNo z → SNo (x * y * z)

In Proofgold the corresponding term root is 4fc87d... and proposition id is 8f5450...

Axiom. (mul_SNo_eq_3) We take the following as an axiom:

∀x y, SNo x → SNo y → ∀p : prop, (∀L R, SNoCutP L R → (∀u, u ∈ L → (∀q : prop, (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, u = w0 * y + x * w1 + - w0 * w1 → q) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, u = z0 * y + x * z1 + - z0 * z1 → q) → q)) → (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, w0 * y + x * w1 + - w0 * w1 ∈ L) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, z0 * y + x * z1 + - z0 * z1 ∈ L) → (∀u, u ∈ R → (∀q : prop, (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, u = w0 * y + x * z1 + - w0 * z1 → q) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, u = z0 * y + x * w1 + - z0 * w1 → q) → q)) → (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, w0 * y + x * z1 + - w0 * z1 ∈ R) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, z0 * y + x * w1 + - z0 * w1 ∈ R) → x * y = SNoCut L R → p) → p

In Proofgold the corresponding term root is 517939... and proposition id is 720ba0...

Axiom. (mul_SNo_Lt) We take the following as an axiom:

∀x y u v, SNo x → SNo y → SNo u → SNo v → u < x → v < y → u * y + x * v < x * y + u * v

In Proofgold the corresponding term root is 428b35... and proposition id is c23201...

Axiom. (mul_SNo_Le) We take the following as an axiom:

∀x y u v, SNo x → SNo y → SNo u → SNo v → u ≤ x → v ≤ y → u * y + x * v ≤ x * y + u * v

In Proofgold the corresponding term root is d9a12c... and proposition id is acb620...

Axiom. (mul_SNo_SNoL_interpolate) We take the following as an axiom:

∀x y, SNo x → SNo y → ∀u ∈ SNoL (x * y), (∃v ∈ SNoL x, ∃w ∈ SNoL y, u + v * w ≤ v * y + x * w) ∨ (∃v ∈ SNoR x, ∃w ∈ SNoR y, u + v * w ≤ v * y + x * w)

In Proofgold the corresponding term root is 7d1b52... and proposition id is f460fc...

Axiom. (mul_SNo_SNoL_interpolate_impred) We take the following as an axiom:

∀x y, SNo x → SNo y → ∀u ∈ SNoL (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoL y, u + v * w ≤ v * y + x * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoR y, u + v * w ≤ v * y + x * w → p) → p

In Proofgold the corresponding term root is 395b74... and proposition id is ad6f96...

Axiom. (mul_SNo_SNoR_interpolate) We take the following as an axiom:

∀x y, SNo x → SNo y → ∀u ∈ SNoR (x * y), (∃v ∈ SNoL x, ∃w ∈ SNoR y, v * y + x * w ≤ u + v * w) ∨ (∃v ∈ SNoR x, ∃w ∈ SNoL y, v * y + x * w ≤ u + v * w)

In Proofgold the corresponding term root is e15949... and proposition id is b67a35...

Axiom. (mul_SNo_SNoR_interpolate_impred) We take the following as an axiom:

∀x y, SNo x → SNo y → ∀u ∈ SNoR (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoR y, v * y + x * w ≤ u + v * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoL y, v * y + x * w ≤ u + v * w → p) → p

In Proofgold the corresponding term root is e5cae5... and proposition id is d1fff1...

Axiom. (mul_SNo_Subq_lem) We take the following as an axiom:

∀x y X Y Z W, ∀U U', (∀u, u ∈ U → (∀q : prop, (∀w0 ∈ X, ∀w1 ∈ Y, u = w0 * y + x * w1 + - w0 * w1 → q) → (∀z0 ∈ Z, ∀z1 ∈ W, u = z0 * y + x * z1 + - z0 * z1 → q) → q)) → (∀w0 ∈ X, ∀w1 ∈ Y, w0 * y + x * w1 + - w0 * w1 ∈ U') → (∀w0 ∈ Z, ∀w1 ∈ W, w0 * y + x * w1 + - w0 * w1 ∈ U') → U ⊆ U'

In Proofgold the corresponding term root is cc8343... and proposition id is e8bfa2...

Axiom. (mul_SNo_zeroR) We take the following as an axiom:

∀x, SNo x → x * 0 = 0

In Proofgold the corresponding term root is d279f4... and proposition id is a4f4a6...

Axiom. (mul_SNo_oneR) We take the following as an axiom:

∀x, SNo x → x * 1 = x

In Proofgold the corresponding term root is 1d2f1d... and proposition id is 5477a4...

Axiom. (mul_SNo_com) We take the following as an axiom:

∀x y, SNo x → SNo y → x * y = y * x

In Proofgold the corresponding term root is 21f7d8... and proposition id is 83d5fa...

Axiom. (mul_SNo_minus_distrL) We take the following as an axiom:

∀x y, SNo x → SNo y → (- x) * y = - x * y

In Proofgold the corresponding term root is 9beaa0... and proposition id is 3d0cd1...

Axiom. (mul_SNo_minus_distrR) We take the following as an axiom:

∀x y, SNo x → SNo y → x * (- y) = - (x * y)

In Proofgold the corresponding term root is ab775a... and proposition id is 2e7475...

Axiom. (mul_SNo_distrR) We take the following as an axiom:

∀x y z, SNo x → SNo y → SNo z → (x + y) * z = x * z + y * z

In Proofgold the corresponding term root is 6a23e5... and proposition id is 5f0382...

Axiom. (mul_SNo_distrL) We take the following as an axiom:

∀x y z, SNo x → SNo y → SNo z → x * (y + z) = x * y + x * z

In Proofgold the corresponding term root is 4e7eba... and proposition id is 2a4834...

Beginning of Section mul_SNo_assoc_lems

Variable M : set → set → set

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term M.

Hypothesis SNo_M : ∀x y, SNo x → SNo y → SNo (x * y)

Hypothesis DL : ∀x y z, SNo x → SNo y → SNo z → x * (y + z) = x * y + x * z

Hypothesis DR : ∀x y z, SNo x → SNo y → SNo z → (x + y) * z = x * z + y * z

Hypothesis IL : ∀x y, SNo x → SNo y → ∀u ∈ SNoL (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoL y, u + v * w ≤ v * y + x * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoR y, u + v * w ≤ v * y + x * w → p) → p

Hypothesis IR : ∀x y, SNo x → SNo y → ∀u ∈ SNoR (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoR y, v * y + x * w ≤ u + v * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoL y, v * y + x * w ≤ u + v * w → p) → p

Hypothesis M_Lt : ∀x y u v, SNo x → SNo y → SNo u → SNo v → u < x → v < y → u * y + x * v < x * y + u * v

Hypothesis M_Le : ∀x y u v, SNo x → SNo y → SNo u → SNo v → u ≤ x → v ≤ y → u * y + x * v ≤ x * y + u * v

Axiom. (mul_SNo_assoc_lem1) We take the following as an axiom:

∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x), u * (y * z) = (u * y) * z) → (∀v ∈ SNoS_ (SNoLev y), x * (v * z) = (x * v) * z) → (∀w ∈ SNoS_ (SNoLev z), x * (y * w) = (x * y) * w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), u * (v * z) = (u * v) * z) → (∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), u * (y * w) = (u * y) * w) → (∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), x * (v * w) = (x * v) * w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), u * (v * w) = (u * v) * w) → ∀L, (∀u ∈ L, ∀q : prop, (∀v ∈ SNoL x, ∀w ∈ SNoL (y * z), u = v * (y * z) + x * w + - v * w → q) → (∀v ∈ SNoR x, ∀w ∈ SNoR (y * z), u = v * (y * z) + x * w + - v * w → q) → q) → ∀u ∈ L, u < (x * y) * z

In Proofgold the corresponding term root is fca036... and proposition id is b70da8...

Axiom. (mul_SNo_assoc_lem2) We take the following as an axiom:

∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x), u * (y * z) = (u * y) * z) → (∀v ∈ SNoS_ (SNoLev y), x * (v * z) = (x * v) * z) → (∀w ∈ SNoS_ (SNoLev z), x * (y * w) = (x * y) * w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), u * (v * z) = (u * v) * z) → (∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), u * (y * w) = (u * y) * w) → (∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), x * (v * w) = (x * v) * w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), u * (v * w) = (u * v) * w) → ∀R, (∀u ∈ R, ∀q : prop, (∀v ∈ SNoL x, ∀w ∈ SNoR (y * z), u = v * (y * z) + x * w + - v * w → q) → (∀v ∈ SNoR x, ∀w ∈ SNoL (y * z), u = v * (y * z) + x * w + - v * w → q) → q) → ∀u ∈ R, (x * y) * z < u

In Proofgold the corresponding term root is 749b30... and proposition id is f249d3...

End of Section mul_SNo_assoc_lems

Axiom. (mul_SNo_assoc) We take the following as an axiom:

∀x y z, SNo x → SNo y → SNo z → x * (y * z) = (x * y) * z

In Proofgold the corresponding term root is 71a504... and proposition id is d322c1...

Axiom. (mul_nat_mul_SNo) We take the following as an axiom:

∀n m ∈ ω, mul_nat n m = n * m

In Proofgold the corresponding term root is da39d3... and proposition id is eb6335...

Axiom. (mul_SNo_In_omega) We take the following as an axiom:

∀n m ∈ ω, n * m ∈ ω

In Proofgold the corresponding term root is 7b6023... and proposition id is 8435a4...

Axiom. (mul_SNo_zeroL) We take the following as an axiom:

∀x, SNo x → 0 * x = 0

In Proofgold the corresponding term root is ddc2f5... and proposition id is aaf0da...

Axiom. (mul_SNo_oneL) We take the following as an axiom:

∀x, SNo x → 1 * x = x

In Proofgold the corresponding term root is 6f8b10... and proposition id is 1b25c9...

Axiom. (SNo_gt2_double_ltS) We take the following as an axiom:

∀x, SNo x → 1 < x → x + 1 < 2 * x

In Proofgold the corresponding term root is c90277... and proposition id is 73cdcc...

Axiom. (pos_mul_SNo_Lt) We take the following as an axiom:

∀x y z, SNo x → 0 < x → SNo y → SNo z → y < z → x * y < x * z

In Proofgold the corresponding term root is 674213... and proposition id is 0e949e...

Axiom. (nonneg_mul_SNo_Le) We take the following as an axiom:

∀x y z, SNo x → 0 ≤ x → SNo y → SNo z → y ≤ z → x * y ≤ x * z

In Proofgold the corresponding term root is b8880b... and proposition id is ae94b7...

Axiom. (neg_mul_SNo_Lt) We take the following as an axiom:

∀x y z, SNo x → x < 0 → SNo y → SNo z → z < y → x * y < x * z

In Proofgold the corresponding term root is 713502... and proposition id is 63326a...

Axiom. (pos_mul_SNo_Lt') We take the following as an axiom:

∀x y z, SNo x → SNo y → SNo z → 0 < z → x < y → x * z < y * z

In Proofgold the corresponding term root is a08fe5... and proposition id is 436be0...

Axiom. (mul_SNo_Lt1_pos_Lt) We take the following as an axiom:

∀x y, SNo x → SNo y → x < 1 → 0 < y → x * y < y

In Proofgold the corresponding term root is c5e733... and proposition id is 9c395c...

Axiom. (nonneg_mul_SNo_Le') We take the following as an axiom:

∀x y z, SNo x → SNo y → SNo z → 0 ≤ z → x ≤ y → x * z ≤ y * z

In Proofgold the corresponding term root is 1577b1... and proposition id is e85848...

Axiom. (mul_SNo_Le1_nonneg_Le) We take the following as an axiom:

∀x y, SNo x → SNo y → x ≤ 1 → 0 ≤ y → x * y ≤ y

In Proofgold the corresponding term root is 26eb53... and proposition id is 655b0c...

Axiom. (pos_mul_SNo_Lt2) We take the following as an axiom:

∀x y z w, SNo x → SNo y → SNo z → SNo w → 0 < x → 0 < y → x < z → y < w → x * y < z * w

In Proofgold the corresponding term root is f53e1e... and proposition id is d23a11...

Axiom. (nonneg_mul_SNo_Le2) We take the following as an axiom:

∀x y z w, SNo x → SNo y → SNo z → SNo w → 0 ≤ x → 0 ≤ y → x ≤ z → y ≤ w → x * y ≤ z * w

In Proofgold the corresponding term root is 37f3f7... and proposition id is e53b91...

Axiom. (mul_SNo_pos_pos) We take the following as an axiom:

∀x y, SNo x → SNo y → 0 < x → 0 < y → 0 < x * y

In Proofgold the corresponding term root is fda250... and proposition id is d984dc...

Axiom. (mul_SNo_pos_neg) We take the following as an axiom:

∀x y, SNo x → SNo y → 0 < x → y < 0 → x * y < 0

In Proofgold the corresponding term root is 4dec1e... and proposition id is 697e77...

Axiom. (mul_SNo_neg_pos) We take the following as an axiom:

∀x y, SNo x → SNo y → x < 0 → 0 < y → x * y < 0

In Proofgold the corresponding term root is 6f7ff5... and proposition id is 6e7adc...

Axiom. (mul_SNo_neg_neg) We take the following as an axiom:

∀x y, SNo x → SNo y → x < 0 → y < 0 → 0 < x * y

In Proofgold the corresponding term root is 86d604... and proposition id is 03517a...

Axiom. (mul_SNo_nonneg_nonneg) We take the following as an axiom:

∀x y, SNo x → SNo y → 0 ≤ x → 0 ≤ y → 0 ≤ x * y

In Proofgold the corresponding term root is 53d610... and proposition id is fc765b...

Axiom. (mul_SNo_nonpos_pos) We take the following as an axiom:

∀x y, SNo x → SNo y → x ≤ 0 → 0 < y → x * y ≤ 0

In Proofgold the corresponding term root is c597ec... and proposition id is fcd532...

Axiom. (mul_SNo_nonpos_neg) We take the following as an axiom:

∀x y, SNo x → SNo y → x ≤ 0 → y < 0 → 0 ≤ x * y

In Proofgold the corresponding term root is 54e1f5... and proposition id is 906128...

Axiom. (nonpos_mul_SNo_Le) We take the following as an axiom:

∀x y z, SNo x → x ≤ 0 → SNo y → SNo z → z ≤ y → x * y ≤ x * z

In Proofgold the corresponding term root is ebad85... and proposition id is c0938c...

Axiom. (SNo_sqr_nonneg) We take the following as an axiom:

∀x, SNo x → 0 ≤ x * x

In Proofgold the corresponding term root is d25bf0... and proposition id is 37e7dc...

Axiom. (SNo_zero_or_sqr_pos) We take the following as an axiom:

∀x, SNo x → x = 0 ∨ 0 < x * x

In Proofgold the corresponding term root is 4929cf... and proposition id is 489689...

Axiom. (SNo_pos_sqr_uniq) We take the following as an axiom:

∀x y, SNo x → SNo y → 0 < x → 0 < y → x * x = y * y → x = y

In Proofgold the corresponding term root is f41831... and proposition id is 31cc9e...

Axiom. (SNo_nonneg_sqr_uniq) We take the following as an axiom:

∀x y, SNo x → SNo y → 0 ≤ x → 0 ≤ y → x * x = y * y → x = y

In Proofgold the corresponding term root is 68d62c... and proposition id is d45b76...

Axiom. (SNo_foil) We take the following as an axiom:

∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y) * (z + w) = x * z + x * w + y * z + y * w

In Proofgold the corresponding term root is d65f34... and proposition id is ab6bae...

Axiom. (mul_SNo_minus_minus) We take the following as an axiom:

∀x y, SNo x → SNo y → (- x) * (- y) = x * y

In Proofgold the corresponding term root is cc94f8... and proposition id is 2674e5...

Axiom. (mul_SNo_com_3_0_1) We take the following as an axiom:

∀x y z, SNo x → SNo y → SNo z → x * y * z = y * x * z

In Proofgold the corresponding term root is 00a644... and proposition id is cda6e7...

Axiom. (mul_SNo_com_3b_1_2) We take the following as an axiom:

∀x y z, SNo x → SNo y → SNo z → (x * y) * z = (x * z) * y

In Proofgold the corresponding term root is 91c3e7... and proposition id is e48f00...

Axiom. (mul_SNo_com_4_inner_mid) We take the following as an axiom:

∀x y z w, SNo x → SNo y → SNo z → SNo w → (x * y) * (z * w) = (x * z) * (y * w)

In Proofgold the corresponding term root is 0bafcb... and proposition id is e23f15...

Axiom. (mul_SNo_rotate_3_1) We take the following as an axiom:

∀x y z, SNo x → SNo y → SNo z → x * y * z = z * x * y

In Proofgold the corresponding term root is 920309... and proposition id is 15ee6c...

Axiom. (mul_SNo_rotate_4_1) We take the following as an axiom:

∀x y z w, SNo x → SNo y → SNo z → SNo w → x * y * z * w = w * x * y * z

In Proofgold the corresponding term root is 6812e9... and proposition id is 5db4b6...

Axiom. (SNo_foil_mm) We take the following as an axiom:

∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + - y) * (z + - w) = x * z + - x * w + - y * z + y * w

In Proofgold the corresponding term root is c5dda6... and proposition id is 6b5f54...

Axiom. (mul_SNo_nonzero_cancel) We take the following as an axiom:

∀x y z, SNo x → x ≠ 0 → SNo y → SNo z → x * y = x * z → y = z

In Proofgold the corresponding term root is 67c26c... and proposition id is 035c5c...

Axiom. (mul_SNoCutP_lem) We take the following as an axiom:

∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → SNoCutP ({w 0 * y + x * w 1 + - w 0 * w 1|w ∈ Lx ⨯ Ly} ∪ {z 0 * y + x * z 1 + - z 0 * z 1|z ∈ Rx ⨯ Ry}) ({w 0 * y + x * w 1 + - w 0 * w 1|w ∈ Lx ⨯ Ry} ∪ {z 0 * y + x * z 1 + - z 0 * z 1|z ∈ Rx ⨯ Ly}) ∧ x * y = SNoCut ({w 0 * y + x * w 1 + - w 0 * w 1|w ∈ Lx ⨯ Ly} ∪ {z 0 * y + x * z 1 + - z 0 * z 1|z ∈ Rx ⨯ Ry}) ({w 0 * y + x * w 1 + - w 0 * w 1|w ∈ Lx ⨯ Ry} ∪ {z 0 * y + x * z 1 + - z 0 * z 1|z ∈ Rx ⨯ Ly}) ∧ ∀q : prop, (∀LxLy' RxRy' LxRy' RxLy', (∀u ∈ LxLy', ∀p : prop, (∀w ∈ Lx, ∀w' ∈ Ly, SNo w → SNo w' → w < x → w' < y → u = w * y + x * w' + - w * w' → p) → p) → (∀w ∈ Lx, ∀w' ∈ Ly, w * y + x * w' + - w * w' ∈ LxLy') → (∀u ∈ RxRy', ∀p : prop, (∀z ∈ Rx, ∀z' ∈ Ry, SNo z → SNo z' → x < z → y < z' → u = z * y + x * z' + - z * z' → p) → p) → (∀z ∈ Rx, ∀z' ∈ Ry, z * y + x * z' + - z * z' ∈ RxRy') → (∀u ∈ LxRy', ∀p : prop, (∀w ∈ Lx, ∀z ∈ Ry, SNo w → SNo z → w < x → y < z → u = w * y + x * z + - w * z → p) → p) → (∀w ∈ Lx, ∀z ∈ Ry, w * y + x * z + - w * z ∈ LxRy') → (∀u ∈ RxLy', ∀p : prop, (∀z ∈ Rx, ∀w ∈ Ly, SNo z → SNo w → x < z → w < y → u = z * y + x * w + - z * w → p) → p) → (∀z ∈ Rx, ∀w ∈ Ly, z * y + x * w + - z * w ∈ RxLy') → SNoCutP (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') → x * y = SNoCut (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') → q) → q

In Proofgold the corresponding term root is 912d2d... and proposition id is 4f23eb...

Axiom. (mul_SNoCutP_gen) We take the following as an axiom:

In Proofgold the corresponding term root is f83ad6... and proposition id is 7463da...

Axiom. (mul_SNoCut_eq) We take the following as an axiom:

∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → x * y = SNoCut ({w 0 * y + x * w 1 + - w 0 * w 1|w ∈ Lx ⨯ Ly} ∪ {z 0 * y + x * z 1 + - z 0 * z 1|z ∈ Rx ⨯ Ry}) ({w 0 * y + x * w 1 + - w 0 * w 1|w ∈ Lx ⨯ Ry} ∪ {z 0 * y + x * z 1 + - z 0 * z 1|z ∈ Rx ⨯ Ly})

In Proofgold the corresponding term root is 2ec52c... and proposition id is 0c0e72...

Axiom. (mul_SNoCut_abs) We take the following as an axiom:

∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀q : prop, (∀LxLy' RxRy' LxRy' RxLy', (∀u ∈ LxLy', ∀p : prop, (∀w ∈ Lx, ∀w' ∈ Ly, SNo w → SNo w' → w < x → w' < y → u = w * y + x * w' + - w * w' → p) → p) → (∀w ∈ Lx, ∀w' ∈ Ly, w * y + x * w' + - w * w' ∈ LxLy') → (∀u ∈ RxRy', ∀p : prop, (∀z ∈ Rx, ∀z' ∈ Ry, SNo z → SNo z' → x < z → y < z' → u = z * y + x * z' + - z * z' → p) → p) → (∀z ∈ Rx, ∀z' ∈ Ry, z * y + x * z' + - z * z' ∈ RxRy') → (∀u ∈ LxRy', ∀p : prop, (∀w ∈ Lx, ∀z ∈ Ry, SNo w → SNo z → w < x → y < z → u = w * y + x * z + - w * z → p) → p) → (∀w ∈ Lx, ∀z ∈ Ry, w * y + x * z + - w * z ∈ LxRy') → (∀u ∈ RxLy', ∀p : prop, (∀z ∈ Rx, ∀w ∈ Ly, SNo z → SNo w → x < z → w < y → u = z * y + x * w + - z * w → p) → p) → (∀z ∈ Rx, ∀w ∈ Ly, z * y + x * w + - z * w ∈ RxLy') → SNoCutP (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') → x * y = SNoCut (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') → q) → q

In Proofgold the corresponding term root is 0c7af3... and proposition id is 32f888...

Axiom. (mul_SNo_SNoCut_SNoL_interpolate) We take the following as an axiom:

∀Lx Rx Ly Ry, SNoCutP Lx Rx → SNoCutP Ly Ry → ∀x y, x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀u ∈ SNoL (x * y), (∃v ∈ Lx, ∃w ∈ Ly, u + v * w ≤ v * y + x * w) ∨ (∃v ∈ Rx, ∃w ∈ Ry, u + v * w ≤ v * y + x * w)

In Proofgold the corresponding term root is a1d92b... and proposition id is cc79b7...

Axiom. (mul_SNo_SNoCut_SNoL_interpolate_impred) We take the following as an axiom:

∀Lx Rx Ly Ry, SNoCutP Lx Rx → SNoCutP Ly Ry → ∀x y, x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀u ∈ SNoL (x * y), ∀p : prop, (∀v ∈ Lx, ∀w ∈ Ly, u + v * w ≤ v * y + x * w → p) → (∀v ∈ Rx, ∀w ∈ Ry, u + v * w ≤ v * y + x * w → p) → p

In Proofgold the corresponding term root is 600e8b... and proposition id is f55f47...

Axiom. (mul_SNo_SNoCut_SNoR_interpolate) We take the following as an axiom:

∀Lx Rx Ly Ry, SNoCutP Lx Rx → SNoCutP Ly Ry → ∀x y, x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀u ∈ SNoR (x * y), (∃v ∈ Lx, ∃w ∈ Ry, v * y + x * w ≤ u + v * w) ∨ (∃v ∈ Rx, ∃w ∈ Ly, v * y + x * w ≤ u + v * w)

In Proofgold the corresponding term root is 1f215f... and proposition id is a2fa89...

Axiom. (mul_SNo_SNoCut_SNoR_interpolate_impred) We take the following as an axiom:

∀Lx Rx Ly Ry, SNoCutP Lx Rx → SNoCutP Ly Ry → ∀x y, x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀u ∈ SNoR (x * y), ∀p : prop, (∀v ∈ Lx, ∀w ∈ Ry, v * y + x * w ≤ u + v * w → p) → (∀v ∈ Rx, ∀w ∈ Ly, v * y + x * w ≤ u + v * w → p) → p

In Proofgold the corresponding term root is 544226... and proposition id is a2323a...

End of Section SurrealMul

Beginning of Section SurrealExp

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.

Primitive. The name exp_SNo_nat is a term of type set → set → set.

In Proofgold the corresponding term root is cc5143... and object id is ea8104...

Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.

Axiom. (exp_SNo_nat_0) We take the following as an axiom:

∀x, SNo x → x ^ 0 = 1

In Proofgold the corresponding term root is c266f2... and proposition id is fe30fb...

Axiom. (exp_SNo_nat_S) We take the following as an axiom:

∀x, SNo x → ∀n, nat_p n → x ^ (ordsucc n) = x * x ^ n

In Proofgold the corresponding term root is 6b5ef9... and proposition id is ae55b7...

Axiom. (exp_SNo_nat_1) We take the following as an axiom:

∀x, SNo x → x ^ 1 = x

In Proofgold the corresponding term root is 9a6103... and proposition id is d52b56...

Axiom. (exp_SNo_nat_2) We take the following as an axiom:

∀x, SNo x → x ^ 2 = x * x

In Proofgold the corresponding term root is a18be1... and proposition id is ea69f6...

Axiom. (SNo_sqr_nonneg') We take the following as an axiom:

∀x, SNo x → 0 ≤ x ^ 2

In Proofgold the corresponding term root is 3934ed... and proposition id is d74d6b...

Axiom. (SNo_zero_or_sqr_pos') We take the following as an axiom:

∀x, SNo x → x = 0 ∨ 0 < x ^ 2

In Proofgold the corresponding term root is e0060a... and proposition id is b58186...

Axiom. (SNo_exp_SNo_nat) We take the following as an axiom:

∀x, SNo x → ∀n, nat_p n → SNo (x ^ n)

In Proofgold the corresponding term root is 7a77b4... and proposition id is f317bf...

Axiom. (nat_exp_SNo_nat) We take the following as an axiom:

∀x, nat_p x → ∀n, nat_p n → nat_p (x ^ n)

In Proofgold the corresponding term root is 14de73... and proposition id is 39327e...

Axiom. (eps_ordsucc_half_add) We take the following as an axiom:

∀n, nat_p n → eps_ (ordsucc n) + eps_ (ordsucc n) = eps_ n

In Proofgold the corresponding term root is 6f06cd... and proposition id is 1a029d...

Axiom. (eps_1_half_eq1) We take the following as an axiom:

eps_ 1 + eps_ 1 = 1

In Proofgold the corresponding term root is 356e75... and proposition id is 2163a7...

Axiom. (eps_1_half_eq2) We take the following as an axiom:

2 * eps_ 1 = 1

In Proofgold the corresponding term root is 69f0c6... and proposition id is 95d3cb...

Axiom. (double_eps_1) We take the following as an axiom:

∀x y z, SNo x → SNo y → SNo z → x + x = y + z → x = eps_ 1 * (y + z)

In Proofgold the corresponding term root is 42def0... and proposition id is 896286...

Axiom. (exp_SNo_1_bd) We take the following as an axiom:

∀x, SNo x → 1 ≤ x → ∀n, nat_p n → 1 ≤ x ^ n

In Proofgold the corresponding term root is a5c549... and proposition id is 002e5b...

Axiom. (exp_SNo_2_bd) We take the following as an axiom:

∀n, nat_p n → n < 2 ^ n

In Proofgold the corresponding term root is 1297d1... and proposition id is 88dd94...

Axiom. (mul_SNo_eps_power_2) We take the following as an axiom:

∀n, nat_p n → eps_ n * 2 ^ n = 1

In Proofgold the corresponding term root is 6921ff... and proposition id is e69e44...

Axiom. (eps_bd_1) We take the following as an axiom:

∀n ∈ ω, eps_ n ≤ 1

In Proofgold the corresponding term root is b781ab... and proposition id is 1165c4...

Axiom. (mul_SNo_eps_power_2') We take the following as an axiom:

∀n, nat_p n → 2 ^ n * eps_ n = 1

In Proofgold the corresponding term root is 721eb5... and proposition id is ce9559...

Axiom. (exp_SNo_nat_mul_add) We take the following as an axiom:

∀x, SNo x → ∀m, nat_p m → ∀n, nat_p n → x ^ m * x ^ n = x ^ (m + n)

In Proofgold the corresponding term root is 3333a9... and proposition id is f04547...

Axiom. (exp_SNo_nat_mul_add') We take the following as an axiom:

∀x, SNo x → ∀m n ∈ ω, x ^ m * x ^ n = x ^ (m + n)

In Proofgold the corresponding term root is 364123... and proposition id is bde099...

Axiom. (exp_SNo_nat_pos) We take the following as an axiom:

∀x, SNo x → 0 < x → ∀n, nat_p n → 0 < x ^ n

In Proofgold the corresponding term root is 795806... and proposition id is 6538ad...

Axiom. (mul_SNo_eps_eps_add_SNo) We take the following as an axiom:

∀m n ∈ ω, eps_ m * eps_ n = eps_ (m + n)

In Proofgold the corresponding term root is 857b85... and proposition id is ea6877...

Axiom. (SNoS_omega_Lev_equip) We take the following as an axiom:

∀n, nat_p n → equip {x ∈ SNoS_ ω|SNoLev x = n} (2 ^ n)

In Proofgold the corresponding term root is 2712ea... and proposition id is 81ef79...

Axiom. (SNoS_finite) We take the following as an axiom:

∀n ∈ ω, finite (SNoS_ n)

In Proofgold the corresponding term root is b18610... and proposition id is c5538e...

Axiom. (SNoS_omega_SNoL_finite) We take the following as an axiom:

∀x ∈ SNoS_ ω, finite (SNoL x)

In Proofgold the corresponding term root is bf4159... and proposition id is 473468...

Axiom. (SNoS_omega_SNoR_finite) We take the following as an axiom:

∀x ∈ SNoS_ ω, finite (SNoR x)

In Proofgold the corresponding term root is c352d0... and proposition id is eafcc9...

End of Section SurrealExp