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

Theorem ltsonq 6496
 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 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nqqs 6446 . . . . . 6 Q = ((N × N) / ~Q )
2 id 19 . . . . . . . 8 ([⟨𝑧, 𝑤⟩] ~Q = 𝑥 → [⟨𝑧, 𝑤⟩] ~Q = 𝑥)
32, 2breq12d 3777 . . . . . . 7 ([⟨𝑧, 𝑤⟩] ~Q = 𝑥 → ([⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q𝑥 <Q 𝑥))
43notbid 592 . . . . . 6 ([⟨𝑧, 𝑤⟩] ~Q = 𝑥 → (¬ [⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ ¬ 𝑥 <Q 𝑥))
5 ltsopi 6418 . . . . . . . 8 <N Or N
6 ltrelpi 6422 . . . . . . . 8 <N ⊆ (N × N)
75, 6soirri 4719 . . . . . . 7 ¬ (𝑤 ·N 𝑧) <N (𝑤 ·N 𝑧)
8 ordpipqqs 6472 . . . . . . . . 9 (((𝑧N𝑤N) ∧ (𝑧N𝑤N)) → ([⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ (𝑧 ·N 𝑤) <N (𝑤 ·N 𝑧)))
98anidms 377 . . . . . . . 8 ((𝑧N𝑤N) → ([⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ (𝑧 ·N 𝑤) <N (𝑤 ·N 𝑧)))
10 mulcompig 6429 . . . . . . . . 9 ((𝑧N𝑤N) → (𝑧 ·N 𝑤) = (𝑤 ·N 𝑧))
1110breq1d 3774 . . . . . . . 8 ((𝑧N𝑤N) → ((𝑧 ·N 𝑤) <N (𝑤 ·N 𝑧) ↔ (𝑤 ·N 𝑧) <N (𝑤 ·N 𝑧)))
129, 11bitrd 177 . . . . . . 7 ((𝑧N𝑤N) → ([⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ (𝑤 ·N 𝑧) <N (𝑤 ·N 𝑧)))
137, 12mtbiri 600 . . . . . 6 ((𝑧N𝑤N) → ¬ [⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q )
141, 4, 13ecoptocl 6193 . . . . 5 (𝑥Q → ¬ 𝑥 <Q 𝑥)
1514adantl 262 . . . 4 ((⊤ ∧ 𝑥Q) → ¬ 𝑥 <Q 𝑥)
16 breq1 3767 . . . . . . . 8 ([⟨𝑎, 𝑏⟩] ~Q = 𝑥 → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q ))
1716anbi1d 438 . . . . . . 7 ([⟨𝑎, 𝑏⟩] ~Q = 𝑥 → (([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ (𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )))
18 breq1 3767 . . . . . . 7 ([⟨𝑎, 𝑏⟩] ~Q = 𝑥 → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q ))
1917, 18imbi12d 223 . . . . . 6 ([⟨𝑎, 𝑏⟩] ~Q = 𝑥 → ((([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) → [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ ((𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) → 𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q )))
20 breq2 3768 . . . . . . . 8 ([⟨𝑐, 𝑑⟩] ~Q = 𝑦 → (𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q𝑥 <Q 𝑦))
21 breq1 3767 . . . . . . . 8 ([⟨𝑐, 𝑑⟩] ~Q = 𝑦 → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q ))
2220, 21anbi12d 442 . . . . . . 7 ([⟨𝑐, 𝑑⟩] ~Q = 𝑦 → ((𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ (𝑥 <Q 𝑦𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q )))
2322imbi1d 220 . . . . . 6 ([⟨𝑐, 𝑑⟩] ~Q = 𝑦 → (((𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) → 𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ ((𝑥 <Q 𝑦𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q ) → 𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q )))
24 breq2 3768 . . . . . . . 8 ([⟨𝑒, 𝑓⟩] ~Q = 𝑧 → (𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q𝑦 <Q 𝑧))
2524anbi2d 437 . . . . . . 7 ([⟨𝑒, 𝑓⟩] ~Q = 𝑧 → ((𝑥 <Q 𝑦𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ (𝑥 <Q 𝑦𝑦 <Q 𝑧)))
26 breq2 3768 . . . . . . 7 ([⟨𝑒, 𝑓⟩] ~Q = 𝑧 → (𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q𝑥 <Q 𝑧))
2725, 26imbi12d 223 . . . . . 6 ([⟨𝑒, 𝑓⟩] ~Q = 𝑧 → (((𝑥 <Q 𝑦𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q ) → 𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ ((𝑥 <Q 𝑦𝑦 <Q 𝑧) → 𝑥 <Q 𝑧)))
28 ordpipqqs 6472 . . . . . . . . . . . . . . . 16 (((𝑎N𝑏N) ∧ (𝑐N𝑑N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ↔ (𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐)))
29283adant3 924 . . . . . . . . . . . . . . 15 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ↔ (𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐)))
30 simp1l 928 . . . . . . . . . . . . . . . . 17 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑎N)
31 simp2r 931 . . . . . . . . . . . . . . . . 17 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑑N)
32 mulclpi 6426 . . . . . . . . . . . . . . . . 17 ((𝑎N𝑑N) → (𝑎 ·N 𝑑) ∈ N)
3330, 31, 32syl2anc 391 . . . . . . . . . . . . . . . 16 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑎 ·N 𝑑) ∈ N)
34 simp1r 929 . . . . . . . . . . . . . . . . 17 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑏N)
35 simp2l 930 . . . . . . . . . . . . . . . . 17 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑐N)
36 mulclpi 6426 . . . . . . . . . . . . . . . . 17 ((𝑏N𝑐N) → (𝑏 ·N 𝑐) ∈ N)
3734, 35, 36syl2anc 391 . . . . . . . . . . . . . . . 16 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑏 ·N 𝑐) ∈ N)
38 simp3r 933 . . . . . . . . . . . . . . . . 17 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑓N)
39 mulclpi 6426 . . . . . . . . . . . . . . . . 17 ((𝑐N𝑓N) → (𝑐 ·N 𝑓) ∈ N)
4035, 38, 39syl2anc 391 . . . . . . . . . . . . . . . 16 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑐 ·N 𝑓) ∈ N)
41 ltmpig 6437 . . . . . . . . . . . . . . . 16 (((𝑎 ·N 𝑑) ∈ N ∧ (𝑏 ·N 𝑐) ∈ N ∧ (𝑐 ·N 𝑓) ∈ N) → ((𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐) ↔ ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐))))
4233, 37, 40, 41syl3anc 1135 . . . . . . . . . . . . . . 15 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐) ↔ ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐))))
4329, 42bitrd 177 . . . . . . . . . . . . . 14 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ↔ ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐))))
4443biimpa 280 . . . . . . . . . . . . 13 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ) → ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐)))
4544adantrr 448 . . . . . . . . . . . 12 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐)))
46 mulcompig 6429 . . . . . . . . . . . . . 14 (((𝑐 ·N 𝑓) ∈ N ∧ (𝑏 ·N 𝑐) ∈ N) → ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐)) = ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)))
4740, 37, 46syl2anc 391 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐)) = ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)))
4847adantr 261 . . . . . . . . . . . 12 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐)) = ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)))
4945, 48breqtrd 3788 . . . . . . . . . . 11 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)))
50 ordpipqqs 6472 . . . . . . . . . . . . . . 15 (((𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ (𝑐 ·N 𝑓) <N (𝑑 ·N 𝑒)))
51503adant1 922 . . . . . . . . . . . . . 14 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ (𝑐 ·N 𝑓) <N (𝑑 ·N 𝑒)))
52 simp3l 932 . . . . . . . . . . . . . . . 16 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑒N)
53 mulclpi 6426 . . . . . . . . . . . . . . . 16 ((𝑑N𝑒N) → (𝑑 ·N 𝑒) ∈ N)
5431, 52, 53syl2anc 391 . . . . . . . . . . . . . . 15 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑑 ·N 𝑒) ∈ N)
55 ltmpig 6437 . . . . . . . . . . . . . . 15 (((𝑐 ·N 𝑓) ∈ N ∧ (𝑑 ·N 𝑒) ∈ N ∧ (𝑏 ·N 𝑐) ∈ N) → ((𝑐 ·N 𝑓) <N (𝑑 ·N 𝑒) ↔ ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
5640, 54, 37, 55syl3anc 1135 . . . . . . . . . . . . . 14 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑓) <N (𝑑 ·N 𝑒) ↔ ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
5751, 56bitrd 177 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
5857biimpa 280 . . . . . . . . . . . 12 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) → ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
5958adantrl 447 . . . . . . . . . . 11 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
605, 6sotri 4720 . . . . . . . . . . 11 ((((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)) ∧ ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))) → ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
6149, 59, 60syl2anc 391 . . . . . . . . . 10 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
62 mulcompig 6429 . . . . . . . . . . . . . . 15 ((𝑥N𝑦N) → (𝑥 ·N 𝑦) = (𝑦 ·N 𝑥))
6362adantl 262 . . . . . . . . . . . . . 14 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ (𝑥N𝑦N)) → (𝑥 ·N 𝑦) = (𝑦 ·N 𝑥))
64 mulasspig 6430 . . . . . . . . . . . . . . 15 ((𝑥N𝑦N𝑧N) → ((𝑥 ·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦 ·N 𝑧)))
6564adantl 262 . . . . . . . . . . . . . 14 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ (𝑥N𝑦N𝑧N)) → ((𝑥 ·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦 ·N 𝑧)))
66 mulclpi 6426 . . . . . . . . . . . . . . 15 ((𝑥N𝑦N) → (𝑥 ·N 𝑦) ∈ N)
6766adantl 262 . . . . . . . . . . . . . 14 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ (𝑥N𝑦N)) → (𝑥 ·N 𝑦) ∈ N)
6835, 31, 30, 63, 65, 38, 67caov411d 5686 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) = ((𝑎 ·N 𝑑) ·N (𝑐 ·N 𝑓)))
6963, 33, 40caovcomd 5657 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑎 ·N 𝑑) ·N (𝑐 ·N 𝑓)) = ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)))
7068, 69eqtrd 2072 . . . . . . . . . . . 12 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) = ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)))
7135, 31, 34, 63, 65, 52, 67caov4d 5685 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)) = ((𝑐 ·N 𝑏) ·N (𝑑 ·N 𝑒)))
7263, 35, 34caovcomd 5657 . . . . . . . . . . . . . 14 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑐 ·N 𝑏) = (𝑏 ·N 𝑐))
7372oveq1d 5527 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑏) ·N (𝑑 ·N 𝑒)) = ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
7471, 73eqtrd 2072 . . . . . . . . . . . 12 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)) = ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
7570, 74breq12d 3777 . . . . . . . . . . 11 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)) ↔ ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
7675adantr 261 . . . . . . . . . 10 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → (((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)) ↔ ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
7761, 76mpbird 156 . . . . . . . . 9 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)))
78 mulclpi 6426 . . . . . . . . . . . 12 ((𝑎N𝑓N) → (𝑎 ·N 𝑓) ∈ N)
7930, 38, 78syl2anc 391 . . . . . . . . . . 11 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑎 ·N 𝑓) ∈ N)
80 mulclpi 6426 . . . . . . . . . . . 12 ((𝑏N𝑒N) → (𝑏 ·N 𝑒) ∈ N)
8134, 52, 80syl2anc 391 . . . . . . . . . . 11 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑏 ·N 𝑒) ∈ N)
82 mulclpi 6426 . . . . . . . . . . . 12 ((𝑐N𝑑N) → (𝑐 ·N 𝑑) ∈ N)
8335, 31, 82syl2anc 391 . . . . . . . . . . 11 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑐 ·N 𝑑) ∈ N)
84 ltmpig 6437 . . . . . . . . . . 11 (((𝑎 ·N 𝑓) ∈ N ∧ (𝑏 ·N 𝑒) ∈ N ∧ (𝑐 ·N 𝑑) ∈ N) → ((𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒) ↔ ((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒))))
8579, 81, 83, 84syl3anc 1135 . . . . . . . . . 10 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒) ↔ ((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒))))
8685adantr 261 . . . . . . . . 9 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒) ↔ ((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒))))
8777, 86mpbird 156 . . . . . . . 8 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → (𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒))
88 ordpipqqs 6472 . . . . . . . . . 10 (((𝑎N𝑏N) ∧ (𝑒N𝑓N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ (𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒)))
89883adant2 923 . . . . . . . . 9 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ (𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒)))
9089adantr 261 . . . . . . . 8 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ (𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒)))
9187, 90mpbird 156 . . . . . . 7 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )
9291ex 108 . . . . . 6 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) → [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ))
931, 19, 23, 27, 923ecoptocl 6195 . . . . 5 ((𝑥Q𝑦Q𝑧Q) → ((𝑥 <Q 𝑦𝑦 <Q 𝑧) → 𝑥 <Q 𝑧))
9493adantl 262 . . . 4 ((⊤ ∧ (𝑥Q𝑦Q𝑧Q)) → ((𝑥 <Q 𝑦𝑦 <Q 𝑧) → 𝑥 <Q 𝑧))
9515, 94ispod 4041 . . 3 (⊤ → <Q Po Q)
96 nqtri3or 6494 . . . 4 ((𝑥Q𝑦Q) → (𝑥 <Q 𝑦𝑥 = 𝑦𝑦 <Q 𝑥))
9796adantl 262 . . 3 ((⊤ ∧ (𝑥Q𝑦Q)) → (𝑥 <Q 𝑦𝑥 = 𝑦𝑦 <Q 𝑥))
9895, 97issod 4056 . 2 (⊤ → <Q Or Q)
9998trud 1252 1 <Q Or Q
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ w3o 884   ∧ w3a 885   = wceq 1243  ⊤wtru 1244   ∈ wcel 1393  ⟨cop 3378   class class class wbr 3764   Or wor 4032  (class class class)co 5512  [cec 6104  Ncnpi 6370   ·N cmi 6372
 Copyright terms: Public domain W3C validator