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

Theorem ltsonq 6860
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 6810 . . . . . 6 Q = ((N × N) / ~Q )
2 id 19 . . . . . . . 8 ([⟨𝑧, 𝑤⟩] ~Q = 𝑥 → [⟨𝑧, 𝑤⟩] ~Q = 𝑥)
32, 2breq12d 3824 . . . . . . 7 ([⟨𝑧, 𝑤⟩] ~Q = 𝑥 → ([⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q𝑥 <Q 𝑥))
43notbid 625 . . . . . 6 ([⟨𝑧, 𝑤⟩] ~Q = 𝑥 → (¬ [⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ ¬ 𝑥 <Q 𝑥))
5 ltsopi 6782 . . . . . . . 8 <N Or N
6 ltrelpi 6786 . . . . . . . 8 <N ⊆ (N × N)
75, 6soirri 4781 . . . . . . 7 ¬ (𝑤 ·N 𝑧) <N (𝑤 ·N 𝑧)
8 ordpipqqs 6836 . . . . . . . . 9 (((𝑧N𝑤N) ∧ (𝑧N𝑤N)) → ([⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ (𝑧 ·N 𝑤) <N (𝑤 ·N 𝑧)))
98anidms 389 . . . . . . . 8 ((𝑧N𝑤N) → ([⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ (𝑧 ·N 𝑤) <N (𝑤 ·N 𝑧)))
10 mulcompig 6793 . . . . . . . . 9 ((𝑧N𝑤N) → (𝑧 ·N 𝑤) = (𝑤 ·N 𝑧))
1110breq1d 3821 . . . . . . . 8 ((𝑧N𝑤N) → ((𝑧 ·N 𝑤) <N (𝑤 ·N 𝑧) ↔ (𝑤 ·N 𝑧) <N (𝑤 ·N 𝑧)))
129, 11bitrd 186 . . . . . . 7 ((𝑧N𝑤N) → ([⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ (𝑤 ·N 𝑧) <N (𝑤 ·N 𝑧)))
137, 12mtbiri 633 . . . . . 6 ((𝑧N𝑤N) → ¬ [⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q )
141, 4, 13ecoptocl 6309 . . . . 5 (𝑥Q → ¬ 𝑥 <Q 𝑥)
1514adantl 271 . . . 4 ((⊤ ∧ 𝑥Q) → ¬ 𝑥 <Q 𝑥)
16 breq1 3814 . . . . . . . 8 ([⟨𝑎, 𝑏⟩] ~Q = 𝑥 → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q ))
1716anbi1d 453 . . . . . . 7 ([⟨𝑎, 𝑏⟩] ~Q = 𝑥 → (([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ (𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )))
18 breq1 3814 . . . . . . 7 ([⟨𝑎, 𝑏⟩] ~Q = 𝑥 → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q ))
1917, 18imbi12d 232 . . . . . 6 ([⟨𝑎, 𝑏⟩] ~Q = 𝑥 → ((([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) → [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ ((𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) → 𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q )))
20 breq2 3815 . . . . . . . 8 ([⟨𝑐, 𝑑⟩] ~Q = 𝑦 → (𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q𝑥 <Q 𝑦))
21 breq1 3814 . . . . . . . 8 ([⟨𝑐, 𝑑⟩] ~Q = 𝑦 → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q ))
2220, 21anbi12d 457 . . . . . . 7 ([⟨𝑐, 𝑑⟩] ~Q = 𝑦 → ((𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ (𝑥 <Q 𝑦𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q )))
2322imbi1d 229 . . . . . 6 ([⟨𝑐, 𝑑⟩] ~Q = 𝑦 → (((𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) → 𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ ((𝑥 <Q 𝑦𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q ) → 𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q )))
24 breq2 3815 . . . . . . . 8 ([⟨𝑒, 𝑓⟩] ~Q = 𝑧 → (𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q𝑦 <Q 𝑧))
2524anbi2d 452 . . . . . . 7 ([⟨𝑒, 𝑓⟩] ~Q = 𝑧 → ((𝑥 <Q 𝑦𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ (𝑥 <Q 𝑦𝑦 <Q 𝑧)))
26 breq2 3815 . . . . . . 7 ([⟨𝑒, 𝑓⟩] ~Q = 𝑧 → (𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q𝑥 <Q 𝑧))
2725, 26imbi12d 232 . . . . . 6 ([⟨𝑒, 𝑓⟩] ~Q = 𝑧 → (((𝑥 <Q 𝑦𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q ) → 𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ ((𝑥 <Q 𝑦𝑦 <Q 𝑧) → 𝑥 <Q 𝑧)))
28 ordpipqqs 6836 . . . . . . . . . . . . . . . 16 (((𝑎N𝑏N) ∧ (𝑐N𝑑N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ↔ (𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐)))
29283adant3 959 . . . . . . . . . . . . . . 15 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ↔ (𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐)))
30 simp1l 963 . . . . . . . . . . . . . . . . 17 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑎N)
31 simp2r 966 . . . . . . . . . . . . . . . . 17 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑑N)
32 mulclpi 6790 . . . . . . . . . . . . . . . . 17 ((𝑎N𝑑N) → (𝑎 ·N 𝑑) ∈ N)
3330, 31, 32syl2anc 403 . . . . . . . . . . . . . . . 16 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑎 ·N 𝑑) ∈ N)
34 simp1r 964 . . . . . . . . . . . . . . . . 17 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑏N)
35 simp2l 965 . . . . . . . . . . . . . . . . 17 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑐N)
36 mulclpi 6790 . . . . . . . . . . . . . . . . 17 ((𝑏N𝑐N) → (𝑏 ·N 𝑐) ∈ N)
3734, 35, 36syl2anc 403 . . . . . . . . . . . . . . . 16 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑏 ·N 𝑐) ∈ N)
38 simp3r 968 . . . . . . . . . . . . . . . . 17 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑓N)
39 mulclpi 6790 . . . . . . . . . . . . . . . . 17 ((𝑐N𝑓N) → (𝑐 ·N 𝑓) ∈ N)
4035, 38, 39syl2anc 403 . . . . . . . . . . . . . . . 16 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑐 ·N 𝑓) ∈ N)
41 ltmpig 6801 . . . . . . . . . . . . . . . 16 (((𝑎 ·N 𝑑) ∈ N ∧ (𝑏 ·N 𝑐) ∈ N ∧ (𝑐 ·N 𝑓) ∈ N) → ((𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐) ↔ ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐))))
4233, 37, 40, 41syl3anc 1170 . . . . . . . . . . . . . . 15 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐) ↔ ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐))))
4329, 42bitrd 186 . . . . . . . . . . . . . 14 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ↔ ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐))))
4443biimpa 290 . . . . . . . . . . . . 13 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ) → ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐)))
4544adantrr 463 . . . . . . . . . . . 12 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐)))
46 mulcompig 6793 . . . . . . . . . . . . . 14 (((𝑐 ·N 𝑓) ∈ N ∧ (𝑏 ·N 𝑐) ∈ N) → ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐)) = ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)))
4740, 37, 46syl2anc 403 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐)) = ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)))
4847adantr 270 . . . . . . . . . . . 12 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐)) = ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)))
4945, 48breqtrd 3835 . . . . . . . . . . 11 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)))
50 ordpipqqs 6836 . . . . . . . . . . . . . . 15 (((𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ (𝑐 ·N 𝑓) <N (𝑑 ·N 𝑒)))
51503adant1 957 . . . . . . . . . . . . . 14 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ (𝑐 ·N 𝑓) <N (𝑑 ·N 𝑒)))
52 simp3l 967 . . . . . . . . . . . . . . . 16 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑒N)
53 mulclpi 6790 . . . . . . . . . . . . . . . 16 ((𝑑N𝑒N) → (𝑑 ·N 𝑒) ∈ N)
5431, 52, 53syl2anc 403 . . . . . . . . . . . . . . 15 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑑 ·N 𝑒) ∈ N)
55 ltmpig 6801 . . . . . . . . . . . . . . 15 (((𝑐 ·N 𝑓) ∈ N ∧ (𝑑 ·N 𝑒) ∈ N ∧ (𝑏 ·N 𝑐) ∈ N) → ((𝑐 ·N 𝑓) <N (𝑑 ·N 𝑒) ↔ ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
5640, 54, 37, 55syl3anc 1170 . . . . . . . . . . . . . 14 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑓) <N (𝑑 ·N 𝑒) ↔ ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
5751, 56bitrd 186 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
5857biimpa 290 . . . . . . . . . . . 12 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) → ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
5958adantrl 462 . . . . . . . . . . 11 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
605, 6sotri 4782 . . . . . . . . . . 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 403 . . . . . . . . . 10 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
62 mulcompig 6793 . . . . . . . . . . . . . . 15 ((𝑥N𝑦N) → (𝑥 ·N 𝑦) = (𝑦 ·N 𝑥))
6362adantl 271 . . . . . . . . . . . . . 14 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ (𝑥N𝑦N)) → (𝑥 ·N 𝑦) = (𝑦 ·N 𝑥))
64 mulasspig 6794 . . . . . . . . . . . . . . 15 ((𝑥N𝑦N𝑧N) → ((𝑥 ·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦 ·N 𝑧)))
6564adantl 271 . . . . . . . . . . . . . 14 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ (𝑥N𝑦N𝑧N)) → ((𝑥 ·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦 ·N 𝑧)))
66 mulclpi 6790 . . . . . . . . . . . . . . 15 ((𝑥N𝑦N) → (𝑥 ·N 𝑦) ∈ N)
6766adantl 271 . . . . . . . . . . . . . 14 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ (𝑥N𝑦N)) → (𝑥 ·N 𝑦) ∈ N)
6835, 31, 30, 63, 65, 38, 67caov411d 5765 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) = ((𝑎 ·N 𝑑) ·N (𝑐 ·N 𝑓)))
6963, 33, 40caovcomd 5736 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑎 ·N 𝑑) ·N (𝑐 ·N 𝑓)) = ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)))
7068, 69eqtrd 2115 . . . . . . . . . . . 12 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) = ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)))
7135, 31, 34, 63, 65, 52, 67caov4d 5764 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)) = ((𝑐 ·N 𝑏) ·N (𝑑 ·N 𝑒)))
7263, 35, 34caovcomd 5736 . . . . . . . . . . . . . 14 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑐 ·N 𝑏) = (𝑏 ·N 𝑐))
7372oveq1d 5606 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑏) ·N (𝑑 ·N 𝑒)) = ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
7471, 73eqtrd 2115 . . . . . . . . . . . 12 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)) = ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
7570, 74breq12d 3824 . . . . . . . . . . 11 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)) ↔ ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
7675adantr 270 . . . . . . . . . 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 165 . . . . . . . . 9 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)))
78 mulclpi 6790 . . . . . . . . . . . 12 ((𝑎N𝑓N) → (𝑎 ·N 𝑓) ∈ N)
7930, 38, 78syl2anc 403 . . . . . . . . . . 11 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑎 ·N 𝑓) ∈ N)
80 mulclpi 6790 . . . . . . . . . . . 12 ((𝑏N𝑒N) → (𝑏 ·N 𝑒) ∈ N)
8134, 52, 80syl2anc 403 . . . . . . . . . . 11 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑏 ·N 𝑒) ∈ N)
82 mulclpi 6790 . . . . . . . . . . . 12 ((𝑐N𝑑N) → (𝑐 ·N 𝑑) ∈ N)
8335, 31, 82syl2anc 403 . . . . . . . . . . 11 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑐 ·N 𝑑) ∈ N)
84 ltmpig 6801 . . . . . . . . . . 11 (((𝑎 ·N 𝑓) ∈ N ∧ (𝑏 ·N 𝑒) ∈ N ∧ (𝑐 ·N 𝑑) ∈ N) → ((𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒) ↔ ((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒))))
8579, 81, 83, 84syl3anc 1170 . . . . . . . . . 10 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒) ↔ ((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒))))
8685adantr 270 . . . . . . . . 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 165 . . . . . . . 8 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → (𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒))
88 ordpipqqs 6836 . . . . . . . . . 10 (((𝑎N𝑏N) ∧ (𝑒N𝑓N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ (𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒)))
89883adant2 958 . . . . . . . . 9 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ (𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒)))
9089adantr 270 . . . . . . . 8 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ (𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒)))
9187, 90mpbird 165 . . . . . . 7 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )
9291ex 113 . . . . . 6 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) → [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ))
931, 19, 23, 27, 923ecoptocl 6311 . . . . 5 ((𝑥Q𝑦Q𝑧Q) → ((𝑥 <Q 𝑦𝑦 <Q 𝑧) → 𝑥 <Q 𝑧))
9493adantl 271 . . . 4 ((⊤ ∧ (𝑥Q𝑦Q𝑧Q)) → ((𝑥 <Q 𝑦𝑦 <Q 𝑧) → 𝑥 <Q 𝑧))
9515, 94ispod 4095 . . 3 (⊤ → <Q Po Q)
96 nqtri3or 6858 . . . 4 ((𝑥Q𝑦Q) → (𝑥 <Q 𝑦𝑥 = 𝑦𝑦 <Q 𝑥))
9796adantl 271 . . 3 ((⊤ ∧ (𝑥Q𝑦Q)) → (𝑥 <Q 𝑦𝑥 = 𝑦𝑦 <Q 𝑥))
9895, 97issod 4110 . 2 (⊤ → <Q Or Q)
9998trud 1294 1 <Q Or Q
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  w3o 919  w3a 920   = wceq 1285  wtru 1286  wcel 1434  cop 3425   class class class wbr 3811   Or wor 4086  (class class class)co 5591  [cec 6220  Ncnpi 6734   ·N cmi 6736   <N clti 6737   ~Q ceq 6741  Qcnq 6742   <Q cltq 6747
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-coll 3919  ax-sep 3922  ax-nul 3930  ax-pow 3974  ax-pr 4000  ax-un 4224  ax-setind 4316  ax-iinf 4366
This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2614  df-sbc 2827  df-csb 2920  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-nul 3270  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-int 3663  df-iun 3706  df-br 3812  df-opab 3866  df-mpt 3867  df-tr 3902  df-eprel 4080  df-id 4084  df-po 4087  df-iso 4088  df-iord 4157  df-on 4159  df-suc 4162  df-iom 4369  df-xp 4407  df-rel 4408  df-cnv 4409  df-co 4410  df-dm 4411  df-rn 4412  df-res 4413  df-ima 4414  df-iota 4934  df-fun 4971  df-fn 4972  df-f 4973  df-f1 4974  df-fo 4975  df-f1o 4976  df-fv 4977  df-ov 5594  df-oprab 5595  df-mpt2 5596  df-1st 5846  df-2nd 5847  df-recs 6002  df-irdg 6067  df-oadd 6117  df-omul 6118  df-er 6222  df-ec 6224  df-qs 6228  df-ni 6766  df-mi 6768  df-lti 6769  df-enq 6809  df-nqqs 6810  df-ltnqqs 6815
This theorem is referenced by:  nqtric  6861  lt2addnq  6866  lt2mulnq  6867  ltbtwnnqq  6877  prarloclemarch2  6881  genplt2i  6972  genpdisj  6985  addlocprlemgt  6996  nqprdisj  7006  nqprloc  7007  addnqprlemfl  7021  addnqprlemfu  7022  prmuloclemcalc  7027  mulnqprlemfl  7037  mulnqprlemfu  7038  distrlem4prl  7046  distrlem4pru  7047  ltsopr  7058  ltexprlemopl  7063  ltexprlemopu  7065  ltexprlemdisj  7068  ltexprlemru  7074  recexprlemlol  7088  recexprlemupu  7090  recexprlemdisj  7092  recexprlemss1l  7097  recexprlemss1u  7098  cauappcvgprlemopl  7108  cauappcvgprlemlol  7109  cauappcvgprlemupu  7111  cauappcvgprlemdisj  7113  cauappcvgprlemloc  7114  cauappcvgprlemladdfu  7116  cauappcvgprlemladdru  7118  cauappcvgprlemladdrl  7119  caucvgprlemk  7127  caucvgprlemnkj  7128  caucvgprlemnbj  7129  caucvgprlemm  7130  caucvgprlemopl  7131  caucvgprlemlol  7132  caucvgprlemupu  7134  caucvgprlemloc  7137  caucvgprlemladdfu  7139  caucvgprprlemloccalc  7146  caucvgprprlemml  7156  caucvgprprlemopl  7159
  Copyright terms: Public domain W3C validator