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	⊢ <_Q Or Q

Proof

Step	Hyp	Ref	Expression
1		elpqn	⊢ ( 𝑥 ∈ Q → 𝑥 ∈ ( N × N ) )
2	1	adantr	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → 𝑥 ∈ ( N × N ) )
3		xp1st	⊢ ( 𝑥 ∈ ( N × N ) → ( 1^st ‘ 𝑥 ) ∈ N )
4	2 3	syl	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 1^st ‘ 𝑥 ) ∈ N )
5		elpqn	⊢ ( 𝑦 ∈ Q → 𝑦 ∈ ( N × N ) )
6	5	adantl	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → 𝑦 ∈ ( N × N ) )
7		xp2nd	⊢ ( 𝑦 ∈ ( N × N ) → ( 2^nd ‘ 𝑦 ) ∈ N )
8	6 7	syl	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 2^nd ‘ 𝑦 ) ∈ N )
9		mulclpi	⊢ ( ( ( 1^st ‘ 𝑥 ) ∈ N ∧ ( 2^nd ‘ 𝑦 ) ∈ N ) → ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ∈ N )
10	4 8 9	syl2anc	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ∈ N )
11		xp1st	⊢ ( 𝑦 ∈ ( N × N ) → ( 1^st ‘ 𝑦 ) ∈ N )
12	6 11	syl	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 1^st ‘ 𝑦 ) ∈ N )
13		xp2nd	⊢ ( 𝑥 ∈ ( N × N ) → ( 2^nd ‘ 𝑥 ) ∈ N )
14	2 13	syl	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 2^nd ‘ 𝑥 ) ∈ N )
15		mulclpi	⊢ ( ( ( 1^st ‘ 𝑦 ) ∈ N ∧ ( 2^nd ‘ 𝑥 ) ∈ N ) → ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ∈ N )
16	12 14 15	syl2anc	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ∈ N )
17		ltsopi	⊢ <_N Or N
18		sotric	⊢ ( ( <_N Or N ∧ ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ∈ N ∧ ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ∈ N ) ) → ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) <_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ↔ ¬ ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) = ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ∨ ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) <_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) ) )
19	17 18	mpan	⊢ ( ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ∈ N ∧ ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ∈ N ) → ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) <_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ↔ ¬ ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) = ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ∨ ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) <_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) ) )
20	10 16 19	syl2anc	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) <_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ↔ ¬ ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) = ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ∨ ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) <_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) ) )
21		ordpinq	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑥 <_Q 𝑦 ↔ ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) <_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) )
22		fveq2	⊢ ( 𝑥 = 𝑦 → ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) )
23		fveq2	⊢ ( 𝑥 = 𝑦 → ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) )
24	23	eqcomd	⊢ ( 𝑥 = 𝑦 → ( 2^nd ‘ 𝑦 ) = ( 2^nd ‘ 𝑥 ) )
25	22 24	oveq12d	⊢ ( 𝑥 = 𝑦 → ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) = ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) )
26		enqbreq2	⊢ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) → ( 𝑥 ~_Q 𝑦 ↔ ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) = ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) )
27	1 5 26	syl2an	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑥 ~_Q 𝑦 ↔ ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) = ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) )
28		enqeq	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑥 ~_Q 𝑦 ) → 𝑥 = 𝑦 )
29	28	3expia	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑥 ~_Q 𝑦 → 𝑥 = 𝑦 ) )
30	27 29	sylbird	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) = ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) → 𝑥 = 𝑦 ) )
31	25 30	impbid2	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑥 = 𝑦 ↔ ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) = ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) )
32		ordpinq	⊢ ( ( 𝑦 ∈ Q ∧ 𝑥 ∈ Q ) → ( 𝑦 <_Q 𝑥 ↔ ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) <_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) )
33	32	ancoms	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑦 <_Q 𝑥 ↔ ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) <_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) )
34	31 33	orbi12d	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( ( 𝑥 = 𝑦 ∨ 𝑦 <_Q 𝑥 ) ↔ ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) = ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ∨ ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) <_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) ) )
35	34	notbid	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( ¬ ( 𝑥 = 𝑦 ∨ 𝑦 <_Q 𝑥 ) ↔ ¬ ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) = ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ∨ ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) <_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) ) )
36	20 21 35	3bitr4d	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑥 <_Q 𝑦 ↔ ¬ ( 𝑥 = 𝑦 ∨ 𝑦 <_Q 𝑥 ) ) )
37	21	3adant3	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑥 <_Q 𝑦 ↔ ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) <_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) )
38		elpqn	⊢ ( 𝑧 ∈ Q → 𝑧 ∈ ( N × N ) )
39	38	3ad2ant3	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → 𝑧 ∈ ( N × N ) )
40		xp2nd	⊢ ( 𝑧 ∈ ( N × N ) → ( 2^nd ‘ 𝑧 ) ∈ N )
41		ltmpi	⊢ ( ( 2^nd ‘ 𝑧 ) ∈ N → ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) <_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ↔ ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) <_N ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) ) )
42	39 40 41	3syl	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) <_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ↔ ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) <_N ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) ) )
43	37 42	bitrd	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑥 <_Q 𝑦 ↔ ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) <_N ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) ) )
44		ordpinq	⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 <_Q 𝑧 ↔ ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑧 ) ) <_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) )
45	44	3adant1	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 <_Q 𝑧 ↔ ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑧 ) ) <_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) )
46	1	3ad2ant1	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → 𝑥 ∈ ( N × N ) )
47		ltmpi	⊢ ( ( 2^nd ‘ 𝑥 ) ∈ N → ( ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑧 ) ) <_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑦 ) ) ↔ ( ( 2^nd ‘ 𝑥 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑧 ) ) ) <_N ( ( 2^nd ‘ 𝑥 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) ) )
48	46 13 47	3syl	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑧 ) ) <_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑦 ) ) ↔ ( ( 2^nd ‘ 𝑥 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑧 ) ) ) <_N ( ( 2^nd ‘ 𝑥 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) ) )
49	45 48	bitrd	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 <_Q 𝑧 ↔ ( ( 2^nd ‘ 𝑥 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑧 ) ) ) <_N ( ( 2^nd ‘ 𝑥 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) ) )
50	43 49	anbi12d	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( ( 𝑥 <_Q 𝑦 ∧ 𝑦 <_Q 𝑧 ) ↔ ( ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) <_N ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( 2^nd ‘ 𝑥 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑧 ) ) ) <_N ( ( 2^nd ‘ 𝑥 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) ) ) )
51		fvex	⊢ ( 2^nd ‘ 𝑥 ) ∈ V
52		fvex	⊢ ( 1^st ‘ 𝑦 ) ∈ V
53		fvex	⊢ ( 2^nd ‘ 𝑧 ) ∈ V
54		mulcompi	⊢ ( 𝑟 ·_N 𝑠 ) = ( 𝑠 ·_N 𝑟 )
55		mulasspi	⊢ ( ( 𝑟 ·_N 𝑠 ) ·_N 𝑡 ) = ( 𝑟 ·_N ( 𝑠 ·_N 𝑡 ) )
56	51 52 53 54 55	caov13	⊢ ( ( 2^nd ‘ 𝑥 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑧 ) ) ) = ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) )
57		fvex	⊢ ( 1^st ‘ 𝑧 ) ∈ V
58		fvex	⊢ ( 2^nd ‘ 𝑦 ) ∈ V
59	51 57 58 54 55	caov13	⊢ ( ( 2^nd ‘ 𝑥 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) = ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑥 ) ) )
60	56 59	breq12i	⊢ ( ( ( 2^nd ‘ 𝑥 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑧 ) ) ) <_N ( ( 2^nd ‘ 𝑥 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) ↔ ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) <_N ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) )
61		fvex	⊢ ( 1^st ‘ 𝑥 ) ∈ V
62	53 61 58 54 55	caov13	⊢ ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) = ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑧 ) ) )
63		ltrelpi	⊢ <_N ⊆ ( N × N )
64	17 63	sotri	⊢ ( ( ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) <_N ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) <_N ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) ) → ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) <_N ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) )
65	62 64	eqbrtrrid	⊢ ( ( ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) <_N ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) <_N ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) ) → ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑧 ) ) ) <_N ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) )
66	60 65	sylan2b	⊢ ( ( ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) <_N ( ( 2^nd ‘ 𝑧 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) ∧ ( ( 2^nd ‘ 𝑥 ) ·_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑧 ) ) ) <_N ( ( 2^nd ‘ 𝑥 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑦 ) ) ) ) → ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑧 ) ) ) <_N ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) )
67	50 66	syl6bi	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( ( 𝑥 <_Q 𝑦 ∧ 𝑦 <_Q 𝑧 ) → ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑧 ) ) ) <_N ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) ) )
68		ordpinq	⊢ ( ( 𝑥 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑥 <_Q 𝑧 ↔ ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑧 ) ) <_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) )
69	68	3adant2	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑥 <_Q 𝑧 ↔ ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑧 ) ) <_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) )
70	5	3ad2ant2	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → 𝑦 ∈ ( N × N ) )
71		ltmpi	⊢ ( ( 2^nd ‘ 𝑦 ) ∈ N → ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑧 ) ) <_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑥 ) ) ↔ ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑧 ) ) ) <_N ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) ) )
72	70 7 71	3syl	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑧 ) ) <_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑥 ) ) ↔ ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑧 ) ) ) <_N ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) ) )
73	69 72	bitrd	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑥 <_Q 𝑧 ↔ ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑧 ) ) ) <_N ( ( 2^nd ‘ 𝑦 ) ·_N ( ( 1^st ‘ 𝑧 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) ) )
74	67 73	sylibrd	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( ( 𝑥 <_Q 𝑦 ∧ 𝑦 <_Q 𝑧 ) → 𝑥 <_Q 𝑧 ) )
75	36 74	isso2i	⊢ <_Q Or Q

Metamath Proof Explorer

Theorem ltsonq

Proof