Metamath Proof Explorer


Theorem divscan2wd

Description: A weak cancellation law for surreal division. (Contributed by Scott Fenton, 13-Mar-2025)

Ref Expression
Hypotheses divscan2wd.1 φANo
divscan2wd.2 φBNo
divscan2wd.3 φB0s
divscan2wd.4 φxNoBsx=1s
Assertion divscan2wd φBsA/suB=A

Proof

Step Hyp Ref Expression
1 divscan2wd.1 φANo
2 divscan2wd.2 φBNo
3 divscan2wd.3 φB0s
4 divscan2wd.4 φxNoBsx=1s
5 eqid A/suB=A/suB
6 1 2 3 4 divsclwd φA/suBNo
7 1 6 2 3 4 divsmulwd φA/suB=A/suBBsA/suB=A
8 5 7 mpbii φBsA/suB=A