Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltsonq GIF version

Theorem ltsonq 6382
 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.
StepHypRef Expression
1 df-nqqs 6332 . . . . . 6 Q = ((N × N) / ~Q )
2 id 19 . . . . . . . 8 ([⟨z, w⟩] ~Q = x → [⟨z, w⟩] ~Q = x)
32, 2breq12d 3768 . . . . . . 7 ([⟨z, w⟩] ~Q = x → ([⟨z, w⟩] ~Q <Q [⟨z, w⟩] ~Qx <Q x))
43notbid 591 . . . . . 6 ([⟨z, w⟩] ~Q = x → (¬ [⟨z, w⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ ¬ x <Q x))
5 ltsopi 6304 . . . . . . . 8 <N Or N
6 ltrelpi 6308 . . . . . . . 8 <N ⊆ (N × N)
75, 6soirri 4662 . . . . . . 7 ¬ (w ·N z) <N (w ·N z)
8 ordpipqqs 6358 . . . . . . . . 9 (((z N w N) (z N w N)) → ([⟨z, w⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ (z ·N w) <N (w ·N z)))
98anidms 377 . . . . . . . 8 ((z N w N) → ([⟨z, w⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ (z ·N w) <N (w ·N z)))
10 mulcompig 6315 . . . . . . . . 9 ((z N w N) → (z ·N w) = (w ·N z))
1110breq1d 3765 . . . . . . . 8 ((z N w N) → ((z ·N w) <N (w ·N z) ↔ (w ·N z) <N (w ·N z)))
129, 11bitrd 177 . . . . . . 7 ((z N w N) → ([⟨z, w⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ (w ·N z) <N (w ·N z)))
137, 12mtbiri 599 . . . . . 6 ((z N w N) → ¬ [⟨z, w⟩] ~Q <Q [⟨z, w⟩] ~Q )
141, 4, 13ecoptocl 6129 . . . . 5 (x Q → ¬ x <Q x)
1514adantl 262 . . . 4 (( ⊤ x Q) → ¬ x <Q x)
16 breq1 3758 . . . . . . . 8 ([⟨𝑎, 𝑏⟩] ~Q = x → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Qx <Q [⟨𝑐, 𝑑⟩] ~Q ))
1716anbi1d 438 . . . . . . 7 ([⟨𝑎, 𝑏⟩] ~Q = x → (([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ) ↔ (x <Q [⟨𝑐, 𝑑⟩] ~Q [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )))
18 breq1 3758 . . . . . . 7 ([⟨𝑎, 𝑏⟩] ~Q = x → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, f⟩] ~Qx <Q [⟨𝑒, f⟩] ~Q ))
1917, 18imbi12d 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 3759 . . . . . . . 8 ([⟨𝑐, 𝑑⟩] ~Q = y → (x <Q [⟨𝑐, 𝑑⟩] ~Qx <Q y))
21 breq1 3758 . . . . . . . 8 ([⟨𝑐, 𝑑⟩] ~Q = y → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Qy <Q [⟨𝑒, f⟩] ~Q ))
2220, 21anbi12d 442 . . . . . . 7 ([⟨𝑐, 𝑑⟩] ~Q = y → ((x <Q [⟨𝑐, 𝑑⟩] ~Q [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ) ↔ (x <Q y y <Q [⟨𝑒, f⟩] ~Q )))
2322imbi1d 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 3759 . . . . . . . 8 ([⟨𝑒, f⟩] ~Q = z → (y <Q [⟨𝑒, f⟩] ~Qy <Q z))
2524anbi2d 437 . . . . . . 7 ([⟨𝑒, f⟩] ~Q = z → ((x <Q y y <Q [⟨𝑒, f⟩] ~Q ) ↔ (x <Q y y <Q z)))
26 breq2 3759 . . . . . . 7 ([⟨𝑒, f⟩] ~Q = z → (x <Q [⟨𝑒, f⟩] ~Qx <Q z))
2725, 26imbi12d 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 6358 . . . . . . . . . . . . . . . 16 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ↔ (𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐)))
29283adant3 923 . . . . . . . . . . . . . . 15 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ↔ (𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐)))
30 simp1l 927 . . . . . . . . . . . . . . . . 17 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → 𝑎 N)
31 simp2r 930 . . . . . . . . . . . . . . . . 17 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → 𝑑 N)
32 mulclpi 6312 . . . . . . . . . . . . . . . . 17 ((𝑎 N 𝑑 N) → (𝑎 ·N 𝑑) N)
3330, 31, 32syl2anc 391 . . . . . . . . . . . . . . . 16 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → (𝑎 ·N 𝑑) N)
34 simp1r 928 . . . . . . . . . . . . . . . . 17 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → 𝑏 N)
35 simp2l 929 . . . . . . . . . . . . . . . . 17 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → 𝑐 N)
36 mulclpi 6312 . . . . . . . . . . . . . . . . 17 ((𝑏 N 𝑐 N) → (𝑏 ·N 𝑐) N)
3734, 35, 36syl2anc 391 . . . . . . . . . . . . . . . 16 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → (𝑏 ·N 𝑐) N)
38 simp3r 932 . . . . . . . . . . . . . . . . 17 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → f N)
39 mulclpi 6312 . . . . . . . . . . . . . . . . 17 ((𝑐 N f N) → (𝑐 ·N f) N)
4035, 38, 39syl2anc 391 . . . . . . . . . . . . . . . 16 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → (𝑐 ·N f) N)
41 ltmpig 6323 . . . . . . . . . . . . . . . 16 (((𝑎 ·N 𝑑) N (𝑏 ·N 𝑐) N (𝑐 ·N f) N) → ((𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐) ↔ ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N f) ·N (𝑏 ·N 𝑐))))
4233, 37, 40, 41syl3anc 1134 . . . . . . . . . . . . . . 15 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → ((𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐) ↔ ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N f) ·N (𝑏 ·N 𝑐))))
4329, 42bitrd 177 . . . . . . . . . . . . . 14 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ↔ ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N f) ·N (𝑏 ·N 𝑐))))
4443biimpa 280 . . . . . . . . . . . . 13 ((((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ) → ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N f) ·N (𝑏 ·N 𝑐)))
4544adantrr 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 6315 . . . . . . . . . . . . . 14 (((𝑐 ·N f) N (𝑏 ·N 𝑐) N) → ((𝑐 ·N f) ·N (𝑏 ·N 𝑐)) = ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)))
4740, 37, 46syl2anc 391 . . . . . . . . . . . . 13 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → ((𝑐 ·N f) ·N (𝑏 ·N 𝑐)) = ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)))
4847adantr 261 . . . . . . . . . . . 12 ((((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )) → ((𝑐 ·N f) ·N (𝑏 ·N 𝑐)) = ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)))
4945, 48breqtrd 3779 . . . . . . . . . . 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 6358 . . . . . . . . . . . . . . 15 (((𝑐 N 𝑑 N) (𝑒 N f N)) → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ↔ (𝑐 ·N f) <N (𝑑 ·N 𝑒)))
51503adant1 921 . . . . . . . . . . . . . 14 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ↔ (𝑐 ·N f) <N (𝑑 ·N 𝑒)))
52 simp3l 931 . . . . . . . . . . . . . . . 16 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → 𝑒 N)
53 mulclpi 6312 . . . . . . . . . . . . . . . 16 ((𝑑 N 𝑒 N) → (𝑑 ·N 𝑒) N)
5431, 52, 53syl2anc 391 . . . . . . . . . . . . . . 15 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → (𝑑 ·N 𝑒) N)
55 ltmpig 6323 . . . . . . . . . . . . . . 15 (((𝑐 ·N f) N (𝑑 ·N 𝑒) N (𝑏 ·N 𝑐) N) → ((𝑐 ·N f) <N (𝑑 ·N 𝑒) ↔ ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
5640, 54, 37, 55syl3anc 1134 . . . . . . . . . . . . . 14 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → ((𝑐 ·N f) <N (𝑑 ·N 𝑒) ↔ ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
5751, 56bitrd 177 . . . . . . . . . . . . 13 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ↔ ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
5857biimpa 280 . . . . . . . . . . . 12 ((((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ) → ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
5958adantrl 447 . . . . . . . . . . 11 ((((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )) → ((𝑏 ·N 𝑐) ·N (𝑐 ·N f)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
605, 6sotri 4663 . . . . . . . . . . 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 𝑒)))
6149, 59, 60syl2anc 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 6315 . . . . . . . . . . . . . . 15 ((x N y N) → (x ·N y) = (y ·N x))
6362adantl 262 . . . . . . . . . . . . . 14 ((((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) (x N y N)) → (x ·N y) = (y ·N x))
64 mulasspig 6316 . . . . . . . . . . . . . . 15 ((x N y N z N) → ((x ·N y) ·N z) = (x ·N (y ·N z)))
6564adantl 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 6312 . . . . . . . . . . . . . . 15 ((x N y N) → (x ·N y) N)
6766adantl 262 . . . . . . . . . . . . . 14 ((((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) (x N y N)) → (x ·N y) N)
6835, 31, 30, 63, 65, 38, 67caov411d 5628 . . . . . . . . . . . . 13 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → ((𝑐 ·N 𝑑) ·N (𝑎 ·N f)) = ((𝑎 ·N 𝑑) ·N (𝑐 ·N f)))
6963, 33, 40caovcomd 5599 . . . . . . . . . . . . 13 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → ((𝑎 ·N 𝑑) ·N (𝑐 ·N f)) = ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)))
7068, 69eqtrd 2069 . . . . . . . . . . . 12 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → ((𝑐 ·N 𝑑) ·N (𝑎 ·N f)) = ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)))
7135, 31, 34, 63, 65, 52, 67caov4d 5627 . . . . . . . . . . . . 13 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)) = ((𝑐 ·N 𝑏) ·N (𝑑 ·N 𝑒)))
7263, 35, 34caovcomd 5599 . . . . . . . . . . . . . 14 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → (𝑐 ·N 𝑏) = (𝑏 ·N 𝑐))
7372oveq1d 5470 . . . . . . . . . . . . 13 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → ((𝑐 ·N 𝑏) ·N (𝑑 ·N 𝑒)) = ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
7471, 73eqtrd 2069 . . . . . . . . . . . 12 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)) = ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
7570, 74breq12d 3768 . . . . . . . . . . 11 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → (((𝑐 ·N 𝑑) ·N (𝑎 ·N f)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)) ↔ ((𝑐 ·N f) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
7675adantr 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 𝑒))))
7761, 76mpbird 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 6312 . . . . . . . . . . . 12 ((𝑎 N f N) → (𝑎 ·N f) N)
7930, 38, 78syl2anc 391 . . . . . . . . . . 11 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → (𝑎 ·N f) N)
80 mulclpi 6312 . . . . . . . . . . . 12 ((𝑏 N 𝑒 N) → (𝑏 ·N 𝑒) N)
8134, 52, 80syl2anc 391 . . . . . . . . . . 11 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → (𝑏 ·N 𝑒) N)
82 mulclpi 6312 . . . . . . . . . . . 12 ((𝑐 N 𝑑 N) → (𝑐 ·N 𝑑) N)
8335, 31, 82syl2anc 391 . . . . . . . . . . 11 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → (𝑐 ·N 𝑑) N)
84 ltmpig 6323 . . . . . . . . . . 11 (((𝑎 ·N f) N (𝑏 ·N 𝑒) N (𝑐 ·N 𝑑) N) → ((𝑎 ·N f) <N (𝑏 ·N 𝑒) ↔ ((𝑐 ·N 𝑑) ·N (𝑎 ·N f)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒))))
8579, 81, 83, 84syl3anc 1134 . . . . . . . . . 10 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → ((𝑎 ·N f) <N (𝑏 ·N 𝑒) ↔ ((𝑐 ·N 𝑑) ·N (𝑎 ·N f)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒))))
8685adantr 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 𝑒))))
8777, 86mpbird 156 . . . . . . . 8 ((((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )) → (𝑎 ·N f) <N (𝑏 ·N 𝑒))
88 ordpipqqs 6358 . . . . . . . . . 10 (((𝑎 N 𝑏 N) (𝑒 N f N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ↔ (𝑎 ·N f) <N (𝑏 ·N 𝑒)))
89883adant2 922 . . . . . . . . 9 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ↔ (𝑎 ·N f) <N (𝑏 ·N 𝑒)))
9089adantr 261 . . . . . . . 8 ((((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ↔ (𝑎 ·N f) <N (𝑏 ·N 𝑒)))
9187, 90mpbird 156 . . . . . . 7 ((((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )) → [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, f⟩] ~Q )
9291ex 108 . . . . . 6 (((𝑎 N 𝑏 N) (𝑐 N 𝑑 N) (𝑒 N f N)) → (([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ) → [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, f⟩] ~Q ))
931, 19, 23, 27, 923ecoptocl 6131 . . . . 5 ((x Q y Q z Q) → ((x <Q y y <Q z) → x <Q z))
9493adantl 262 . . . 4 (( ⊤ (x Q y Q z Q)) → ((x <Q y y <Q z) → x <Q z))
9515, 94ispod 4032 . . 3 ( ⊤ → <Q Po Q)
96 nqtri3or 6380 . . . 4 ((x Q y Q) → (x <Q y x = y y <Q x))
9796adantl 262 . . 3 (( ⊤ (x Q y Q)) → (x <Q y x = y y <Q x))
9895, 97issod 4047 . 2 ( ⊤ → <Q Or Q)
9998trud 1251 1 <Q Or Q
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ w3o 883   ∧ w3a 884   = wceq 1242   ⊤ wtru 1243   ∈ wcel 1390  ⟨cop 3370   class class class wbr 3755   Or wor 4023  (class class class)co 5455  [cec 6040  Ncnpi 6256   ·N cmi 6258
 Copyright terms: Public domain W3C validator