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	eqtrid	⊢ ( ( 𝑥 ∈ 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	eqtrid	⊢ ( ( 𝑥 ∈ 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 ‘ 𝐴 ) )