Metamath Proof Explorer


Theorem muls02

Description: Surreal multiplication by zero. (Contributed by Scott Fenton, 4-Feb-2025)

Ref Expression
Assertion muls02 A No 0 s s A = 0 s

Proof

Step Hyp Ref Expression
1 0sno 0 s No
2 mulscom 0 s No A No 0 s s A = A s 0 s
3 1 2 mpan A No 0 s s A = A s 0 s
4 muls01 A No A s 0 s = 0 s
5 3 4 eqtrd A No 0 s s A = 0 s