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 ( 𝐶 ∈ N → ( 𝐴 <N 𝐵 ↔ ( 𝐶 ·N 𝐴 ) <N ( 𝐶 ·N 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 dmmulpi ⊢ dom ·N = ( N × N )
2 ltrelpi ⊢ <N ⊆ ( N × N )
3 0npi ⊢ ¬ ∅ ∈ N
4 pinn ⊢ ( 𝐴 ∈ N → 𝐴 ∈ ω )
5 pinn ⊢ ( 𝐵 ∈ N → 𝐵 ∈ ω )
6 elni2 ⊢ ( 𝐶 ∈ N ↔ ( 𝐶 ∈ ω ∧ ∅ ∈ 𝐶 ) )
7 iba ⊢ ( ∅ ∈ 𝐶 → ( 𝐴 ∈ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐶 ) ) )
8 nnmord ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐶 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )
9 7 8 sylan9bbr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )
10 9 3exp1 ⊢ ( 𝐴 ∈ ω → ( 𝐵 ∈ ω → ( 𝐶 ∈ ω → ( ∅ ∈ 𝐶 → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) ) ) )
11 10 imp4b ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐶 ∈ ω ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) )
12 6 11 syl5bi ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐶 ∈ N → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) )
13 4 5 12 syl2an ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐶 ∈ N → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) )
14 13 imp ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )
15 ltpiord ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 <N 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
16 15 adantr ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( 𝐴 <N 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
17 mulclpi ⊢ ( ( 𝐶 ∈ N ∧ 𝐴 ∈ N ) → ( 𝐶 ·N 𝐴 ) ∈ N )
18 mulclpi ⊢ ( ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐶 ·N 𝐵 ) ∈ N )
19 ltpiord ⊢ ( ( ( 𝐶 ·N 𝐴 ) ∈ N ∧ ( 𝐶 ·N 𝐵 ) ∈ N ) → ( ( 𝐶 ·N 𝐴 ) <N ( 𝐶 ·N 𝐵 ) ↔ ( 𝐶 ·N 𝐴 ) ∈ ( 𝐶 ·N 𝐵 ) ) )
20 17 18 19 syl2an ⊢ ( ( ( 𝐶 ∈ N ∧ 𝐴 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) ) → ( ( 𝐶 ·N 𝐴 ) <N ( 𝐶 ·N 𝐵 ) ↔ ( 𝐶 ·N 𝐴 ) ∈ ( 𝐶 ·N 𝐵 ) ) )
21 mulpiord ⊢ ( ( 𝐶 ∈ N ∧ 𝐴 ∈ N ) → ( 𝐶 ·N 𝐴 ) = ( 𝐶 ·o 𝐴 ) )
22 21 adantr ⊢ ( ( ( 𝐶 ∈ N ∧ 𝐴 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) ) → ( 𝐶 ·N 𝐴 ) = ( 𝐶 ·o 𝐴 ) )
23 mulpiord ⊢ ( ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐶 ·N 𝐵 ) = ( 𝐶 ·o 𝐵 ) )
24 23 adantl ⊢ ( ( ( 𝐶 ∈ N ∧ 𝐴 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) ) → ( 𝐶 ·N 𝐵 ) = ( 𝐶 ·o 𝐵 ) )
25 22 24 eleq12d ⊢ ( ( ( 𝐶 ∈ N ∧ 𝐴 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) ) → ( ( 𝐶 ·N 𝐴 ) ∈ ( 𝐶 ·N 𝐵 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )
26 20 25 bitrd ⊢ ( ( ( 𝐶 ∈ N ∧ 𝐴 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) ) → ( ( 𝐶 ·N 𝐴 ) <N ( 𝐶 ·N 𝐵 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )
27 26 anandis ⊢ ( ( 𝐶 ∈ N ∧ ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ) → ( ( 𝐶 ·N 𝐴 ) <N ( 𝐶 ·N 𝐵 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )
28 27 ancoms ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( ( 𝐶 ·N 𝐴 ) <N ( 𝐶 ·N 𝐵 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )
29 14 16 28 3bitr4d ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( 𝐴 <N 𝐵 ↔ ( 𝐶 ·N 𝐴 ) <N ( 𝐶 ·N 𝐵 ) ) )
30 29 3impa ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐴 <N 𝐵 ↔ ( 𝐶 ·N 𝐴 ) <N ( 𝐶 ·N 𝐵 ) ) )
31 1 2 3 30 ndmovord ⊢ ( 𝐶 ∈ N → ( 𝐴 <N 𝐵 ↔ ( 𝐶 ·N 𝐴 ) <N ( 𝐶 ·N 𝐵 ) ) )