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

Metamath Proof Explorer

Theorem ltmpi

Description: Ordering property of multiplication for positive integers. (Contributed by NM, 8-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion ltmpi 
|- ( C e. N. -> ( A  ( C .N A )

Proof

Step Hyp Ref Expression
1 dmmulpi 
 |-  dom .N = ( N. X. N. )
2 ltrelpi 
 |-
3 0npi 
 |-  -. (/) e. N.
4 pinn 
 |-  ( A e. N. -> A e. _om )
5 pinn 
 |-  ( B e. N. -> B e. _om )
6 elni2 
 |-  ( C e. N. <-> ( C e. _om /\ (/) e. C ) )
7 iba 
 |-  ( (/) e. C -> ( A e. B <-> ( A e. B /\ (/) e. C ) ) )
8 nnmord 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( A e. B /\ (/) e. C ) <-> ( C .o A ) e. ( C .o B ) ) )
9 7 8 sylan9bbr 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. C ) -> ( A e. B <-> ( C .o A ) e. ( C .o B ) ) )
10 9 3exp1 
 |-  ( A e. _om -> ( B e. _om -> ( C e. _om -> ( (/) e. C -> ( A e. B <-> ( C .o A ) e. ( C .o B ) ) ) ) ) )
11 10 imp4b 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( C e. _om /\ (/) e. C ) -> ( A e. B <-> ( C .o A ) e. ( C .o B ) ) ) )
12 6 11 biimtrid 
 |-  ( ( A e. _om /\ B e. _om ) -> ( C e. N. -> ( A e. B <-> ( C .o A ) e. ( C .o B ) ) ) )
13 4 5 12 syl2an 
 |-  ( ( A e. N. /\ B e. N. ) -> ( C e. N. -> ( A e. B <-> ( C .o A ) e. ( C .o B ) ) ) )
14 13 imp 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( A e. B <-> ( C .o A ) e. ( C .o B ) ) )
15 ltpiord 
 |-  ( ( A e. N. /\ B e. N. ) -> ( A  A e. B ) )
16 15 adantr 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( A  A e. B ) )
17 mulclpi 
 |-  ( ( C e. N. /\ A e. N. ) -> ( C .N A ) e. N. )
18 mulclpi 
 |-  ( ( C e. N. /\ B e. N. ) -> ( C .N B ) e. N. )
19 ltpiord 
 |-  ( ( ( C .N A ) e. N. /\ ( C .N B ) e. N. ) -> ( ( C .N A )  ( C .N A ) e. ( C .N B ) ) )
20 17 18 19 syl2an 
 |-  ( ( ( C e. N. /\ A e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> ( ( C .N A )  ( C .N A ) e. ( C .N B ) ) )
21 mulpiord 
 |-  ( ( C e. N. /\ A e. N. ) -> ( C .N A ) = ( C .o A ) )
22 21 adantr 
 |-  ( ( ( C e. N. /\ A e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> ( C .N A ) = ( C .o A ) )
23 mulpiord 
 |-  ( ( C e. N. /\ B e. N. ) -> ( C .N B ) = ( C .o B ) )
24 23 adantl 
 |-  ( ( ( C e. N. /\ A e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> ( C .N B ) = ( C .o B ) )
25 22 24 eleq12d 
 |-  ( ( ( C e. N. /\ A e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> ( ( C .N A ) e. ( C .N B ) <-> ( C .o A ) e. ( C .o B ) ) )
26 20 25 bitrd 
 |-  ( ( ( C e. N. /\ A e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> ( ( C .N A )  ( C .o A ) e. ( C .o B ) ) )
27 26 anandis 
 |-  ( ( C e. N. /\ ( A e. N. /\ B e. N. ) ) -> ( ( C .N A )  ( C .o A ) e. ( C .o B ) ) )
28 27 ancoms 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( ( C .N A )  ( C .o A ) e. ( C .o B ) ) )
29 14 16 28 3bitr4d 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( A  ( C .N A )
30 29 3impa 
 |-  ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( A  ( C .N A )
31 1 2 3 30 ndmovord 
 |-  ( C e. N. -> ( A  ( C .N A )