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.
(*** $I sig/Part1.mgs ***)
(*** $I sig/Part2.mgs ***)
(*** $I sig/Part3.mgs ***)
(*** $I sig/Part4.mgs ***)
(*** $I sig/Part5.mgs ***)
(*** Part 6 ***)
L14
Definition. We define mul_SNo to be SNo_rec2 (λx y m ⇒ SNoCut ({m (w 0) y + m x (w 1) + - m (w 0) (w 1)|w ∈ SNoL x ⨯ SNoL y} ∪ {m (z 0) y + m x (z 1) + - m (z 0) (z 1)|z ∈ SNoR x ⨯ SNoR y}) ({m (w 0) y + m x (w 1) + - m (w 0) (w 1)|w ∈ SNoL x ⨯ SNoR y} ∪ {m (z 0) y + m x (z 1) + - m (z 0) (z 1)|z ∈ SNoR x ⨯ SNoL y})) 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.
L25
Theorem. (mul_SNo_eq)
∀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...
Proof:
Proof not loaded.
L185
Theorem. (mul_SNo_eq_2)
∀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...
Proof:
Proof not loaded.
L299
Theorem. (mul_SNo_prop_1)
∀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...
Proof:
Proof not loaded.
L1340
Theorem. (SNo_mul_SNo)
∀x y, SNo x → SNo y → SNo (x * y)
In Proofgold the corresponding term root is 7fa2e2... and proposition id is 9fd082...
Proof:
Proof not loaded.
L1345
Theorem. (SNo_mul_SNo_lem)
∀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...
Proof:
Proof not loaded.
L1359
Theorem. (SNo_mul_SNo_3)
∀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...
Proof:
Proof not loaded.
L1368
Theorem. (mul_SNo_eq_3)
∀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...
Proof:
Proof not loaded.
L1609
Theorem. (mul_SNo_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
In Proofgold the corresponding term root is 428b35... and proposition id is c23201...
Proof:
Proof not loaded.
L1965
Theorem. (mul_SNo_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
In Proofgold the corresponding term root is d9a12c... and proposition id is acb620...
Proof:
Proof not loaded.
L1984
Theorem. (mul_SNo_SNoL_interpolate)
∀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...
Proof:
Proof not loaded.
L2166
Theorem. (mul_SNo_SNoL_interpolate_impred)
∀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...
Proof:
Proof not loaded.
L2188
Theorem. (mul_SNo_SNoR_interpolate)
∀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...
Proof:
Proof not loaded.
L2370
Theorem. (mul_SNo_SNoR_interpolate_impred)
∀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...
Proof:
Proof not loaded.
L2392
Theorem. (mul_SNo_Subq_lem)
∀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...
Proof:
Proof not loaded.
L2415
Theorem. (mul_SNo_zeroR)
∀x, SNo x → x * 0 = 0
In Proofgold the corresponding term root is d279f4... and proposition id is a4f4a6...
Proof:
Proof not loaded.
L2457
Theorem. (mul_SNo_oneR)
∀x, SNo x → x * 1 = x
In Proofgold the corresponding term root is 1d2f1d... and proposition id is 5477a4...
Proof:
Proof not loaded.
L2585
Theorem. (mul_SNo_com)
∀x y, SNo x → SNo y → x * y = y * x
In Proofgold the corresponding term root is 21f7d8... and proposition id is 83d5fa...
Proof:
Proof not loaded.
L2744
Theorem. (mul_SNo_minus_distrL)
∀x y, SNo x → SNo y → (- x) * y = - x * y
In Proofgold the corresponding term root is 9beaa0... and proposition id is 3d0cd1...
Proof:
Proof not loaded.
L3136
Theorem. (mul_SNo_minus_distrR)
∀x y, SNo x → SNo y → x * (- y) = - (x * y)
In Proofgold the corresponding term root is ab775a... and proposition id is 2e7475...
Proof:
Proof not loaded.
L3143
Theorem. (mul_SNo_distrR)
∀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...
Proof:
Proof not loaded.
L4456
Theorem. (mul_SNo_distrL)
∀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...
Proof:
Proof not loaded.
Beginning of Section mul_SNo_assoc_lems
L4471
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.
L4474
Hypothesis SNo_M : ∀x y, SNo x → SNo y → SNo (x * y)
L4476
Hypothesis DL : ∀x y z, SNo x → SNo y → SNo z → x * (y + z) = x * y + x * z
L4478
Hypothesis DR : ∀x y z, SNo x → SNo y → SNo z → (x + y) * z = x * z + y * z
L4479
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
L4484
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
L4489
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
L4492
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
L4494
Theorem. (mul_SNo_assoc_lem1)
∀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...
Proof:
Proof not loaded.
L4954
Theorem. (mul_SNo_assoc_lem2)
∀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...
Proof:
Proof not loaded.
End of Section mul_SNo_assoc_lems
L5439
Theorem. (mul_SNo_assoc)
∀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...
Proof:
Proof not loaded.
L5654
Theorem. (mul_nat_mul_SNo)
∀n m ∈ ω, mul_nat n m = n * m
In Proofgold the corresponding term root is da39d3... and proposition id is eb6335...
Proof:
Proof not loaded.
L5696
Theorem. (mul_SNo_In_omega)
∀n m ∈ ω, n * m ∈ ω
In Proofgold the corresponding term root is 7b6023... and proposition id is 8435a4...
Proof:
Proof not loaded.
L5702
Theorem. (mul_SNo_zeroL)
∀x, SNo x → 0 * x = 0
In Proofgold the corresponding term root is ddc2f5... and proposition id is aaf0da...
Proof:
Proof not loaded.
L5708
Theorem. (mul_SNo_oneL)
∀x, SNo x → 1 * x = x
In Proofgold the corresponding term root is 6f8b10... and proposition id is 1b25c9...
Proof:
Proof not loaded.
L5714
Theorem. (SNo_gt2_double_ltS)
∀x, SNo x → 1 < x → x + 1 < 2 * x
In Proofgold the corresponding term root is c90277... and proposition id is 73cdcc...
Proof:
Proof not loaded.
L5726
Theorem. (pos_mul_SNo_Lt)
∀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...
Proof:
Proof not loaded.
L5744
Theorem. (nonneg_mul_SNo_Le)
∀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...
Proof:
Proof not loaded.
L5762
Theorem. (neg_mul_SNo_Lt)
∀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...
Proof:
Proof not loaded.
L5780
Theorem. (pos_mul_SNo_Lt')
∀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...
Proof:
Proof not loaded.
L5787
Theorem. (mul_SNo_Lt1_pos_Lt)
∀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...
Proof:
Proof not loaded.
L5794
Theorem. (nonneg_mul_SNo_Le')
∀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...
Proof:
Proof not loaded.
L5801
Theorem. (mul_SNo_Le1_nonneg_Le)
∀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...
Proof:
Proof not loaded.
L5808
Theorem. (pos_mul_SNo_Lt2)
∀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...
Proof:
Proof not loaded.
L5823
Theorem. (nonneg_mul_SNo_Le2)
∀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...
Proof:
Proof not loaded.
L5838
Theorem. (mul_SNo_pos_pos)
∀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...
Proof:
Proof not loaded.
L5854
Theorem. (mul_SNo_pos_neg)
∀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...
Proof:
Proof not loaded.
L5868
Theorem. (mul_SNo_neg_pos)
∀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...
Proof:
Proof not loaded.
L5882
Theorem. (mul_SNo_neg_neg)
∀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...
Proof:
Proof not loaded.
L5898
Theorem. (mul_SNo_nonneg_nonneg)
∀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...
Proof:
Proof not loaded.
L5914
Theorem. (mul_SNo_nonpos_pos)
∀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...
Proof:
Proof not loaded.
L5931
Theorem. (mul_SNo_nonpos_neg)
∀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...
Proof:
Proof not loaded.
L5948
Theorem. (nonpos_mul_SNo_Le)
∀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...
Proof:
Proof not loaded.
L5976
Theorem. (SNo_sqr_nonneg)
∀x, SNo x → 0 ≤ x * x
In Proofgold the corresponding term root is d25bf0... and proposition id is 37e7dc...
Proof:
Proof not loaded.
L5992
Theorem. (SNo_zero_or_sqr_pos)
∀x, SNo x → x = 0 ∨ 0 < x * x
In Proofgold the corresponding term root is 4929cf... and proposition id is 489689...
Proof:
Proof not loaded.
L6010
Theorem. (SNo_pos_sqr_uniq)
∀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...
Proof:
Proof not loaded.
L6029
Theorem. (SNo_nonneg_sqr_uniq)
∀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...
Proof:
Proof not loaded.
L6054
Theorem. (SNo_foil)
∀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...
Proof:
Proof not loaded.
L6080
Theorem. (mul_SNo_minus_minus)
∀x y, SNo x → SNo y → (- x) * (- y) = x * y
In Proofgold the corresponding term root is cc94f8... and proposition id is 2674e5...
Proof:
Proof not loaded.
L6089
Theorem. (mul_SNo_com_3_0_1)
∀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...
Proof:
Proof not loaded.
L6099
Theorem. (mul_SNo_com_3b_1_2)
∀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...
Proof:
Proof not loaded.
L6109
Theorem. (mul_SNo_com_4_inner_mid)
∀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...
Proof:
Proof not loaded.
L6121
Theorem. (mul_SNo_rotate_3_1)
∀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...
Proof:
Proof not loaded.
L6135
Theorem. (mul_SNo_rotate_4_1)
∀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...
Proof:
Proof not loaded.
L6143
Theorem. (SNo_foil_mm)
∀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...
Proof:
Proof not loaded.
L6158
Theorem. (mul_SNo_nonzero_cancel)
∀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...
Proof:
Proof not loaded.
L6194
Theorem. (mul_SNoCutP_lem)
∀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...
Proof:
Proof not loaded.
L7487
Theorem. (mul_SNoCutP_gen)
∀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})
In Proofgold the corresponding term root is f83ad6... and proposition id is 7463da...
Proof:
Proof not loaded.
L7504
Theorem. (mul_SNoCut_eq)
∀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...
Proof:
Proof not loaded.
L7521
Theorem. (mul_SNoCut_abs)
∀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...
Proof:
Proof not loaded.
L7546
Theorem. (mul_SNo_SNoCut_SNoL_interpolate)
∀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...
Proof:
Proof not loaded.
L7786
Theorem. (mul_SNo_SNoCut_SNoL_interpolate_impred)
∀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...
Proof:
Proof not loaded.
L7812
Theorem. (mul_SNo_SNoCut_SNoR_interpolate)
∀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...
Proof:
Proof not loaded.
L8052
Theorem. (mul_SNo_SNoCut_SNoR_interpolate_impred)
∀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...
Proof:
Proof not loaded.
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.
L8086
Definition. We define exp_SNo_nat to be λn m : set ⇒ nat_primrec 1 (λ_ r ⇒ n * r) m 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.
L8090
Theorem. (exp_SNo_nat_0)
∀x, SNo x → x ^ 0 = 1
In Proofgold the corresponding term root is c266f2... and proposition id is fe30fb...
Proof:
Proof not loaded.
L8095
Theorem. (exp_SNo_nat_S)
∀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...
Proof:
Proof not loaded.
L8100
Theorem. (exp_SNo_nat_1)
∀x, SNo x → x ^ 1 = x
In Proofgold the corresponding term root is 9a6103... and proposition id is d52b56...
Proof:
Proof not loaded.
L8109
Theorem. (exp_SNo_nat_2)
∀x, SNo x → x ^ 2 = x * x
In Proofgold the corresponding term root is a18be1... and proposition id is ea69f6...
Proof:
Proof not loaded.
L8117
Theorem. (SNo_sqr_nonneg')
∀x, SNo x → 0 ≤ x ^ 2
In Proofgold the corresponding term root is 3934ed... and proposition id is d74d6b...
Proof:
Proof not loaded.
L8123
Theorem. (SNo_zero_or_sqr_pos')
∀x, SNo x → x = 0 ∨ 0 < x ^ 2
In Proofgold the corresponding term root is e0060a... and proposition id is b58186...
Proof:
Proof not loaded.
L8129
Theorem. (SNo_exp_SNo_nat)
∀x, SNo x → ∀n, nat_p n → SNo (x ^ n)
In Proofgold the corresponding term root is 7a77b4... and proposition id is f317bf...
Proof:
Proof not loaded.
L8139
Theorem. (nat_exp_SNo_nat)
∀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...
Proof:
Proof not loaded.
L8154
Theorem. (eps_ordsucc_half_add)
∀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...
Proof:
Proof not loaded.
L8314
Theorem. (eps_1_half_eq1)
eps_ 1 + eps_ 1 = 1
In Proofgold the corresponding term root is 356e75... and proposition id is 2163a7...
Proof:
Proof not loaded.
L8320
Theorem. (eps_1_half_eq2)
2 * eps_ 1 = 1
In Proofgold the corresponding term root is 69f0c6... and proposition id is 95d3cb...
Proof:
Proof not loaded.
L8329
Theorem. (double_eps_1)
∀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...
Proof:
Proof not loaded.
L8350
Theorem. (exp_SNo_1_bd)
∀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...
Proof:
Proof not loaded.
L8370
Theorem. (exp_SNo_2_bd)
∀n, nat_p n → n < 2 ^ n
In Proofgold the corresponding term root is 1297d1... and proposition id is 88dd94...
Proof:
Proof not loaded.
L8404
Theorem. (mul_SNo_eps_power_2)
∀n, nat_p n → eps_ n * 2 ^ n = 1
In Proofgold the corresponding term root is 6921ff... and proposition id is e69e44...
Proof:
Proof not loaded.
L8429
Theorem. (eps_bd_1)
∀n ∈ ω, eps_ n ≤ 1
In Proofgold the corresponding term root is b781ab... and proposition id is 1165c4...
Proof:
Proof not loaded.
L8447
Theorem. (mul_SNo_eps_power_2')
∀n, nat_p n → 2 ^ n * eps_ n = 1
In Proofgold the corresponding term root is 721eb5... and proposition id is ce9559...
Proof:
Proof not loaded.
L8456
Theorem. (exp_SNo_nat_mul_add)
∀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...
Proof:
Proof not loaded.
L8488
Theorem. (exp_SNo_nat_mul_add')
∀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...
Proof:
Proof not loaded.
L8493
Theorem. (exp_SNo_nat_pos)
∀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...
Proof:
Proof not loaded.
L8507
Theorem. (mul_SNo_eps_eps_add_SNo)
∀m n ∈ ω, eps_ m * eps_ n = eps_ (m + n)
In Proofgold the corresponding term root is 857b85... and proposition id is ea6877...
Proof:
Proof not loaded.
L8557
Theorem. (SNoS_omega_Lev_equip)
∀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...
Proof:
Proof not loaded.
L8954
Theorem. (SNoS_finite)
∀n ∈ ω, finite (SNoS_ n)
In Proofgold the corresponding term root is b18610... and proposition id is c5538e...
Proof:
Proof not loaded.
L9006
Theorem. (SNoS_omega_SNoL_finite)
∀x ∈ SNoS_ ω, finite (SNoL x)
In Proofgold the corresponding term root is bf4159... and proposition id is 473468...
Proof:
Proof not loaded.
L9026
Theorem. (SNoS_omega_SNoR_finite)
∀x ∈ SNoS_ ω, finite (SNoR x)
In Proofgold the corresponding term root is c352d0... and proposition id is eafcc9...
Proof:
Proof not loaded.
End of Section SurrealExp