Metamath Proof Explorer

Theorem ltrnq

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

Ref Expression
Assertion ltrnq ⊢ A < 𝑸 B ↔ * 𝑸 ⁡ B < 𝑸 * 𝑸 ⁡ A

Proof

Step Hyp Ref Expression
1 ltrelnq ⊢ < 𝑸 ⊆ 𝑸 × 𝑸
2 1 brel ⊢ A < 𝑸 B → A ∈ 𝑸 ∧ B ∈ 𝑸
3 1 brel ⊢ * 𝑸 ⁡ B < 𝑸 * 𝑸 ⁡ A → * 𝑸 ⁡ B ∈ 𝑸 ∧ * 𝑸 ⁡ A ∈ 𝑸
4 dmrecnq ⊢ dom ⁡ * 𝑸 = 𝑸
5 0nnq ⊢ ¬ ∅ ∈ 𝑸
6 4 5 ndmfvrcl ⊢ * 𝑸 ⁡ B ∈ 𝑸 → B ∈ 𝑸
7 4 5 ndmfvrcl ⊢ * 𝑸 ⁡ A ∈ 𝑸 → A ∈ 𝑸
8 6 7 anim12ci ⊢ * 𝑸 ⁡ B ∈ 𝑸 ∧ * 𝑸 ⁡ A ∈ 𝑸 → A ∈ 𝑸 ∧ B ∈ 𝑸
9 3 8 syl ⊢ * 𝑸 ⁡ B < 𝑸 * 𝑸 ⁡ A → A ∈ 𝑸 ∧ B ∈ 𝑸
10 breq1 ⊢ x = A → x < 𝑸 y ↔ A < 𝑸 y
11 fveq2 ⊢ x = A → * 𝑸 ⁡ x = * 𝑸 ⁡ A
12 11 breq2d ⊢ x = A → * 𝑸 ⁡ y < 𝑸 * 𝑸 ⁡ x ↔ * 𝑸 ⁡ y < 𝑸 * 𝑸 ⁡ A
13 10 12 bibi12d ⊢ x = A → x < 𝑸 y ↔ * 𝑸 ⁡ y < 𝑸 * 𝑸 ⁡ x ↔ A < 𝑸 y ↔ * 𝑸 ⁡ y < 𝑸 * 𝑸 ⁡ A
14 breq2 ⊢ y = B → A < 𝑸 y ↔ A < 𝑸 B
15 fveq2 ⊢ y = B → * 𝑸 ⁡ y = * 𝑸 ⁡ B
16 15 breq1d ⊢ y = B → * 𝑸 ⁡ y < 𝑸 * 𝑸 ⁡ A ↔ * 𝑸 ⁡ B < 𝑸 * 𝑸 ⁡ A
17 14 16 bibi12d ⊢ y = B → A < 𝑸 y ↔ * 𝑸 ⁡ y < 𝑸 * 𝑸 ⁡ A ↔ A < 𝑸 B ↔ * 𝑸 ⁡ B < 𝑸 * 𝑸 ⁡ A
18 recclnq ⊢ x ∈ 𝑸 → * 𝑸 ⁡ x ∈ 𝑸
19 recclnq ⊢ y ∈ 𝑸 → * 𝑸 ⁡ y ∈ 𝑸
20 mulclnq ⊢ * 𝑸 ⁡ x ∈ 𝑸 ∧ * 𝑸 ⁡ y ∈ 𝑸 → * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y ∈ 𝑸
21 18 19 20 syl2an ⊢ x ∈ 𝑸 ∧ y ∈ 𝑸 → * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y ∈ 𝑸
22 ltmnq ⊢ * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y ∈ 𝑸 → x < 𝑸 y ↔ * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y ⋅ 𝑸 x < 𝑸 * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y ⋅ 𝑸 y
23 21 22 syl ⊢ x ∈ 𝑸 ∧ y ∈ 𝑸 → x < 𝑸 y ↔ * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y ⋅ 𝑸 x < 𝑸 * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y ⋅ 𝑸 y
24 mulcomnq ⊢ * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y ⋅ 𝑸 x = x ⋅ 𝑸 * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y
25 mulassnq ⊢ x ⋅ 𝑸 * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y = x ⋅ 𝑸 * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y
26 mulcomnq ⊢ x ⋅ 𝑸 * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y = * 𝑸 ⁡ y ⋅ 𝑸 x ⋅ 𝑸 * 𝑸 ⁡ x
27 24 25 26 3eqtr2i ⊢ * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y ⋅ 𝑸 x = * 𝑸 ⁡ y ⋅ 𝑸 x ⋅ 𝑸 * 𝑸 ⁡ x
28 recidnq ⊢ x ∈ 𝑸 → x ⋅ 𝑸 * 𝑸 ⁡ x = 1 𝑸
29 28 oveq2d ⊢ x ∈ 𝑸 → * 𝑸 ⁡ y ⋅ 𝑸 x ⋅ 𝑸 * 𝑸 ⁡ x = * 𝑸 ⁡ y ⋅ 𝑸 1 𝑸
30 mulidnq ⊢ * 𝑸 ⁡ y ∈ 𝑸 → * 𝑸 ⁡ y ⋅ 𝑸 1 𝑸 = * 𝑸 ⁡ y
31 19 30 syl ⊢ y ∈ 𝑸 → * 𝑸 ⁡ y ⋅ 𝑸 1 𝑸 = * 𝑸 ⁡ y
32 29 31 sylan9eq ⊢ x ∈ 𝑸 ∧ y ∈ 𝑸 → * 𝑸 ⁡ y ⋅ 𝑸 x ⋅ 𝑸 * 𝑸 ⁡ x = * 𝑸 ⁡ y
33 27 32 eqtrid ⊢ x ∈ 𝑸 ∧ y ∈ 𝑸 → * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y ⋅ 𝑸 x = * 𝑸 ⁡ y
34 mulassnq ⊢ * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y ⋅ 𝑸 y = * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y ⋅ 𝑸 y
35 mulcomnq ⊢ * 𝑸 ⁡ y ⋅ 𝑸 y = y ⋅ 𝑸 * 𝑸 ⁡ y
36 35 oveq2i ⊢ * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y ⋅ 𝑸 y = * 𝑸 ⁡ x ⋅ 𝑸 y ⋅ 𝑸 * 𝑸 ⁡ y
37 34 36 eqtri ⊢ * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y ⋅ 𝑸 y = * 𝑸 ⁡ x ⋅ 𝑸 y ⋅ 𝑸 * 𝑸 ⁡ y
38 recidnq ⊢ y ∈ 𝑸 → y ⋅ 𝑸 * 𝑸 ⁡ y = 1 𝑸
39 38 oveq2d ⊢ y ∈ 𝑸 → * 𝑸 ⁡ x ⋅ 𝑸 y ⋅ 𝑸 * 𝑸 ⁡ y = * 𝑸 ⁡ x ⋅ 𝑸 1 𝑸
40 mulidnq ⊢ * 𝑸 ⁡ x ∈ 𝑸 → * 𝑸 ⁡ x ⋅ 𝑸 1 𝑸 = * 𝑸 ⁡ x
41 18 40 syl ⊢ x ∈ 𝑸 → * 𝑸 ⁡ x ⋅ 𝑸 1 𝑸 = * 𝑸 ⁡ x
42 39 41 sylan9eqr ⊢ x ∈ 𝑸 ∧ y ∈ 𝑸 → * 𝑸 ⁡ x ⋅ 𝑸 y ⋅ 𝑸 * 𝑸 ⁡ y = * 𝑸 ⁡ x
43 37 42 eqtrid ⊢ x ∈ 𝑸 ∧ y ∈ 𝑸 → * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y ⋅ 𝑸 y = * 𝑸 ⁡ x
44 33 43 breq12d ⊢ x ∈ 𝑸 ∧ y ∈ 𝑸 → * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y ⋅ 𝑸 x < 𝑸 * 𝑸 ⁡ x ⋅ 𝑸 * 𝑸 ⁡ y ⋅ 𝑸 y ↔ * 𝑸 ⁡ y < 𝑸 * 𝑸 ⁡ x
45 23 44 bitrd ⊢ x ∈ 𝑸 ∧ y ∈ 𝑸 → x < 𝑸 y ↔ * 𝑸 ⁡ y < 𝑸 * 𝑸 ⁡ x
46 13 17 45 vtocl2ga ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → A < 𝑸 B ↔ * 𝑸 ⁡ B < 𝑸 * 𝑸 ⁡ A
47 2 9 46 pm5.21nii ⊢ A < 𝑸 B ↔ * 𝑸 ⁡ B < 𝑸 * 𝑸 ⁡ A