Beginning of Section SurrealDiv

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.

Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.

Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.

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

Definition. We define SNoL_pos to be λx ⇒ {w ∈ SNoL x|0 < w} of type set → set.

In Proofgold the corresponding term root is 399f06... and object id is 65d5ad...

Theorem. (SNo_recip_pos_pos)

∀x xi, SNo x → SNo xi → 0 < x → x * xi = 1 → 0 < xi

In Proofgold the corresponding term root is 8f0063... and proposition id is 5b48db...

Proof:
Proof not loaded.

Theorem. (SNo_recip_lem1)

∀x x' x'i y y', SNo x → 0 < x → x' ∈ SNoL_pos x → SNo x'i → x' * x'i = 1 → SNo y → x * y < 1 → SNo y' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i → 1 < x * y'

In Proofgold the corresponding term root is 761151... and proposition id is b197c8...

Proof:
Proof not loaded.

Theorem. (SNo_recip_lem2)

∀x x' x'i y y', SNo x → 0 < x → x' ∈ SNoL_pos x → SNo x'i → x' * x'i = 1 → SNo y → 1 < x * y → SNo y' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i → x * y' < 1

In Proofgold the corresponding term root is 423150... and proposition id is 1a06f3...

Proof:
Proof not loaded.

Theorem. (SNo_recip_lem3)

∀x x' x'i y y', SNo x → 0 < x → x' ∈ SNoR x → SNo x'i → x' * x'i = 1 → SNo y → x * y < 1 → SNo y' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i → x * y' < 1

In Proofgold the corresponding term root is b6e635... and proposition id is 22668c...

Proof:
Proof not loaded.

Theorem. (SNo_recip_lem4)

∀x x' x'i y y', SNo x → 0 < x → x' ∈ SNoR x → SNo x'i → x' * x'i = 1 → SNo y → 1 < x * y → SNo y' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i → 1 < x * y'

In Proofgold the corresponding term root is 417306... and proposition id is b572bc...

Proof:
Proof not loaded.

Definition. We define SNo_recipauxset to be λY x X g ⇒ ⋃_{y ∈ Y}{(1 + (x' + - x) * y) * g x'|x' ∈ X} of type set → set → set → (set → set) → set.

In Proofgold the corresponding term root is f6355f... and object id is d40943...

Theorem. (SNo_recipauxset_I)

∀Y x X, ∀g : set → set, ∀y ∈ Y, ∀x' ∈ X, (1 + (x' + - x) * y) * g x' ∈ SNo_recipauxset Y x X g

In Proofgold the corresponding term root is fb23ea... and proposition id is 3cd34a...

Proof:
Proof not loaded.

Theorem. (SNo_recipauxset_E)

∀Y x X, ∀g : set → set, ∀z ∈ SNo_recipauxset Y x X g, ∀p : prop, (∀y ∈ Y, ∀x' ∈ X, z = (1 + (x' + - x) * y) * g x' → p) → p

In Proofgold the corresponding term root is ea0c30... and proposition id is 9c174a...

Proof:
Proof not loaded.

Theorem. (SNo_recipauxset_ext)

