This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnmwordri

Description: Weak ordering property of ordinal multiplication. Proposition 8.21 of TakeutiZaring p. 63, limited to natural numbers. (Contributed by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion nnmwordri 
|- ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A C_ B -> ( A .o C ) C_ ( B .o C ) ) )

Proof

Step Hyp Ref Expression
1 nnmwordi 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A C_ B -> ( C .o A ) C_ ( C .o B ) ) )
2 nnmcom 
 |-  ( ( A e. _om /\ C e. _om ) -> ( A .o C ) = ( C .o A ) )
3 2 3adant2 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A .o C ) = ( C .o A ) )
4 nnmcom 
 |-  ( ( B e. _om /\ C e. _om ) -> ( B .o C ) = ( C .o B ) )
5 4 3adant1 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( B .o C ) = ( C .o B ) )
6 3 5 sseq12d 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( A .o C ) C_ ( B .o C ) <-> ( C .o A ) C_ ( C .o B ) ) )
7 1 6 sylibrd 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A C_ B -> ( A .o C ) C_ ( B .o C ) ) )