ltsonq

Description: 'Less than' is a strict ordering on positive fractions. (Contributed by NM, 19-Feb-1996) (Revised by Mario Carneiro, 4-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	ltsonq	$⊢ <_{𝑸} Or 𝑸$

Proof

Step	Hyp	Ref	Expression
1		elpqn	$⊢ x \in 𝑸 \to x \in (𝑵 \times 𝑵)$
2	1	adantr	$⊢ (x \in 𝑸 \land y \in 𝑸) \to x \in (𝑵 \times 𝑵)$
3		xp1st	$⊢ x \in (𝑵 \times 𝑵) \to 1^{st} (x) \in 𝑵$
4	2 3	syl	$⊢ (x \in 𝑸 \land y \in 𝑸) \to 1^{st} (x) \in 𝑵$
5		elpqn	$⊢ y \in 𝑸 \to y \in (𝑵 \times 𝑵)$
6	5	adantl	$⊢ (x \in 𝑸 \land y \in 𝑸) \to y \in (𝑵 \times 𝑵)$
7		xp2nd	$⊢ y \in (𝑵 \times 𝑵) \to 2^{nd} (y) \in 𝑵$
8	6 7	syl	$⊢ (x \in 𝑸 \land y \in 𝑸) \to 2^{nd} (y) \in 𝑵$
9		mulclpi	$⊢ (1^{st} (x) \in 𝑵 \land 2^{nd} (y) \in 𝑵) \to 1^{st} (x) \cdot_{𝑵} 2^{nd} (y) \in 𝑵$
10	4 8 9	syl2anc	$⊢ (x \in 𝑸 \land y \in 𝑸) \to 1^{st} (x) \cdot_{𝑵} 2^{nd} (y) \in 𝑵$
11		xp1st	$⊢ y \in (𝑵 \times 𝑵) \to 1^{st} (y) \in 𝑵$
12	6 11	syl	$⊢ (x \in 𝑸 \land y \in 𝑸) \to 1^{st} (y) \in 𝑵$
13		xp2nd	$⊢ x \in (𝑵 \times 𝑵) \to 2^{nd} (x) \in 𝑵$
14	2 13	syl	$⊢ (x \in 𝑸 \land y \in 𝑸) \to 2^{nd} (x) \in 𝑵$
15		mulclpi	$⊢ (1^{st} (y) \in 𝑵 \land 2^{nd} (x) \in 𝑵) \to 1^{st} (y) \cdot_{𝑵} 2^{nd} (x) \in 𝑵$
16	12 14 15	syl2anc	$⊢ (x \in 𝑸 \land y \in 𝑸) \to 1^{st} (y) \cdot_{𝑵} 2^{nd} (x) \in 𝑵$
17		ltsopi	$⊢ <_{𝑵} Or 𝑵$
18		sotric	$⊢ (<_{𝑵} Or 𝑵 \land (1^{st} (x) \cdot_{𝑵} 2^{nd} (y) \in 𝑵 \land 1^{st} (y) \cdot_{𝑵} 2^{nd} (x) \in 𝑵)) \to ((1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)) \leftrightarrow \neg (1^{st} (x) \cdot_{𝑵} 2^{nd} (y) = 1^{st} (y) \cdot_{𝑵} 2^{nd} (x) \lor (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)) <_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (y))))$
19	17 18	mpan	$⊢ (1^{st} (x) \cdot_{𝑵} 2^{nd} (y) \in 𝑵 \land 1^{st} (y) \cdot_{𝑵} 2^{nd} (x) \in 𝑵) \to ((1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)) \leftrightarrow \neg (1^{st} (x) \cdot_{𝑵} 2^{nd} (y) = 1^{st} (y) \cdot_{𝑵} 2^{nd} (x) \lor (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)) <_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (y))))$
20	10 16 19	syl2anc	$⊢ (x \in 𝑸 \land y \in 𝑸) \to ((1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)) \leftrightarrow \neg (1^{st} (x) \cdot_{𝑵} 2^{nd} (y) = 1^{st} (y) \cdot_{𝑵} 2^{nd} (x) \lor (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)) <_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (y))))$
21		ordpinq	$⊢ (x \in 𝑸 \land y \in 𝑸) \to (x <_{𝑸} y \leftrightarrow (1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)))$
22		fveq2	$⊢ x = y \to 1^{st} (x) = 1^{st} (y)$
23		fveq2	$⊢ x = y \to 2^{nd} (x) = 2^{nd} (y)$
24	23	eqcomd	$⊢ x = y \to 2^{nd} (y) = 2^{nd} (x)$
25	22 24	oveq12d	$⊢ x = y \to 1^{st} (x) \cdot_{𝑵} 2^{nd} (y) = 1^{st} (y) \cdot_{𝑵} 2^{nd} (x)$
26		enqbreq2	$⊢ (x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \to (x ~_{𝑸} y \leftrightarrow 1^{st} (x) \cdot_{𝑵} 2^{nd} (y) = 1^{st} (y) \cdot_{𝑵} 2^{nd} (x))$
27	1 5 26	syl2an	$⊢ (x \in 𝑸 \land y \in 𝑸) \to (x ~_{𝑸} y \leftrightarrow 1^{st} (x) \cdot_{𝑵} 2^{nd} (y) = 1^{st} (y) \cdot_{𝑵} 2^{nd} (x))$
28		enqeq	$⊢ (x \in 𝑸 \land y \in 𝑸 \land x ~_{𝑸} y) \to x = y$
29	28	3expia	$⊢ (x \in 𝑸 \land y \in 𝑸) \to (x ~_{𝑸} y \to x = y)$
30	27 29	sylbird	$⊢ (x \in 𝑸 \land y \in 𝑸) \to (1^{st} (x) \cdot_{𝑵} 2^{nd} (y) = 1^{st} (y) \cdot_{𝑵} 2^{nd} (x) \to x = y)$
31	25 30	impbid2	$⊢ (x \in 𝑸 \land y \in 𝑸) \to (x = y \leftrightarrow 1^{st} (x) \cdot_{𝑵} 2^{nd} (y) = 1^{st} (y) \cdot_{𝑵} 2^{nd} (x))$
32		ordpinq	$⊢ (y \in 𝑸 \land x \in 𝑸) \to (y <_{𝑸} x \leftrightarrow (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)) <_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (y)))$
33	32	ancoms	$⊢ (x \in 𝑸 \land y \in 𝑸) \to (y <_{𝑸} x \leftrightarrow (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)) <_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (y)))$
34	31 33	orbi12d	$⊢ (x \in 𝑸 \land y \in 𝑸) \to ((x = y \lor y <_{𝑸} x) \leftrightarrow (1^{st} (x) \cdot_{𝑵} 2^{nd} (y) = 1^{st} (y) \cdot_{𝑵} 2^{nd} (x) \lor (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)) <_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (y))))$
35	34	notbid	$⊢ (x \in 𝑸 \land y \in 𝑸) \to (\neg (x = y \lor y <_{𝑸} x) \leftrightarrow \neg (1^{st} (x) \cdot_{𝑵} 2^{nd} (y) = 1^{st} (y) \cdot_{𝑵} 2^{nd} (x) \lor (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)) <_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (y))))$
36	20 21 35	3bitr4d	$⊢ (x \in 𝑸 \land y \in 𝑸) \to (x <_{𝑸} y \leftrightarrow \neg (x = y \lor y <_{𝑸} x))$
37	21	3adant3	$⊢ (x \in 𝑸 \land y \in 𝑸 \land z \in 𝑸) \to (x <_{𝑸} y \leftrightarrow (1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)))$
38		elpqn	$⊢ z \in 𝑸 \to z \in (𝑵 \times 𝑵)$
39	38	3ad2ant3	$⊢ (x \in 𝑸 \land y \in 𝑸 \land z \in 𝑸) \to z \in (𝑵 \times 𝑵)$
40		xp2nd	$⊢ z \in (𝑵 \times 𝑵) \to 2^{nd} (z) \in 𝑵$
41		ltmpi	$⊢ 2^{nd} (z) \in 𝑵 \to ((1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)) \leftrightarrow (2^{nd} (z) \cdot_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (y))) <_{𝑵} (2^{nd} (z) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x))))$
42	39 40 41	3syl	$⊢ (x \in 𝑸 \land y \in 𝑸 \land z \in 𝑸) \to ((1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)) \leftrightarrow (2^{nd} (z) \cdot_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (y))) <_{𝑵} (2^{nd} (z) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x))))$
43	37 42	bitrd	$⊢ (x \in 𝑸 \land y \in 𝑸 \land z \in 𝑸) \to (x <_{𝑸} y \leftrightarrow (2^{nd} (z) \cdot_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (y))) <_{𝑵} (2^{nd} (z) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x))))$
44		ordpinq	$⊢ (y \in 𝑸 \land z \in 𝑸) \to (y <_{𝑸} z \leftrightarrow (1^{st} (y) \cdot_{𝑵} 2^{nd} (z)) <_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (y)))$
45	44	3adant1	$⊢ (x \in 𝑸 \land y \in 𝑸 \land z \in 𝑸) \to (y <_{𝑸} z \leftrightarrow (1^{st} (y) \cdot_{𝑵} 2^{nd} (z)) <_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (y)))$
46	1	3ad2ant1	$⊢ (x \in 𝑸 \land y \in 𝑸 \land z \in 𝑸) \to x \in (𝑵 \times 𝑵)$
47		ltmpi	$⊢ 2^{nd} (x) \in 𝑵 \to ((1^{st} (y) \cdot_{𝑵} 2^{nd} (z)) <_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (y)) \leftrightarrow (2^{nd} (x) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (z))) <_{𝑵} (2^{nd} (x) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (y))))$
48	46 13 47	3syl	$⊢ (x \in 𝑸 \land y \in 𝑸 \land z \in 𝑸) \to ((1^{st} (y) \cdot_{𝑵} 2^{nd} (z)) <_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (y)) \leftrightarrow (2^{nd} (x) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (z))) <_{𝑵} (2^{nd} (x) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (y))))$
49	45 48	bitrd	$⊢ (x \in 𝑸 \land y \in 𝑸 \land z \in 𝑸) \to (y <_{𝑸} z \leftrightarrow (2^{nd} (x) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (z))) <_{𝑵} (2^{nd} (x) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (y))))$
50	43 49	anbi12d	$⊢ (x \in 𝑸 \land y \in 𝑸 \land z \in 𝑸) \to ((x <_{𝑸} y \land y <_{𝑸} z) \leftrightarrow ((2^{nd} (z) \cdot_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (y))) <_{𝑵} (2^{nd} (z) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x))) \land (2^{nd} (x) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (z))) <_{𝑵} (2^{nd} (x) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (y)))))$
51		fvex	$⊢ 2^{nd} (x) \in V$
52		fvex	$⊢ 1^{st} (y) \in V$
53		fvex	$⊢ 2^{nd} (z) \in V$
54		mulcompi	$⊢ r \cdot_{𝑵} s = s \cdot_{𝑵} r$
55		mulasspi	$⊢ (r \cdot_{𝑵} s) \cdot_{𝑵} t = r \cdot_{𝑵} (s \cdot_{𝑵} t)$
56	51 52 53 54 55	caov13	$⊢ 2^{nd} (x) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (z)) = 2^{nd} (z) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x))$
57		fvex	$⊢ 1^{st} (z) \in V$
58		fvex	$⊢ 2^{nd} (y) \in V$
59	51 57 58 54 55	caov13	$⊢ 2^{nd} (x) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (y)) = 2^{nd} (y) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (x))$
60	56 59	breq12i	$⊢ (2^{nd} (x) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (z))) <_{𝑵} (2^{nd} (x) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (y))) \leftrightarrow (2^{nd} (z) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x))) <_{𝑵} (2^{nd} (y) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (x)))$
61		fvex	$⊢ 1^{st} (x) \in V$
62	53 61 58 54 55	caov13	$⊢ 2^{nd} (z) \cdot_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) = 2^{nd} (y) \cdot_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (z))$
63		ltrelpi	$⊢ <_{𝑵} \subseteq 𝑵 \times 𝑵$
64	17 63	sotri	$⊢ ((2^{nd} (z) \cdot_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (y))) <_{𝑵} (2^{nd} (z) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x))) \land (2^{nd} (z) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x))) <_{𝑵} (2^{nd} (y) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (x)))) \to (2^{nd} (z) \cdot_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (y))) <_{𝑵} (2^{nd} (y) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (x)))$
65	62 64	eqbrtrrid	$⊢ ((2^{nd} (z) \cdot_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (y))) <_{𝑵} (2^{nd} (z) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x))) \land (2^{nd} (z) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x))) <_{𝑵} (2^{nd} (y) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (x)))) \to (2^{nd} (y) \cdot_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (z))) <_{𝑵} (2^{nd} (y) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (x)))$
66	60 65	sylan2b	$⊢ ((2^{nd} (z) \cdot_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (y))) <_{𝑵} (2^{nd} (z) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x))) \land (2^{nd} (x) \cdot_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (z))) <_{𝑵} (2^{nd} (x) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (y)))) \to (2^{nd} (y) \cdot_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (z))) <_{𝑵} (2^{nd} (y) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (x)))$
67	50 66	syl6bi	$⊢ (x \in 𝑸 \land y \in 𝑸 \land z \in 𝑸) \to ((x <_{𝑸} y \land y <_{𝑸} z) \to (2^{nd} (y) \cdot_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (z))) <_{𝑵} (2^{nd} (y) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (x))))$
68		ordpinq	$⊢ (x \in 𝑸 \land z \in 𝑸) \to (x <_{𝑸} z \leftrightarrow (1^{st} (x) \cdot_{𝑵} 2^{nd} (z)) <_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (x)))$
69	68	3adant2	$⊢ (x \in 𝑸 \land y \in 𝑸 \land z \in 𝑸) \to (x <_{𝑸} z \leftrightarrow (1^{st} (x) \cdot_{𝑵} 2^{nd} (z)) <_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (x)))$
70	5	3ad2ant2	$⊢ (x \in 𝑸 \land y \in 𝑸 \land z \in 𝑸) \to y \in (𝑵 \times 𝑵)$
71		ltmpi	$⊢ 2^{nd} (y) \in 𝑵 \to ((1^{st} (x) \cdot_{𝑵} 2^{nd} (z)) <_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (x)) \leftrightarrow (2^{nd} (y) \cdot_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (z))) <_{𝑵} (2^{nd} (y) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (x))))$
72	70 7 71	3syl	$⊢ (x \in 𝑸 \land y \in 𝑸 \land z \in 𝑸) \to ((1^{st} (x) \cdot_{𝑵} 2^{nd} (z)) <_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (x)) \leftrightarrow (2^{nd} (y) \cdot_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (z))) <_{𝑵} (2^{nd} (y) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (x))))$
73	69 72	bitrd	$⊢ (x \in 𝑸 \land y \in 𝑸 \land z \in 𝑸) \to (x <_{𝑸} z \leftrightarrow (2^{nd} (y) \cdot_{𝑵} (1^{st} (x) \cdot_{𝑵} 2^{nd} (z))) <_{𝑵} (2^{nd} (y) \cdot_{𝑵} (1^{st} (z) \cdot_{𝑵} 2^{nd} (x))))$
74	67 73	sylibrd	$⊢ (x \in 𝑸 \land y \in 𝑸 \land z \in 𝑸) \to ((x <_{𝑸} y \land y <_{𝑸} z) \to x <_{𝑸} z)$
75	36 74	isso2i	$⊢ <_{𝑸} Or 𝑸$

Metamath Proof Explorer

Theorem ltsonq

Proof