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