ltmnq

Description: Ordering property of multiplication for positive fractions. Proposition 9-2.6(iii) of Gleason p. 120. (Contributed by NM, 6-Mar-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	ltmnq	⊢ ( 𝐶 ∈ Q → ( 𝐴 <_Q 𝐵 ↔ ( 𝐶 ·_Q 𝐴 ) <_Q ( 𝐶 ·_Q 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulnqf	⊢ ·_Q : ( Q × Q ) ⟶ Q
2	1	fdmi	⊢ dom ·_Q = ( Q × Q )
3		ltrelnq	⊢ <_Q ⊆ ( Q × Q )
4		0nnq	⊢ ¬ ∅ ∈ Q
5		elpqn	⊢ ( 𝐶 ∈ Q → 𝐶 ∈ ( N × N ) )
6	5	3ad2ant3	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → 𝐶 ∈ ( N × N ) )
7		xp1st	⊢ ( 𝐶 ∈ ( N × N ) → ( 1^st ‘ 𝐶 ) ∈ N )
8	6 7	syl	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 1^st ‘ 𝐶 ) ∈ N )
9		xp2nd	⊢ ( 𝐶 ∈ ( N × N ) → ( 2^nd ‘ 𝐶 ) ∈ N )
10	6 9	syl	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 2^nd ‘ 𝐶 ) ∈ N )
11		mulclpi	⊢ ( ( ( 1^st ‘ 𝐶 ) ∈ N ∧ ( 2^nd ‘ 𝐶 ) ∈ N ) → ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ∈ N )
12	8 10 11	syl2anc	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ∈ N )
13		ltmpi	⊢ ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ∈ N → ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) <_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ↔ ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) <_N ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) ) )
14	12 13	syl	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) <_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ↔ ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) <_N ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) ) )
15		fvex	⊢ ( 1^st ‘ 𝐶 ) ∈ V
16		fvex	⊢ ( 2^nd ‘ 𝐶 ) ∈ V
17		fvex	⊢ ( 1^st ‘ 𝐴 ) ∈ V
18		mulcompi	⊢ ( 𝑥 ·_N 𝑦 ) = ( 𝑦 ·_N 𝑥 )
19		mulasspi	⊢ ( ( 𝑥 ·_N 𝑦 ) ·_N 𝑧 ) = ( 𝑥 ·_N ( 𝑦 ·_N 𝑧 ) )
20		fvex	⊢ ( 2^nd ‘ 𝐵 ) ∈ V
21	15 16 17 18 19 20	caov4	⊢ ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) = ( ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐴 ) ) ·_N ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐵 ) ) )
22		fvex	⊢ ( 1^st ‘ 𝐵 ) ∈ V
23		fvex	⊢ ( 2^nd ‘ 𝐴 ) ∈ V
24	15 16 22 18 19 23	caov4	⊢ ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) = ( ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐵 ) ) ·_N ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐴 ) ) )
25	21 24	breq12i	⊢ ( ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) <_N ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) ↔ ( ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐴 ) ) ·_N ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) <_N ( ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐵 ) ) ·_N ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
26	14 25	bitrdi	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) <_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ↔ ( ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐴 ) ) ·_N ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) <_N ( ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐵 ) ) ·_N ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) ) )
27		ordpipq	⊢ ( ⟨ ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐴 ) ) , ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐴 ) ) ⟩ <_pQ ⟨ ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐵 ) ) , ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐵 ) ) ⟩ ↔ ( ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐴 ) ) ·_N ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) <_N ( ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐵 ) ) ·_N ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
28	26 27	bitr4di	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) <_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ↔ ⟨ ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐴 ) ) , ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐴 ) ) ⟩ <_pQ ⟨ ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐵 ) ) , ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐵 ) ) ⟩ ) )
29		elpqn	⊢ ( 𝐴 ∈ Q → 𝐴 ∈ ( N × N ) )
30	29	3ad2ant1	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → 𝐴 ∈ ( N × N ) )
31		mulpipq2	⊢ ( ( 𝐶 ∈ ( N × N ) ∧ 𝐴 ∈ ( N × N ) ) → ( 𝐶 ·_pQ 𝐴 ) = ⟨ ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐴 ) ) , ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐴 ) ) ⟩ )
32	6 30 31	syl2anc	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐶 ·_pQ 𝐴 ) = ⟨ ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐴 ) ) , ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐴 ) ) ⟩ )
33		elpqn	⊢ ( 𝐵 ∈ Q → 𝐵 ∈ ( N × N ) )
34	33	3ad2ant2	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → 𝐵 ∈ ( N × N ) )
35		mulpipq2	⊢ ( ( 𝐶 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐶 ·_pQ 𝐵 ) = ⟨ ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐵 ) ) , ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐵 ) ) ⟩ )
36	6 34 35	syl2anc	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐶 ·_pQ 𝐵 ) = ⟨ ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐵 ) ) , ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐵 ) ) ⟩ )
37	32 36	breq12d	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( 𝐶 ·_pQ 𝐴 ) <_pQ ( 𝐶 ·_pQ 𝐵 ) ↔ ⟨ ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐴 ) ) , ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐴 ) ) ⟩ <_pQ ⟨ ( ( 1^st ‘ 𝐶 ) ·_N ( 1^st ‘ 𝐵 ) ) , ( ( 2^nd ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐵 ) ) ⟩ ) )
38	28 37	bitr4d	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) <_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ↔ ( 𝐶 ·_pQ 𝐴 ) <_pQ ( 𝐶 ·_pQ 𝐵 ) ) )
39		ordpinq	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐴 <_Q 𝐵 ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) <_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
40	39	3adant3	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐴 <_Q 𝐵 ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) <_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
41		mulpqnq	⊢ ( ( 𝐶 ∈ Q ∧ 𝐴 ∈ Q ) → ( 𝐶 ·_Q 𝐴 ) = ( [Q] ‘ ( 𝐶 ·_pQ 𝐴 ) ) )
42	41	ancoms	⊢ ( ( 𝐴 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐶 ·_Q 𝐴 ) = ( [Q] ‘ ( 𝐶 ·_pQ 𝐴 ) ) )
43	42	3adant2	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐶 ·_Q 𝐴 ) = ( [Q] ‘ ( 𝐶 ·_pQ 𝐴 ) ) )
44		mulpqnq	⊢ ( ( 𝐶 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐶 ·_Q 𝐵 ) = ( [Q] ‘ ( 𝐶 ·_pQ 𝐵 ) ) )
45	44	ancoms	⊢ ( ( 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐶 ·_Q 𝐵 ) = ( [Q] ‘ ( 𝐶 ·_pQ 𝐵 ) ) )
46	45	3adant1	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐶 ·_Q 𝐵 ) = ( [Q] ‘ ( 𝐶 ·_pQ 𝐵 ) ) )
47	43 46	breq12d	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( 𝐶 ·_Q 𝐴 ) <_Q ( 𝐶 ·_Q 𝐵 ) ↔ ( [Q] ‘ ( 𝐶 ·_pQ 𝐴 ) ) <_Q ( [Q] ‘ ( 𝐶 ·_pQ 𝐵 ) ) ) )
48		lterpq	⊢ ( ( 𝐶 ·_pQ 𝐴 ) <_pQ ( 𝐶 ·_pQ 𝐵 ) ↔ ( [Q] ‘ ( 𝐶 ·_pQ 𝐴 ) ) <_Q ( [Q] ‘ ( 𝐶 ·_pQ 𝐵 ) ) )
49	47 48	bitr4di	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( 𝐶 ·_Q 𝐴 ) <_Q ( 𝐶 ·_Q 𝐵 ) ↔ ( 𝐶 ·_pQ 𝐴 ) <_pQ ( 𝐶 ·_pQ 𝐵 ) ) )
50	38 40 49	3bitr4d	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐴 <_Q 𝐵 ↔ ( 𝐶 ·_Q 𝐴 ) <_Q ( 𝐶 ·_Q 𝐵 ) ) )
51	2 3 4 50	ndmovord	⊢ ( 𝐶 ∈ Q → ( 𝐴 <_Q 𝐵 ↔ ( 𝐶 ·_Q 𝐴 ) <_Q ( 𝐶 ·_Q 𝐵 ) ) )

Metamath Proof Explorer

Theorem ltmnq

Proof