Metamath Proof Explorer

Theorem nnmord

Description: Ordering property of multiplication. Proposition 8.19 of TakeutiZaring p. 63, limited to natural numbers. (Contributed by NM, 22-Jan-1996) (Revised by Mario Carneiro, 15-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 nnmordi 
 |-  ( ( ( B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( A e. B -> ( C .o A ) e. ( C .o B ) ) )
2 1 ex 
 |-  ( ( B e. _om /\ C e. _om ) -> ( (/) e. C -> ( A e. B -> ( C .o A ) e. ( C .o B ) ) ) )
3 2 impcomd 
 |-  ( ( B e. _om /\ C e. _om ) -> ( ( A e. B /\ (/) e. C ) -> ( C .o A ) e. ( C .o B ) ) )
4 3 3adant1 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( A e. B /\ (/) e. C ) -> ( C .o A ) e. ( C .o B ) ) )
5 ne0i 
 |-  ( ( C .o A ) e. ( C .o B ) -> ( C .o B ) =/= (/) )
6 nnm0r 
 |-  ( B e. _om -> ( (/) .o B ) = (/) )
7 oveq1 
 |-  ( C = (/) -> ( C .o B ) = ( (/) .o B ) )
8 7 eqeq1d 
 |-  ( C = (/) -> ( ( C .o B ) = (/) <-> ( (/) .o B ) = (/) ) )
9 6 8 syl5ibrcom 
 |-  ( B e. _om -> ( C = (/) -> ( C .o B ) = (/) ) )
10 9 necon3d 
 |-  ( B e. _om -> ( ( C .o B ) =/= (/) -> C =/= (/) ) )
11 5 10 syl5 
 |-  ( B e. _om -> ( ( C .o A ) e. ( C .o B ) -> C =/= (/) ) )
12 11 adantr 
 |-  ( ( B e. _om /\ C e. _om ) -> ( ( C .o A ) e. ( C .o B ) -> C =/= (/) ) )
13 nnord 
 |-  ( C e. _om -> Ord C )
14 ord0eln0 
 |-  ( Ord C -> ( (/) e. C <-> C =/= (/) ) )
15 13 14 syl 
 |-  ( C e. _om -> ( (/) e. C <-> C =/= (/) ) )
16 15 adantl 
 |-  ( ( B e. _om /\ C e. _om ) -> ( (/) e. C <-> C =/= (/) ) )
17 12 16 sylibrd 
 |-  ( ( B e. _om /\ C e. _om ) -> ( ( C .o A ) e. ( C .o B ) -> (/) e. C ) )
18 17 3adant1 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( C .o A ) e. ( C .o B ) -> (/) e. C ) )
19 oveq2 
 |-  ( A = B -> ( C .o A ) = ( C .o B ) )
20 19 a1i 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( A = B -> ( C .o A ) = ( C .o B ) ) )
21 nnmordi 
 |-  ( ( ( A e. _om /\ C e. _om ) /\ (/) e. C ) -> ( B e. A -> ( C .o B ) e. ( C .o A ) ) )
22 21 3adantl2 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( B e. A -> ( C .o B ) e. ( C .o A ) ) )
23 20 22 orim12d 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( ( A = B \/ B e. A ) -> ( ( C .o A ) = ( C .o B ) \/ ( C .o B ) e. ( C .o A ) ) ) )
24 23 con3d 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( -. ( ( C .o A ) = ( C .o B ) \/ ( C .o B ) e. ( C .o A ) ) -> -. ( A = B \/ B e. A ) ) )
25 simpl3 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> C e. _om )
26 simpl1 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> A e. _om )
27 nnmcl 
 |-  ( ( C e. _om /\ A e. _om ) -> ( C .o A ) e. _om )
28 25 26 27 syl2anc 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( C .o A ) e. _om )
29 simpl2 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> B e. _om )
30 nnmcl 
 |-  ( ( C e. _om /\ B e. _om ) -> ( C .o B ) e. _om )
31 25 29 30 syl2anc 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( C .o B ) e. _om )
32 nnord 
 |-  ( ( C .o A ) e. _om -> Ord ( C .o A ) )
33 nnord 
 |-  ( ( C .o B ) e. _om -> Ord ( C .o B ) )
34 ordtri2 
 |-  ( ( Ord ( C .o A ) /\ Ord ( C .o B ) ) -> ( ( C .o A ) e. ( C .o B ) <-> -. ( ( C .o A ) = ( C .o B ) \/ ( C .o B ) e. ( C .o A ) ) ) )
35 32 33 34 syl2an 
 |-  ( ( ( C .o A ) e. _om /\ ( C .o B ) e. _om ) -> ( ( C .o A ) e. ( C .o B ) <-> -. ( ( C .o A ) = ( C .o B ) \/ ( C .o B ) e. ( C .o A ) ) ) )
36 28 31 35 syl2anc 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( ( C .o A ) e. ( C .o B ) <-> -. ( ( C .o A ) = ( C .o B ) \/ ( C .o B ) e. ( C .o A ) ) ) )
37 nnord 
 |-  ( A e. _om -> Ord A )
38 nnord 
 |-  ( B e. _om -> Ord B )
39 ordtri2 
 |-  ( ( Ord A /\ Ord B ) -> ( A e. B <-> -. ( A = B \/ B e. A ) ) )
40 37 38 39 syl2an 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A e. B <-> -. ( A = B \/ B e. A ) ) )
41 26 29 40 syl2anc 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( A e. B <-> -. ( A = B \/ B e. A ) ) )
42 24 36 41 3imtr4d 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( ( C .o A ) e. ( C .o B ) -> A e. B ) )
43 42 ex 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( (/) e. C -> ( ( C .o A ) e. ( C .o B ) -> A e. B ) ) )
44 43 com23 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( C .o A ) e. ( C .o B ) -> ( (/) e. C -> A e. B ) ) )
45 18 44 mpdd 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( C .o A ) e. ( C .o B ) -> A e. B ) )
46 45 18 jcad 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( C .o A ) e. ( C .o B ) -> ( A e. B /\ (/) e. C ) ) )
47 4 46 impbid 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( A e. B /\ (/) e. C ) <-> ( C .o A ) e. ( C .o B ) ) )