Metamath Proof Explorer

Theorem 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 ⊢ C ∈ 𝑸 → A < 𝑸 B ↔ C ⋅ 𝑸 A < 𝑸 C ⋅ 𝑸 B

Proof

Step Hyp Ref Expression
1 mulnqf ⊢ ⋅ 𝑸 : 𝑸 × 𝑸 ⟶ 𝑸
2 1 fdmi ⊢ dom ⁡ ⋅ 𝑸 = 𝑸 × 𝑸
3 ltrelnq ⊢ < 𝑸 ⊆ 𝑸 × 𝑸
4 0nnq ⊢ ¬ ∅ ∈ 𝑸
5 elpqn ⊢ C ∈ 𝑸 → C ∈ 𝑵 × 𝑵
6 5 3ad2ant3 ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → C ∈ 𝑵 × 𝑵
7 xp1st ⊢ C ∈ 𝑵 × 𝑵 → 1 st ⁡ C ∈ 𝑵
8 6 7 syl ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 1 st ⁡ C ∈ 𝑵
9 xp2nd ⊢ C ∈ 𝑵 × 𝑵 → 2 nd ⁡ C ∈ 𝑵
10 6 9 syl ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 2 nd ⁡ C ∈ 𝑵
11 mulclpi ⊢ 1 st ⁡ C ∈ 𝑵 ∧ 2 nd ⁡ C ∈ 𝑵 → 1 st ⁡ C ⋅ 𝑵 2 nd ⁡ C ∈ 𝑵
12 8 10 11 syl2anc ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 1 st ⁡ C ⋅ 𝑵 2 nd ⁡ C ∈ 𝑵
13 ltmpi ⊢ 1 st ⁡ C ⋅ 𝑵 2 nd ⁡ C ∈ 𝑵 → 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B < 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A ↔ 1 st ⁡ C ⋅ 𝑵 2 nd ⁡ C ⋅ 𝑵 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B < 𝑵 1 st ⁡ C ⋅ 𝑵 2 nd ⁡ C ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A
14 12 13 syl ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B < 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A ↔ 1 st ⁡ C ⋅ 𝑵 2 nd ⁡ C ⋅ 𝑵 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B < 𝑵 1 st ⁡ C ⋅ 𝑵 2 nd ⁡ C ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A
15 fvex ⊢ 1 st ⁡ C ∈ V
16 fvex ⊢ 2 nd ⁡ C ∈ V
17 fvex ⊢ 1 st ⁡ A ∈ V
18 mulcompi ⊢ x ⋅ 𝑵 y = y ⋅ 𝑵 x
19 mulasspi ⊢ x ⋅ 𝑵 y ⋅ 𝑵 z = x ⋅ 𝑵 y ⋅ 𝑵 z
20 fvex ⊢ 2 nd ⁡ B ∈ V
21 15 16 17 18 19 20 caov4 ⊢ 1 st ⁡ C ⋅ 𝑵 2 nd ⁡ C ⋅ 𝑵 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B = 1 st ⁡ C ⋅ 𝑵 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ B
22 fvex ⊢ 1 st ⁡ B ∈ V
23 fvex ⊢ 2 nd ⁡ A ∈ V
24 15 16 22 18 19 23 caov4 ⊢ 1 st ⁡ C ⋅ 𝑵 2 nd ⁡ C ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A = 1 st ⁡ C ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ A
25 21 24 breq12i ⊢ 1 st ⁡ C ⋅ 𝑵 2 nd ⁡ C ⋅ 𝑵 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B < 𝑵 1 st ⁡ C ⋅ 𝑵 2 nd ⁡ C ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A ↔ 1 st ⁡ C ⋅ 𝑵 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ B < 𝑵 1 st ⁡ C ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ A
26 14 25 bitrdi ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B < 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A ↔ 1 st ⁡ C ⋅ 𝑵 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ B < 𝑵 1 st ⁡ C ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ A
27 ordpipq ⊢ 1 st ⁡ C ⋅ 𝑵 1 st ⁡ A 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ A < 𝑝𝑸 1 st ⁡ C ⋅ 𝑵 1 st ⁡ B 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ B ↔ 1 st ⁡ C ⋅ 𝑵 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ B < 𝑵 1 st ⁡ C ⋅ 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ A
28 26 27 bitr4di ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B < 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A ↔ 1 st ⁡ C ⋅ 𝑵 1 st ⁡ A 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ A < 𝑝𝑸 1 st ⁡ C ⋅ 𝑵 1 st ⁡ B 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ B
29 elpqn ⊢ A ∈ 𝑸 → A ∈ 𝑵 × 𝑵
30 29 3ad2ant1 ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → A ∈ 𝑵 × 𝑵
31 mulpipq2 ⊢ C ∈ 𝑵 × 𝑵 ∧ A ∈ 𝑵 × 𝑵 → C ⋅ 𝑝𝑸 A = 1 st ⁡ C ⋅ 𝑵 1 st ⁡ A 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ A
32 6 30 31 syl2anc ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → C ⋅ 𝑝𝑸 A = 1 st ⁡ C ⋅ 𝑵 1 st ⁡ A 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ A
33 elpqn ⊢ B ∈ 𝑸 → B ∈ 𝑵 × 𝑵
34 33 3ad2ant2 ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → B ∈ 𝑵 × 𝑵
35 mulpipq2 ⊢ C ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 → C ⋅ 𝑝𝑸 B = 1 st ⁡ C ⋅ 𝑵 1 st ⁡ B 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ B
36 6 34 35 syl2anc ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → C ⋅ 𝑝𝑸 B = 1 st ⁡ C ⋅ 𝑵 1 st ⁡ B 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ B
37 32 36 breq12d ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → C ⋅ 𝑝𝑸 A < 𝑝𝑸 C ⋅ 𝑝𝑸 B ↔ 1 st ⁡ C ⋅ 𝑵 1 st ⁡ A 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ A < 𝑝𝑸 1 st ⁡ C ⋅ 𝑵 1 st ⁡ B 2 nd ⁡ C ⋅ 𝑵 2 nd ⁡ B
38 28 37 bitr4d ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B < 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A ↔ C ⋅ 𝑝𝑸 A < 𝑝𝑸 C ⋅ 𝑝𝑸 B
39 ordpinq ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → A < 𝑸 B ↔ 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B < 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A
40 39 3adant3 ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → A < 𝑸 B ↔ 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B < 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A
41 mulpqnq ⊢ C ∈ 𝑸 ∧ A ∈ 𝑸 → C ⋅ 𝑸 A = / 𝑸 ⁡ C ⋅ 𝑝𝑸 A
42 41 ancoms ⊢ A ∈ 𝑸 ∧ C ∈ 𝑸 → C ⋅ 𝑸 A = / 𝑸 ⁡ C ⋅ 𝑝𝑸 A
43 42 3adant2 ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → C ⋅ 𝑸 A = / 𝑸 ⁡ C ⋅ 𝑝𝑸 A
44 mulpqnq ⊢ C ∈ 𝑸 ∧ B ∈ 𝑸 → C ⋅ 𝑸 B = / 𝑸 ⁡ C ⋅ 𝑝𝑸 B
45 44 ancoms ⊢ B ∈ 𝑸 ∧ C ∈ 𝑸 → C ⋅ 𝑸 B = / 𝑸 ⁡ C ⋅ 𝑝𝑸 B
46 45 3adant1 ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → C ⋅ 𝑸 B = / 𝑸 ⁡ C ⋅ 𝑝𝑸 B
47 43 46 breq12d ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → C ⋅ 𝑸 A < 𝑸 C ⋅ 𝑸 B ↔ / 𝑸 ⁡ C ⋅ 𝑝𝑸 A < 𝑸 / 𝑸 ⁡ C ⋅ 𝑝𝑸 B
48 lterpq ⊢ C ⋅ 𝑝𝑸 A < 𝑝𝑸 C ⋅ 𝑝𝑸 B ↔ / 𝑸 ⁡ C ⋅ 𝑝𝑸 A < 𝑸 / 𝑸 ⁡ C ⋅ 𝑝𝑸 B
49 47 48 bitr4di ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → C ⋅ 𝑸 A < 𝑸 C ⋅ 𝑸 B ↔ C ⋅ 𝑝𝑸 A < 𝑝𝑸 C ⋅ 𝑝𝑸 B
50 38 40 49 3bitr4d ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 ∧ C ∈ 𝑸 → A < 𝑸 B ↔ C ⋅ 𝑸 A < 𝑸 C ⋅ 𝑸 B
51 2 3 4 50 ndmovord ⊢ C ∈ 𝑸 → A < 𝑸 B ↔ C ⋅ 𝑸 A < 𝑸 C ⋅ 𝑸 B