∀Y x X, ∀g h : set → set, (∀x' ∈ X, g x' = h x') → SNo_recipauxset Y x X g = SNo_recipauxset Y x X h

In Proofgold the corresponding term root is 7eb20f... and proposition id is a033a6...

Proof:
Proof not loaded.

Definition. We define SNo_recipaux to be λx g ⇒ nat_primrec ({0},0) (λk p ⇒ (p 0 ∪ SNo_recipauxset (p 0) x (SNoR x) g ∪ SNo_recipauxset (p 1) x (SNoL_pos x) g,p 1 ∪ SNo_recipauxset (p 0) x (SNoL_pos x) g ∪ SNo_recipauxset (p 1) x (SNoR x) g)) of type set → (set → set) → set → set.

In Proofgold the corresponding term root is 8cdbea... and object id is 6fc28a...

Theorem. (SNo_recipaux_0)

∀x, ∀g : set → set, SNo_recipaux x g 0 = ({0},0)

In Proofgold the corresponding term root is 1a1104... and proposition id is a9fc4d...

Proof:
Proof not loaded.

Theorem. (SNo_recipaux_S)

∀x, ∀g : set → set, ∀n, nat_p n → SNo_recipaux x g (ordsucc n) = (SNo_recipaux x g n 0 ∪ SNo_recipauxset (SNo_recipaux x g n 0) x (SNoR x) g ∪ SNo_recipauxset (SNo_recipaux x g n 1) x (SNoL_pos x) g,SNo_recipaux x g n 1 ∪ SNo_recipauxset (SNo_recipaux x g n 0) x (SNoL_pos x) g ∪ SNo_recipauxset (SNo_recipaux x g n 1) x (SNoR x) g)

In Proofgold the corresponding term root is 35af7d... and proposition id is 55b106...

Proof:
Proof not loaded.

Theorem. (SNo_recipaux_lem1)

∀x, SNo x → 0 < x → ∀g : set → set, (∀x' ∈ SNoS_ (SNoLev x), 0 < x' → SNo (g x') ∧ x' * g x' = 1) → ∀k, nat_p k → (∀y ∈ SNo_recipaux x g k 0, SNo y ∧ x * y < 1) ∧ (∀y ∈ SNo_recipaux x g k 1, SNo y ∧ 1 < x * y)

In Proofgold the corresponding term root is af615d... and proposition id is 7c3309...

Proof:
Proof not loaded.

Theorem. (SNo_recipaux_lem2)

∀x, SNo x → 0 < x → ∀g : set → set, (∀x' ∈ SNoS_ (SNoLev x), 0 < x' → SNo (g x') ∧ x' * g x' = 1) → SNoCutP (⋃_{k ∈ ω}SNo_recipaux x g k 0) (⋃_{k ∈ ω}SNo_recipaux x g k 1)

In Proofgold the corresponding term root is 38996c... and proposition id is c6f6db...

Proof:
Proof not loaded.

Theorem. (SNo_recipaux_ext)

∀x, SNo x → ∀g h : set → set, (∀x' ∈ SNoS_ (SNoLev x), g x' = h x') → ∀k, nat_p k → SNo_recipaux x g k = SNo_recipaux x h k

In Proofgold the corresponding term root is b2de41... and proposition id is e7b024...

Proof:
Proof not loaded.

Beginning of Section recip_SNo_pos

Let G : set → (set → set) → set ≝ λx g ⇒ SNoCut (⋃_{k ∈ ω}SNo_recipaux x g k 0) (⋃_{k ∈ ω}SNo_recipaux x g k 1)

Definition. We define recip_SNo_pos to be SNo_rec_i G of type set → set.

In Proofgold the corresponding term root is 88641a... and object id is 2f4ee1...

Theorem. (recip_SNo_pos_eq)

∀x, SNo x → recip_SNo_pos x = G x recip_SNo_pos

In Proofgold the corresponding term root is 2e3e0e... and proposition id is ebab77...

Proof:
Proof not loaded.

Theorem. (recip_SNo_pos_prop1)

∀x, SNo x → 0 < x → SNo (recip_SNo_pos x) ∧ x * recip_SNo_pos x = 1

In Proofgold the corresponding term root is 42138c... and proposition id is 785262...

Proof:
Proof not loaded.

Theorem. (SNo_recip_SNo_pos)

∀x, SNo x → 0 < x → SNo (recip_SNo_pos x)

In Proofgold the corresponding term root is 90e6e6... and proposition id is 6b9294...

Proof:
Proof not loaded.

Theorem. (recip_SNo_pos_invR)

∀x, SNo x → 0 < x → x * recip_SNo_pos x = 1

In Proofgold the corresponding term root is 12c412... and proposition id is a4f83c...

Proof:
Proof not loaded.

Theorem. (recip_SNo_pos_1)

recip_SNo_pos 1 = 1

In Proofgold the corresponding term root is df53e8... and proposition id is bf8279...

Proof:
Proof not loaded.

Theorem. (recip_SNo_pos_is_pos)

∀x, SNo x → 0 < x → 0 < recip_SNo_pos x

In Proofgold the corresponding term root is c95744... and proposition id is 30d6a5...

Proof:
Proof not loaded.

Theorem. (recip_SNo_pos_invol)

∀x, SNo x → 0 < x → recip_SNo_pos (recip_SNo_pos x) = x

In Proofgold the corresponding term root is 5e7409... and proposition id is a3c6c5...

Proof:
Proof not loaded.

Theorem. (recip_SNo_pos_eps_)

∀n, nat_p n → recip_SNo_pos (eps_ n) = 2 ^ n

In Proofgold the corresponding term root is ce7e5d... and proposition id is 3c7219...

Proof:
Proof not loaded.

Theorem. (recip_SNo_pos_pow_2)

∀n, nat_p n → recip_SNo_pos (2 ^ n) = eps_ n

In Proofgold the corresponding term root is e4f02a... and proposition id is 9ca0e9...

Proof:
Proof not loaded.

Theorem. (recip_SNo_pos_2)

recip_SNo_pos 2 = eps_ 1

In Proofgold the corresponding term root is 1953c2... and proposition id is 4addd0...

Proof:
Proof not loaded.

End of Section recip_SNo_pos

Definition. We define recip_SNo to be λx ⇒ if 0 < x then recip_SNo_pos x else if x < 0 then - recip_SNo_pos (- x) else 0 of type set → set.

In Proofgold the corresponding term root is aa96a2... and object id is 0d39b7...

Theorem. (recip_SNo_poscase)

∀x, 0 < x → recip_SNo x = recip_SNo_pos x

In Proofgold the corresponding term root is 152688... and proposition id is 2f43fd...

Proof:
Proof not loaded.

Theorem. (recip_SNo_negcase)

∀x, SNo x → x < 0 → recip_SNo x = - recip_SNo_pos (- x)

In Proofgold the corresponding term root is c96182... and proposition id is 126cc9...

Proof:
Proof not loaded.

Theorem. (recip_SNo_0)

recip_SNo 0 = 0

In Proofgold the corresponding term root is bda1b2... and proposition id is 466dab...

Proof:
Proof not loaded.

Theorem. (recip_SNo_1)

recip_SNo 1 = 1

In Proofgold the corresponding term root is cb7d70... and proposition id is 75c888...

Proof:
Proof not loaded.

Theorem. (SNo_recip_SNo)

∀x, SNo x → SNo (recip_SNo x)

In Proofgold the corresponding term root is 675572... and proposition id is 9f0369...

Proof:
Proof not loaded.

Theorem. (recip_SNo_invR)

∀x, SNo x → x ≠ 0 → x * recip_SNo x = 1

In Proofgold the corresponding term root is 33c26e... and proposition id is 446f16...

Proof:
Proof not loaded.

Theorem. (recip_SNo_invL)

∀x, SNo x → x ≠ 0 → recip_SNo x * x = 1

In Proofgold the corresponding term root is 85d435... and proposition id is e80fdb...

Proof:
Proof not loaded.

Theorem. (recip_SNo_eps_)

∀n, nat_p n → recip_SNo (eps_ n) = 2 ^ n

In Proofgold the corresponding term root is bbfaeb... and proposition id is 811e50...

Proof:
Proof not loaded.

Theorem. (recip_SNo_pow_2)

∀n, nat_p n → recip_SNo (2 ^ n) = eps_ n

In Proofgold the corresponding term root is 761b63... and proposition id is 80f328...

Proof:
Proof not loaded.

Theorem. (recip_SNo_2)

recip_SNo 2 = eps_ 1

In Proofgold the corresponding term root is 1a7547... and proposition id is c21d28...

Proof:
Proof not loaded.

Theorem. (recip_SNo_invol)

∀x, SNo x → recip_SNo (recip_SNo x) = x

In Proofgold the corresponding term root is d2c4c3... and proposition id is f0af46...

Proof:
Proof not loaded.

Theorem. (recip_SNo_of_pos_is_pos)

∀x, SNo x → 0 < x → 0 < recip_SNo x

In Proofgold the corresponding term root is 8f5692... and proposition id is 1015d4...

Proof:
Proof not loaded.

Theorem. (recip_SNo_neg')

∀x, SNo x → x < 0 → recip_SNo x < 0

In Proofgold the corresponding term root is eceae8... and proposition id is 49b9ec...

Proof:
Proof not loaded.

Definition. We define div_SNo to be λx y ⇒ x * recip_SNo y of type set → set → set.

In Proofgold the corresponding term root is a77cc8... and object id is 8b12fd...

Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.

Theorem. (SNo_div_SNo)

∀x y, SNo x → SNo y → SNo (x :/: y)

In Proofgold the corresponding term root is cebe75... and proposition id is c761b5...

Proof:
Proof not loaded.

Theorem. (div_SNo_0_num)

∀x, SNo x → 0 :/: x = 0

In Proofgold the corresponding term root is 28c3dc... and proposition id is ec5f74...

Proof:
Proof not loaded.

Theorem. (div_SNo_0_denum)

∀x, SNo x → x :/: 0 = 0

In Proofgold the corresponding term root is d6eb4e... and proposition id is 46b3d2...

Proof:
Proof not loaded.

Theorem. (mul_div_SNo_invL)

∀x y, SNo x → SNo y → y ≠ 0 → (x :/: y) * y = x

In Proofgold the corresponding term root is 2484b5... and proposition id is 07d80b...

Proof:
Proof not loaded.

Theorem. (mul_div_SNo_invR)

∀x y, SNo x → SNo y → y ≠ 0 → y * (x :/: y) = x

In Proofgold the corresponding term root is 9b260e... and proposition id is df334a...

Proof:
Proof not loaded.

Theorem. (mul_div_SNo_R)

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

In Proofgold the corresponding term root is a78538... and proposition id is daa8eb...

Proof:
Proof not loaded.

Theorem. (mul_div_SNo_L)

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

In Proofgold the corresponding term root is 95a4c6... and proposition id is c10e5c...

Proof:
Proof not loaded.

Theorem. (div_mul_SNo_invL)

∀x y, SNo x → SNo y → y ≠ 0 → (x * y) :/: y = x

In Proofgold the corresponding term root is c74971... and proposition id is b99cd5...

Proof:
Proof not loaded.

Theorem. (div_div_SNo)

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

In Proofgold the corresponding term root is 3e9827... and proposition id is de0369...

Proof:
Proof not loaded.

Theorem. (mul_div_SNo_both)

∀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 06b28b... and proposition id is e61f18...

Proof:
Proof not loaded.

Theorem. (recip_SNo_pos_pos)

∀x, SNo x → 0 < x → 0 < recip_SNo_pos x

In Proofgold the corresponding term root is c95744... and proposition id is 30d6a5...

Proof:
Proof not loaded.

Theorem. (recip_SNo_of_neg_is_neg)

∀x, SNo x → x < 0 → recip_SNo x < 0

In Proofgold the corresponding term root is eceae8... and proposition id is 49b9ec...

Proof:
Proof not loaded.

Theorem. (div_SNo_pos_pos)

∀x y, SNo x → SNo y → 0 < x → 0 < y → 0 < x :/: y

In Proofgold the corresponding term root is acf73b... and proposition id is 9935dd...

Proof:
Proof not loaded.

Theorem. (div_SNo_neg_neg)

∀x y, SNo x → SNo y → x < 0 → y < 0 → 0 < x :/: y

In Proofgold the corresponding term root is 92b216... and proposition id is 7268ee...

Proof:
Proof not loaded.

Theorem. (div_SNo_pos_neg)

∀x y, SNo x → SNo y → 0 < x → y < 0 → x :/: y < 0

In Proofgold the corresponding term root is 8b3bd2... and proposition id is d188d5...

Proof:
Proof not loaded.

Theorem. (div_SNo_neg_pos)

∀x y, SNo x → SNo y → x < 0 → 0 < y → x :/: y < 0

In Proofgold the corresponding term root is ff8d4c... and proposition id is df8e4a...

Proof:
Proof not loaded.

Theorem. (div_SNo_pos_LtL)

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

In Proofgold the corresponding term root is 6ffbf3... and proposition id is 87c1ac...

Proof:
Proof not loaded.

Theorem. (div_SNo_pos_LtR)

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

In Proofgold the corresponding term root is caaa93... and proposition id is c36da0...

Proof:
Proof not loaded.

Theorem. (div_SNo_pos_LtL')

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

In Proofgold the corresponding term root is 6d81ed... and proposition id is de6389...

Proof:
Proof not loaded.

Theorem. (div_SNo_pos_LtR')

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

In Proofgold the corresponding term root is 0c5a47... and proposition id is a7e3d6...

Proof:
Proof not loaded.

Theorem. (mul_div_SNo_nonzero_eq)

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

In Proofgold the corresponding term root is 4c4da2... and proposition id is bea168...

Proof:
Proof not loaded.

End of Section SurrealDiv