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 ( 𝐴 <Q 𝐵 ↔ ( *Q ‘ 𝐵 ) <Q ( *Q ‘ 𝐴 ) )

Proof

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