Metamath Proof Explorer

Theorem nnmwordi

Description: Weak ordering property of multiplication. (Contributed by Mario Carneiro, 17-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 nnmword 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( A C_ B <-> ( C .o A ) C_ ( C .o B ) ) )
2 1 biimpd 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( A C_ B -> ( C .o A ) C_ ( C .o B ) ) )
3 2 ex 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( (/) e. C -> ( A C_ B -> ( C .o A ) C_ ( C .o B ) ) ) )
4 nnord 
 |-  ( C e. _om -> Ord C )
5 ord0eln0 
 |-  ( Ord C -> ( (/) e. C <-> C =/= (/) ) )
6 5 necon2bbid 
 |-  ( Ord C -> ( C = (/) <-> -. (/) e. C ) )
7 4 6 syl 
 |-  ( C e. _om -> ( C = (/) <-> -. (/) e. C ) )
8 7 3ad2ant3 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( C = (/) <-> -. (/) e. C ) )
9 ssid 
 |-  (/) C_ (/)
10 nnm0r 
 |-  ( A e. _om -> ( (/) .o A ) = (/) )
11 10 adantr 
 |-  ( ( A e. _om /\ B e. _om ) -> ( (/) .o A ) = (/) )
12 nnm0r 
 |-  ( B e. _om -> ( (/) .o B ) = (/) )
13 12 adantl 
 |-  ( ( A e. _om /\ B e. _om ) -> ( (/) .o B ) = (/) )
14 11 13 sseq12d 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( (/) .o A ) C_ ( (/) .o B ) <-> (/) C_ (/) ) )
15 9 14 mpbiri 
 |-  ( ( A e. _om /\ B e. _om ) -> ( (/) .o A ) C_ ( (/) .o B ) )
16 oveq1 
 |-  ( C = (/) -> ( C .o A ) = ( (/) .o A ) )
17 oveq1 
 |-  ( C = (/) -> ( C .o B ) = ( (/) .o B ) )
18 16 17 sseq12d 
 |-  ( C = (/) -> ( ( C .o A ) C_ ( C .o B ) <-> ( (/) .o A ) C_ ( (/) .o B ) ) )
19 15 18 syl5ibrcom 
 |-  ( ( A e. _om /\ B e. _om ) -> ( C = (/) -> ( C .o A ) C_ ( C .o B ) ) )
20 19 3adant3 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( C = (/) -> ( C .o A ) C_ ( C .o B ) ) )
21 8 20 sylbird 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( -. (/) e. C -> ( C .o A ) C_ ( C .o B ) ) )
22 21 a1dd 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( -. (/) e. C -> ( A C_ B -> ( C .o A ) C_ ( C .o B ) ) ) )
23 3 22 pm2.61d 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A C_ B -> ( C .o A ) C_ ( C .o B ) ) )