Theorem ltsonq 6243

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

Assertion

Ref	Expression
ltsonq	⊢ <Q Or Q

Proof of Theorem ltsonq

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 f x y z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-nqqs 6193	. . . . . 6 ⊢ Q = ((N × N) / ~Q )
2		id 19	. . . . . . . 8 ⊢ ([⟨z, w⟩] ~Q = x → [⟨z, w⟩] ~Q = x)
3	2, 2	breq12d 3740	. . . . . . 7 ⊢ ([⟨z, w⟩] ~Q = x → ([⟨z, w⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ x <Q x))
4	3	notbid 576	. . . . . 6 ⊢ ([⟨z, w⟩] ~Q = x → (¬ [⟨z, w⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ ¬ x <Q x))
5		ltsopi 6166	. . . . . . . 8 ⊢ <N Or N
6		ltrelpi 6170	. . . . . . . 8 ⊢ <N ⊆ (N × N)
7	5, 6	soirri 4634	. . . . . . 7 ⊢ ¬ (w ·N z) <N (w ·N z)
8		ordpipqqs 6219	. . . . . . . . 9 ⊢ (((z ∈ N ∧ w ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → ([⟨z, w⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ (z ·N w) <N (w ·N z)))
9	8	anidms 377	. . . . . . . 8 ⊢ ((z ∈ N ∧ w ∈ N) → ([⟨z, w⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ (z ·N w) <N (w ·N z)))
10		mulcompig 6177	. . . . . . . . 9 ⊢ ((z ∈ N ∧ w ∈ N) → (z ·N w) = (w ·N z))
11	10	breq1d 3737	. . . . . . . 8 ⊢ ((z ∈ N ∧ w ∈ N) → ((z ·N w) <N (w ·N z) ↔ (w ·N z) <N (w ·N z)))
12	9, 11	bitrd 177	. . . . . . 7 ⊢ ((z ∈ N ∧ w ∈ N) → ([⟨z, w⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ (w ·N z) <N (w ·N z)))
13	7, 12	mtbiri 584	. . . . . 6 ⊢ ((z ∈ N ∧ w ∈ N) → ¬ [⟨z, w⟩] ~Q <Q [⟨z, w⟩] ~Q )
14	1, 4, 13	ecoptocl 6092	. . . . 5 ⊢ (x ∈ Q → ¬ x <Q x)
15	14	adantl 262	. . . 4 ⊢ (( ⊤ ∧ x ∈ Q) → ¬ x <Q x)
16		breq1 3730	. . . . . . . 8 ⊢ ([⟨𝑎, 𝑏⟩] ~Q = x → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ↔ x <Q [⟨𝑐, 𝑑⟩] ~Q ))
17	16	anbi1d 438	. . . . . . 7 ⊢ ([⟨𝑎, 𝑏⟩] ~Q = x → (([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ) ↔ (x <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )))
18		breq1 3730	. . . . . . 7 ⊢ ([⟨𝑎, 𝑏⟩] ~Q = x → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ↔ x <Q [⟨𝑒, f⟩] ~Q ))
19	17, 18	imbi12d 223	. . . . . 6 ⊢ ([⟨𝑎, 𝑏⟩] ~Q = x → ((([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ) → [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ) ↔ ((x <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ) → x <Q [⟨𝑒, f⟩] ~Q )))
20		breq2 3731	. . . . . . . 8 ⊢ ([⟨𝑐, 𝑑⟩] ~Q = y → (x <Q [⟨𝑐, 𝑑⟩] ~Q ↔ x <Q y))
21		breq1 3730	. . . . . . . 8 ⊢ ([⟨𝑐, 𝑑⟩] ~Q = y → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ↔ y <Q [⟨𝑒, f⟩] ~Q ))
22	20, 21	anbi12d 442	. . . . . . 7 ⊢ ([⟨𝑐, 𝑑⟩] ~Q = y → ((x <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ) ↔ (x <Q y ∧ y <Q [⟨𝑒, f⟩] ~Q )))
23	22	imbi1d 220	. . . . . 6 ⊢ ([⟨𝑐, 𝑑⟩] ~Q = y → (((x <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ) → x <Q [⟨𝑒, f⟩] ~Q ) ↔ ((x <Q y ∧ y <Q [⟨𝑒, f⟩] ~Q ) → x <Q [⟨𝑒, f⟩] ~Q )))
24		breq2 3731	. . . . . . . 8 ⊢ ([⟨𝑒, f⟩] ~Q = z → (y <Q [⟨𝑒, f⟩] ~Q ↔ y <Q z))
25	24	anbi2d 437	. . . . . . 7 ⊢ ([⟨𝑒, f⟩] ~Q = z → ((x <Q y ∧ y <Q [⟨𝑒, f⟩] ~Q ) ↔ (x <Q y ∧ y <Q z)))
26		breq2 3731	. . . . . . 7 ⊢ ([⟨𝑒, f⟩] ~Q = z → (x <Q [⟨𝑒, f⟩] ~Q ↔ x <Q z))
27	25, 26	imbi12d 223	. . . . . 6 ⊢ ([⟨𝑒, f⟩] ~Q = z → (((x <Q y ∧ y <Q [⟨𝑒, f⟩] ~Q ) → x <Q [⟨𝑒, f⟩] ~Q ) ↔ ((x <Q y ∧ y <Q z) → x <Q z)))
28		ordpipqqs 6219	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ↔ (𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐)))
29	28	3adant3 906	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ↔ (𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐)))
30		simp1l 910	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → 𝑎 ∈ N)
31		simp2r 913	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → 𝑑 ∈ N)
32		mulclpi 6174	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ N ∧ 𝑑 ∈ N) → (𝑎 ·N 𝑑) ∈ N)
33	30, 31, 32	syl2anc 391	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → (𝑎 ·N 𝑑) ∈ N)
34		simp1r 911	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → 𝑏 ∈ N)
35		simp2l 912	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → 𝑐 ∈ N)
36		mulclpi 6174	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ N ∧ 𝑐 ∈ N) → (𝑏 ·N 𝑐) ∈ N)
37	34, 35, 36	syl2anc 391	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → (𝑏 ·N 𝑐) ∈ N)
38		simp3r 915	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → f ∈ N)
39		mulclpi 6174	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ N ∧ f ∈ N) → (𝑐 ·N f) ∈ N)
40	35, 38, 39	syl2anc 391	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → (𝑐 ·N f) ∈ N)
41		ltmpig 6185	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ·N 𝑑) ∈ N ∧ (𝑏 ·N 𝑐) ∈ N ∧ (𝑐 ·N f) ∈ N) → ((𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐) ↔ ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N f) ·N (𝑏 ·N 𝑐))))
42	33, 37, 40, 41	syl3anc 1116	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → ((𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐) ↔ ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N f) ·N (𝑏 ·N 𝑐))))
43	29, 42	bitrd 177	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ↔ ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N f) ·N (𝑏 ·N 𝑐))))
44	43	biimpa 280	. . . . . . . . . . . . 13 ⊢ ((((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) ∧ [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ) → ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N f) ·N (𝑏 ·N 𝑐)))
45	44	adantrr 448	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )) → ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N f) ·N (𝑏 ·N 𝑐)))
46		mulcompig 6177	. . . . . . . . . . . . . 14 ⊢ (((𝑐 ·N f) ∈ N ∧ (𝑏 ·N 𝑐) ∈ N) → ((𝑐 ·N f) ·N (𝑏 ·N 𝑐)) = ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)))
47	40, 37, 46	syl2anc 391	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → ((𝑐 ·N f) ·N (𝑏 ·N 𝑐)) = ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)))
48	47	adantr 261	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )) → ((𝑐 ·N f) ·N (𝑏 ·N 𝑐)) = ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)))
49	45, 48	breqtrd 3751	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )) → ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)))
50		ordpipqqs 6219	. . . . . . . . . . . . . . 15 ⊢ (((𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ↔ (𝑐 ·N f) <N (𝑑 ·N 𝑒)))
51	50	3adant1 904	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ↔ (𝑐 ·N f) <N (𝑑 ·N 𝑒)))
52		simp3l 914	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → 𝑒 ∈ N)
53		mulclpi 6174	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 ∈ N ∧ 𝑒 ∈ N) → (𝑑 ·N 𝑒) ∈ N)
54	31, 52, 53	syl2anc 391	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → (𝑑 ·N 𝑒) ∈ N)
55		ltmpig 6185	. . . . . . . . . . . . . . 15 ⊢ (((𝑐 ·N f) ∈ N ∧ (𝑑 ·N 𝑒) ∈ N ∧ (𝑏 ·N 𝑐) ∈ N) → ((𝑐 ·N f) <N (𝑑 ·N 𝑒) ↔ ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
56	40, 54, 37, 55	syl3anc 1116	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → ((𝑐 ·N f) <N (𝑑 ·N 𝑒) ↔ ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
57	51, 56	bitrd 177	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ↔ ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
58	57	biimpa 280	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ) → ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
59	58	adantrl 447	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )) → ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
60	5, 6	sotri 4635	. . . . . . . . . . 11 ⊢ ((((𝑐 ·N f) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)) ∧ ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))) → ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
61	49, 59, 60	syl2anc 391	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )) → ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
62		mulcompig 6177	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ N ∧ y ∈ N) → (x ·N y) = (y ·N x))
63	62	adantl 262	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) ∧ (x ∈ N ∧ y ∈ N)) → (x ·N y) = (y ·N x))
64		mulasspig 6178	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ N ∧ y ∈ N ∧ z ∈ N) → ((x ·N y) ·N z) = (x ·N (y ·N z)))
65	64	adantl 262	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) ∧ (x ∈ N ∧ y ∈ N ∧ z ∈ N)) → ((x ·N y) ·N z) = (x ·N (y ·N z)))
66		mulclpi 6174	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ N ∧ y ∈ N) → (x ·N y) ∈ N)
67	66	adantl 262	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) ∧ (x ∈ N ∧ y ∈ N)) → (x ·N y) ∈ N)
68	35, 31, 30, 63, 65, 38, 67	caov411d 5597	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → ((𝑐 ·N 𝑑) ·N (𝑎 ·N f)) = ((𝑎 ·N 𝑑) ·N (𝑐 ·N f)))
69	63, 33, 40	caovcomd 5568	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → ((𝑎 ·N 𝑑) ·N (𝑐 ·N f)) = ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)))
70	68, 69	eqtrd 2045	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → ((𝑐 ·N 𝑑) ·N (𝑎 ·N f)) = ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)))
71	35, 31, 34, 63, 65, 52, 67	caov4d 5596	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)) = ((𝑐 ·N 𝑏) ·N (𝑑 ·N 𝑒)))
72	63, 35, 34	caovcomd 5568	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → (𝑐 ·N 𝑏) = (𝑏 ·N 𝑐))
73	72	oveq1d 5439	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → ((𝑐 ·N 𝑏) ·N (𝑑 ·N 𝑒)) = ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
74	71, 73	eqtrd 2045	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)) = ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
75	70, 74	breq12d 3740	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → (((𝑐 ·N 𝑑) ·N (𝑎 ·N f)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)) ↔ ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
76	75	adantr 261	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )) → (((𝑐 ·N 𝑑) ·N (𝑎 ·N f)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)) ↔ ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
77	61, 76	mpbird 156	. . . . . . . . 9 ⊢ ((((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )) → ((𝑐 ·N 𝑑) ·N (𝑎 ·N f)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)))
78		mulclpi 6174	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ N ∧ f ∈ N) → (𝑎 ·N f) ∈ N)
79	30, 38, 78	syl2anc 391	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → (𝑎 ·N f) ∈ N)
80		mulclpi 6174	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ N ∧ 𝑒 ∈ N) → (𝑏 ·N 𝑒) ∈ N)
81	34, 52, 80	syl2anc 391	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → (𝑏 ·N 𝑒) ∈ N)
82		mulclpi 6174	. . . . . . . . . . . 12 ⊢ ((𝑐 ∈ N ∧ 𝑑 ∈ N) → (𝑐 ·N 𝑑) ∈ N)
83	35, 31, 82	syl2anc 391	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → (𝑐 ·N 𝑑) ∈ N)
84		ltmpig 6185	. . . . . . . . . . 11 ⊢ (((𝑎 ·N f) ∈ N ∧ (𝑏 ·N 𝑒) ∈ N ∧ (𝑐 ·N 𝑑) ∈ N) → ((𝑎 ·N f) <N (𝑏 ·N 𝑒) ↔ ((𝑐 ·N 𝑑) ·N (𝑎 ·N f)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒))))
85	79, 81, 83, 84	syl3anc 1116	. . . . . . . . . 10 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → ((𝑎 ·N f) <N (𝑏 ·N 𝑒) ↔ ((𝑐 ·N 𝑑) ·N (𝑎 ·N f)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒))))
86	85	adantr 261	. . . . . . . . 9 ⊢ ((((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )) → ((𝑎 ·N f) <N (𝑏 ·N 𝑒) ↔ ((𝑐 ·N 𝑑) ·N (𝑎 ·N f)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒))))
87	77, 86	mpbird 156	. . . . . . . 8 ⊢ ((((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )) → (𝑎 ·N f) <N (𝑏 ·N 𝑒))
88		ordpipqqs 6219	. . . . . . . . . 10 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ↔ (𝑎 ·N f) <N (𝑏 ·N 𝑒)))
89	88	3adant2 905	. . . . . . . . 9 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ↔ (𝑎 ·N f) <N (𝑏 ·N 𝑒)))
90	89	adantr 261	. . . . . . . 8 ⊢ ((((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ↔ (𝑎 ·N f) <N (𝑏 ·N 𝑒)))
91	87, 90	mpbird 156	. . . . . . 7 ⊢ ((((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )) → [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )
92	91	ex 108	. . . . . 6 ⊢ (((𝑎 ∈ N ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ N ∧ 𝑑 ∈ N) ∧ (𝑒 ∈ N ∧ f ∈ N)) → (([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ) → [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ))
93	1, 19, 23, 27, 92	3ecoptocl 6094	. . . . 5 ⊢ ((x ∈ Q ∧ y ∈ Q ∧ z ∈ Q) → ((x <Q y ∧ y <Q z) → x <Q z))
94	93	adantl 262	. . . 4 ⊢ (( ⊤ ∧ (x ∈ Q ∧ y ∈ Q ∧ z ∈ Q)) → ((x <Q y ∧ y <Q z) → x <Q z))
95	15, 94	ispod 4004	. . 3 ⊢ ( ⊤ → <Q Po Q)
96		nqtri3or 6241	. . . 4 ⊢ ((x ∈ Q ∧ y ∈ Q) → (x <Q y ∨ x = y ∨ y <Q x))
97	96	adantl 262	. . 3 ⊢ (( ⊤ ∧ (x ∈ Q ∧ y ∈ Q)) → (x <Q y ∨ x = y ∨ y <Q x))
98	95, 97	issod 4019	. 2 ⊢ ( ⊤ → <Q Or Q)
99	98	trud 1232	1 ⊢ <Q Or Q

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ w3o 866   ∧ w3a 867   = wceq 1223   ⊤ wtru 1224   ∈ wcel 1366  ⟨cop 3342   class class class wbr 3727   Or wor 3995  (class class class)co 5424  [cec 6003  Ncnpi 6118   ·_N cmi 6120   <_N clti 6121   ~_Q ceq 6125  Qcnq 6126   <_Q cltq 6131

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 529  ax-in2 530  ax-io 614  ax-5 1309  ax-7 1310  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-10 1369  ax-11 1370  ax-i12 1371  ax-bnd 1372  ax-4 1373  ax-13 1377  ax-14 1378  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-i5r 1401  ax-ext 1995  ax-coll 3835  ax-sep 3838  ax-nul 3846  ax-pow 3890  ax-pr 3907  ax-un 4108  ax-setind 4192  ax-iinf 4226

This theorem depends on definitions:  df-bi 110  df-dc 727  df-3or 868  df-3an 869  df-tru 1226  df-fal 1229  df-nf 1323  df-sb 1619  df-eu 1876  df-mo 1877  df-clab 2000  df-cleq 2006  df-clel 2009  df-nfc 2140  df-ne 2179  df-ral 2280  df-rex 2281  df-reu 2282  df-rab 2284  df-v 2528  df-sbc 2733  df-csb 2821  df-dif 2888  df-un 2890  df-in 2892  df-ss 2899  df-nul 3193  df-pw 3325  df-sn 3345  df-pr 3346  df-op 3348  df-uni 3544  df-int 3579  df-iun 3622  df-br 3728  df-opab 3782  df-mpt 3783  df-tr 3818  df-eprel 3989  df-id 3993  df-po 3996  df-iso 3997  df-iord 4041  df-on 4043  df-suc 4046  df-iom 4229  df-xp 4266  df-rel 4267  df-cnv 4268  df-co 4269  df-dm 4270  df-rn 4271  df-res 4272  df-ima 4273  df-iota 4782  df-fun 4819  df-fn 4820  df-f 4821  df-f1 4822  df-fo 4823  df-f1o 4824  df-fv 4825  df-ov 5427  df-oprab 5428  df-mpt2 5429  df-1st 5678  df-2nd 5679  df-recs 5830  df-irdg 5866  df-oadd 5908  df-omul 5909  df-er 6005  df-ec 6007  df-qs 6011  df-ni 6150  df-mi 6152  df-lti 6153  df-enq 6192  df-nqqs 6193  df-ltnqqs 6198

This theorem is referenced by:  nqtric  6244  lt2addnq  6249  ltbtwnnqq  6258  prarloclemarch2  6262  genplt2i  6350  genpdisj  6364  addlocprlemgt  6375  nqprdisj  6385  nqprloc  6386  prmuloclemcalc  6395  distrlem4prl  6409  distrlem4pru  6410  ltsopr  6419  ltexprlemopl  6424  ltexprlemopu  6426  ltexprlemdisj  6429  ltexprlemru  6435  recexprlemlol  6447  recexprlemupu  6449  recexprlemdisj  6451  recexprlemss1l  6456  recexprlemss1u  6457