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 biimtrid ⊢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