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