Metamath Proof Explorer


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