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 𝑵 A < 𝑵 B C 𝑵 A < 𝑵 C 𝑵 B

Proof

Step Hyp Ref Expression
1 dmmulpi dom 𝑵 = 𝑵 × 𝑵
2 ltrelpi < 𝑵 𝑵 × 𝑵
3 0npi ¬ 𝑵
4 pinn A 𝑵 A ω
5 pinn B 𝑵 B ω
6 elni2 C 𝑵 C ω C
7 iba C A B A B C
8 nnmord A ω B ω C ω A B C C 𝑜 A C 𝑜 B
9 7 8 sylan9bbr A ω B ω C ω C A B C 𝑜 A C 𝑜 B
10 9 3exp1 A ω B ω C ω C A B C 𝑜 A C 𝑜 B
11 10 imp4b A ω B ω C ω C A B C 𝑜 A C 𝑜 B
12 6 11 syl5bi A ω B ω C 𝑵 A B C 𝑜 A C 𝑜 B
13 4 5 12 syl2an A 𝑵 B 𝑵 C 𝑵 A B C 𝑜 A C 𝑜 B
14 13 imp A 𝑵 B 𝑵 C 𝑵 A B C 𝑜 A C 𝑜 B
15 ltpiord A 𝑵 B 𝑵 A < 𝑵 B A B
16 15 adantr A 𝑵 B 𝑵 C 𝑵 A < 𝑵 B A B
17 mulclpi C 𝑵 A 𝑵 C 𝑵 A 𝑵
18 mulclpi C 𝑵 B 𝑵 C 𝑵 B 𝑵
19 ltpiord C 𝑵 A 𝑵 C 𝑵 B 𝑵 C 𝑵 A < 𝑵 C 𝑵 B C 𝑵 A C 𝑵 B
20 17 18 19 syl2an C 𝑵 A 𝑵 C 𝑵 B 𝑵 C 𝑵 A < 𝑵 C 𝑵 B C 𝑵 A C 𝑵 B
21 mulpiord C 𝑵 A 𝑵 C 𝑵 A = C 𝑜 A
22 21 adantr C 𝑵 A 𝑵 C 𝑵 B 𝑵 C 𝑵 A = C 𝑜 A
23 mulpiord C 𝑵 B 𝑵 C 𝑵 B = C 𝑜 B
24 23 adantl C 𝑵 A 𝑵 C 𝑵 B 𝑵 C 𝑵 B = C 𝑜 B
25 22 24 eleq12d C 𝑵 A 𝑵 C 𝑵 B 𝑵 C 𝑵 A C 𝑵 B C 𝑜 A C 𝑜 B
26 20 25 bitrd C 𝑵 A 𝑵 C 𝑵 B 𝑵 C 𝑵 A < 𝑵 C 𝑵 B C 𝑜 A C 𝑜 B
27 26 anandis C 𝑵 A 𝑵 B 𝑵 C 𝑵 A < 𝑵 C 𝑵 B C 𝑜 A C 𝑜 B
28 27 ancoms A 𝑵 B 𝑵 C 𝑵 C 𝑵 A < 𝑵 C 𝑵 B C 𝑜 A C 𝑜 B
29 14 16 28 3bitr4d A 𝑵 B 𝑵 C 𝑵 A < 𝑵 B C 𝑵 A < 𝑵 C 𝑵 B
30 29 3impa A 𝑵 B 𝑵 C 𝑵 A < 𝑵 B C 𝑵 A < 𝑵 C 𝑵 B
31 1 2 3 30 ndmovord C 𝑵 A < 𝑵 B C 𝑵 A < 𝑵 C 𝑵 B