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 ) ) )