Database
SURREAL NUMBERS
Surreal arithmetic
Division
divscl
Next ⟩
divscld
Metamath Proof Explorer
Ascii
Unicode
Theorem
divscl
Description:
Surreal division closure law.
(Contributed by
Scott Fenton
, 16-Mar-2025)
Ref
Expression
Assertion
divscl
⊢
A
∈
No
∧
B
∈
No
∧
B
≠
0
s
→
A
/
su
B
∈
No
Proof
Step
Hyp
Ref
Expression
1
recsex
⊢
B
∈
No
∧
B
≠
0
s
→
∃
x
∈
No
B
⋅
s
x
=
1
s
2
1
3adant1
⊢
A
∈
No
∧
B
∈
No
∧
B
≠
0
s
→
∃
x
∈
No
B
⋅
s
x
=
1
s
3
divsclw
⊢
A
∈
No
∧
B
∈
No
∧
B
≠
0
s
∧
∃
x
∈
No
B
⋅
s
x
=
1
s
→
A
/
su
B
∈
No
4
2
3
mpdan
⊢
A
∈
No
∧
B
∈
No
∧
B
≠
0
s
→
A
/
su
B
∈
No