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.
L16Definition. We define
SNoL_pos to be
λx ⇒ {w ∈ SNoL x|0 < w} of type
set → set.
L17Axiom. (
SNo_recip_pos_pos) We take the following as an axiom:
∀x xi, SNo x → SNo xi → 0 < x → x * xi = 1 → 0 < xi
L18Axiom. (
SNo_recip_lem1) We take the following as an axiom:
∀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'
L19Axiom. (
SNo_recip_lem2) We take the following as an axiom:
∀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
L20Axiom. (
SNo_recip_lem3) We take the following as an axiom:
∀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
L21Axiom. (
SNo_recip_lem4) We take the following as an axiom:
∀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'
L22Definition. 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.
L29Axiom. (
SNo_recipaux_lem1) We take the following as an axiom:
∀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)
L30Axiom. (
SNo_recipaux_lem2) We take the following as an axiom:
∀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)
Beginning of Section recip_SNo_pos
End of Section recip_SNo_pos
Primitive. The name
recip_SNo is a term of type
set → set.
L51Axiom. (
recip_SNo_0) We take the following as an axiom:
L52Axiom. (
recip_SNo_1) We take the following as an axiom:
L58Axiom. (
recip_SNo_2) We take the following as an axiom:
Notation. We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
div_SNo.
L65Axiom. (
SNo_div_SNo) We take the following as an axiom:
∀x y, SNo x → SNo y → SNo (x :/: y)
L68Axiom. (
mul_div_SNo_invL) We take the following as an axiom:
∀x y, SNo x → SNo y → y ≠ 0 → (x :/: y) * y = x
L69Axiom. (
mul_div_SNo_invR) We take the following as an axiom:
∀x y, SNo x → SNo y → y ≠ 0 → y * (x :/: y) = x
L70Axiom. (
mul_div_SNo_R) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → (x :/: y) * z = (x * z) :/: y
L71Axiom. (
mul_div_SNo_L) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → z * (x :/: y) = (z * x) :/: y
L72Axiom. (
div_mul_SNo_invL) We take the following as an axiom:
∀x y, SNo x → SNo y → y ≠ 0 → (x * y) :/: y = x
L73Axiom. (
div_div_SNo) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → (x :/: y) :/: z = x :/: (y * z)
L74Axiom. (
mul_div_SNo_both) 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)
L77Axiom. (
div_SNo_pos_pos) We take the following as an axiom:
∀x y, SNo x → SNo y → 0 < x → 0 < y → 0 < x :/: y
L78Axiom. (
div_SNo_neg_neg) We take the following as an axiom:
∀x y, SNo x → SNo y → x < 0 → y < 0 → 0 < x :/: y
L79Axiom. (
div_SNo_pos_neg) We take the following as an axiom:
∀x y, SNo x → SNo y → 0 < x → y < 0 → x :/: y < 0
L80Axiom. (
div_SNo_neg_pos) We take the following as an axiom:
∀x y, SNo x → SNo y → x < 0 → 0 < y → x :/: y < 0
L81Axiom. (
div_SNo_pos_LtL) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → 0 < y → x < z * y → x :/: y < z
L82Axiom. (
div_SNo_pos_LtR) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → 0 < y → z * y < x → z < x :/: y
L83Axiom. (
div_SNo_pos_LtL') We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → 0 < y → x :/: y < z → x < z * y
L84Axiom. (
div_SNo_pos_LtR') We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → 0 < y → z < x :/: y → z * y < x
L85Axiom. (
mul_div_SNo_nonzero_eq) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → y ≠ 0 → x = y * z → x :/: y = z
End of Section SurrealDiv