Database
SURREAL NUMBERS
Surreal arithmetic
Division
df-divs
Metamath Proof Explorer
Description: Define surreal division. This is not the definition used in the
literature, but we use it here because it is technically easier to work
with. (Contributed by Scott Fenton , 12-Mar-2025)
Ref
Expression
Assertion
df-divs
⊢ / su = x ∈ No , y ∈ No ∖ 0 s ⟼ ι z ∈ No | y ⋅ s z = x
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cdivs
class / su
1
vx
setvar x
2
csur
class No
3
vy
setvar y
4
c0s
class 0 s
5
4
csn
class 0 s
6
2 5
cdif
class No ∖ 0 s
7
vz
setvar z
8
3
cv
setvar y
9
cmuls
class ⋅ s
10
7
cv
setvar z
11
8 10 9
co
class y ⋅ s z
12
1
cv
setvar x
13
11 12
wceq
wff y ⋅ s z = x
14
13 7 2
crio
class ι z ∈ No | y ⋅ s z = x
15
1 3 2 6 14
cmpo
class x ∈ No , y ∈ No ∖ 0 s ⟼ ι z ∈ No | y ⋅ s z = x
16
0 15
wceq
wff / su = x ∈ No , y ∈ No ∖ 0 s ⟼ ι z ∈ No | y ⋅ s z = x