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 \leftrightarrow _{𝑸} (B) <_{𝑸} _{𝑸} (A)$

Proof

Step	Hyp	Ref	Expression
1		ltrelnq	$⊢ <_{𝑸} \subseteq 𝑸 \times 𝑸$
2	1	brel	$⊢ A <_{𝑸} B \to (A \in 𝑸 \land B \in 𝑸)$
3	1	brel	$⊢ _{𝑸} (B) <_{𝑸} _{𝑸} (A) \to (_{𝑸} (B) \in 𝑸 \land _{𝑸} (A) \in 𝑸)$
4		dmrecnq	$⊢ dom *_{𝑸} = 𝑸$
5		0nnq	$⊢ \neg \emptyset \in 𝑸$
6	4 5	ndmfvrcl	$⊢ *_{𝑸} (B) \in 𝑸 \to B \in 𝑸$
7	4 5	ndmfvrcl	$⊢ *_{𝑸} (A) \in 𝑸 \to A \in 𝑸$
8	6 7	anim12ci	$⊢ (_{𝑸} (B) \in 𝑸 \land _{𝑸} (A) \in 𝑸) \to (A \in 𝑸 \land B \in 𝑸)$
9	3 8	syl	$⊢ _{𝑸} (B) <_{𝑸} _{𝑸} (A) \to (A \in 𝑸 \land B \in 𝑸)$
10		breq1	$⊢ x = A \to (x <_{𝑸} y \leftrightarrow A <_{𝑸} y)$
11		fveq2	$⊢ x = A \to _{𝑸} (x) = _{𝑸} (A)$
12	11	breq2d	$⊢ x = A \to (_{𝑸} (y) <_{𝑸} _{𝑸} (x) \leftrightarrow _{𝑸} (y) <_{𝑸} _{𝑸} (A))$
13	10 12	bibi12d	$⊢ x = A \to ((x <_{𝑸} y \leftrightarrow _{𝑸} (y) <_{𝑸} _{𝑸} (x)) \leftrightarrow (A <_{𝑸} y \leftrightarrow _{𝑸} (y) <_{𝑸} _{𝑸} (A)))$
14		breq2	$⊢ y = B \to (A <_{𝑸} y \leftrightarrow A <_{𝑸} B)$
15		fveq2	$⊢ y = B \to _{𝑸} (y) = _{𝑸} (B)$
16	15	breq1d	$⊢ y = B \to (_{𝑸} (y) <_{𝑸} _{𝑸} (A) \leftrightarrow _{𝑸} (B) <_{𝑸} _{𝑸} (A))$
17	14 16	bibi12d	$⊢ y = B \to ((A <_{𝑸} y \leftrightarrow _{𝑸} (y) <_{𝑸} _{𝑸} (A)) \leftrightarrow (A <_{𝑸} B \leftrightarrow _{𝑸} (B) <_{𝑸} _{𝑸} (A)))$
18		recclnq	$⊢ x \in 𝑸 \to *_{𝑸} (x) \in 𝑸$
19		recclnq	$⊢ y \in 𝑸 \to *_{𝑸} (y) \in 𝑸$
20		mulclnq	$⊢ (_{𝑸} (x) \in 𝑸 \land _{𝑸} (y) \in 𝑸) \to _{𝑸} (x) \cdot_{𝑸} _{𝑸} (y) \in 𝑸$
21	18 19 20	syl2an	$⊢ (x \in 𝑸 \land y \in 𝑸) \to _{𝑸} (x) \cdot_{𝑸} _{𝑸} (y) \in 𝑸$
22		ltmnq	$⊢ _{𝑸} (x) \cdot_{𝑸} _{𝑸} (y) \in 𝑸 \to (x <_{𝑸} y \leftrightarrow ((_{𝑸} (x) \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x) <_{𝑸} ((_{𝑸} (x) \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} y))$
23	21 22	syl	$⊢ (x \in 𝑸 \land y \in 𝑸) \to (x <_{𝑸} y \leftrightarrow ((_{𝑸} (x) \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x) <_{𝑸} ((_{𝑸} (x) \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} y))$
24		mulcomnq	$⊢ (_{𝑸} (x) \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x = x \cdot_{𝑸} (_{𝑸} (x) \cdot_{𝑸} _{𝑸} (y))$
25		mulassnq	$⊢ (x \cdot_{𝑸} _{𝑸} (x)) \cdot_{𝑸} _{𝑸} (y) = x \cdot_{𝑸} (_{𝑸} (x) \cdot_{𝑸} _{𝑸} (y))$
26		mulcomnq	$⊢ (x \cdot_{𝑸} _{𝑸} (x)) \cdot_{𝑸} _{𝑸} (y) = _{𝑸} (y) \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (x))$
27	24 25 26	3eqtr2i	$⊢ (_{𝑸} (x) \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x = _{𝑸} (y) \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (x))$
28		recidnq	$⊢ x \in 𝑸 \to x \cdot_{𝑸} *_{𝑸} (x) = 1_{𝑸}$
29	28	oveq2d	$⊢ x \in 𝑸 \to _{𝑸} (y) \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (x)) = *_{𝑸} (y) \cdot_{𝑸} 1_{𝑸}$
30		mulidnq	$⊢ _{𝑸} (y) \in 𝑸 \to _{𝑸} (y) \cdot_{𝑸} 1_{𝑸} = *_{𝑸} (y)$
31	19 30	syl	$⊢ y \in 𝑸 \to _{𝑸} (y) \cdot_{𝑸} 1_{𝑸} = _{𝑸} (y)$
32	29 31	sylan9eq	$⊢ (x \in 𝑸 \land y \in 𝑸) \to _{𝑸} (y) \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (x)) = *_{𝑸} (y)$
33	27 32	eqtrid	$⊢ (x \in 𝑸 \land y \in 𝑸) \to (_{𝑸} (x) \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x = *_{𝑸} (y)$
34		mulassnq	$⊢ (_{𝑸} (x) \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} y = _{𝑸} (x) \cdot_{𝑸} (_{𝑸} (y) \cdot_{𝑸} y)$
35		mulcomnq	$⊢ _{𝑸} (y) \cdot_{𝑸} y = y \cdot_{𝑸} _{𝑸} (y)$
36	35	oveq2i	$⊢ _{𝑸} (x) \cdot_{𝑸} (_{𝑸} (y) \cdot_{𝑸} y) = _{𝑸} (x) \cdot_{𝑸} (y \cdot_{𝑸} _{𝑸} (y))$
37	34 36	eqtri	$⊢ (_{𝑸} (x) \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} y = _{𝑸} (x) \cdot_{𝑸} (y \cdot_{𝑸} _{𝑸} (y))$
38		recidnq	$⊢ y \in 𝑸 \to y \cdot_{𝑸} *_{𝑸} (y) = 1_{𝑸}$
39	38	oveq2d	$⊢ y \in 𝑸 \to _{𝑸} (x) \cdot_{𝑸} (y \cdot_{𝑸} _{𝑸} (y)) = *_{𝑸} (x) \cdot_{𝑸} 1_{𝑸}$
40		mulidnq	$⊢ _{𝑸} (x) \in 𝑸 \to _{𝑸} (x) \cdot_{𝑸} 1_{𝑸} = *_{𝑸} (x)$
41	18 40	syl	$⊢ x \in 𝑸 \to _{𝑸} (x) \cdot_{𝑸} 1_{𝑸} = _{𝑸} (x)$
42	39 41	sylan9eqr	$⊢ (x \in 𝑸 \land y \in 𝑸) \to _{𝑸} (x) \cdot_{𝑸} (y \cdot_{𝑸} _{𝑸} (y)) = *_{𝑸} (x)$
43	37 42	eqtrid	$⊢ (x \in 𝑸 \land y \in 𝑸) \to (_{𝑸} (x) \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} y = *_{𝑸} (x)$
44	33 43	breq12d	$⊢ (x \in 𝑸 \land y \in 𝑸) \to (((_{𝑸} (x) \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x) <_{𝑸} ((_{𝑸} (x) \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} y) \leftrightarrow _{𝑸} (y) <_{𝑸} _{𝑸} (x))$
45	23 44	bitrd	$⊢ (x \in 𝑸 \land y \in 𝑸) \to (x <_{𝑸} y \leftrightarrow _{𝑸} (y) <_{𝑸} _{𝑸} (x))$
46	13 17 45	vtocl2ga	$⊢ (A \in 𝑸 \land B \in 𝑸) \to (A <_{𝑸} B \leftrightarrow _{𝑸} (B) <_{𝑸} _{𝑸} (A))$
47	2 9 46	pm5.21nii	$⊢ A <_{𝑸} B \leftrightarrow _{𝑸} (B) <_{𝑸} _{𝑸} (A)$

Metamath Proof Explorer

Theorem ltrnq

Proof