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