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	biimtrid	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐶 ∈ 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 𝐵 ) ) )