Metamath Proof Explorer

Theorem muls02

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

Ref Expression
Assertion muls02 
|- ( A e. No -> ( 0s x.s A ) = 0s )

Proof

Step Hyp Ref Expression
1 0sno 
 |-  0s e. No
2 mulscom 
 |-  ( ( 0s e. No /\ A e. No ) -> ( 0s x.s A ) = ( A x.s 0s ) )
3 1 2 mpan 
 |-  ( A e. No -> ( 0s x.s A ) = ( A x.s 0s ) )
4 muls01 
 |-  ( A e. No -> ( A x.s 0s ) = 0s )
5 3 4 eqtrd 
 |-  ( A e. No -> ( 0s x.s A ) = 0s )