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

Theorem ltsonq 7422
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 7372 . . . . . 6 Q = ((N × N) / ~Q )
2 id 19 . . . . . . . 8 ([⟨𝑧, 𝑤⟩] ~Q = 𝑥 → [⟨𝑧, 𝑤⟩] ~Q = 𝑥)
32, 2breq12d 4031 . . . . . . 7 ([⟨𝑧, 𝑤⟩] ~Q = 𝑥 → ([⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q𝑥 <Q 𝑥))
43notbid 668 . . . . . 6 ([⟨𝑧, 𝑤⟩] ~Q = 𝑥 → (¬ [⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ ¬ 𝑥 <Q 𝑥))
5 ltsopi 7344 . . . . . . . 8 <N Or N
6 ltrelpi 7348 . . . . . . . 8 <N ⊆ (N × N)
75, 6soirri 5038 . . . . . . 7 ¬ (𝑤 ·N 𝑧) <N (𝑤 ·N 𝑧)
8 ordpipqqs 7398 . . . . . . . . 9 (((𝑧N𝑤N) ∧ (𝑧N𝑤N)) → ([⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ (𝑧 ·N 𝑤) <N (𝑤 ·N 𝑧)))
98anidms 397 . . . . . . . 8 ((𝑧N𝑤N) → ([⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ (𝑧 ·N 𝑤) <N (𝑤 ·N 𝑧)))
10 mulcompig 7355 . . . . . . . . 9 ((𝑧N𝑤N) → (𝑧 ·N 𝑤) = (𝑤 ·N 𝑧))
1110breq1d 4028 . . . . . . . 8 ((𝑧N𝑤N) → ((𝑧 ·N 𝑤) <N (𝑤 ·N 𝑧) ↔ (𝑤 ·N 𝑧) <N (𝑤 ·N 𝑧)))
129, 11bitrd 188 . . . . . . 7 ((𝑧N𝑤N) → ([⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q ↔ (𝑤 ·N 𝑧) <N (𝑤 ·N 𝑧)))
137, 12mtbiri 676 . . . . . 6 ((𝑧N𝑤N) → ¬ [⟨𝑧, 𝑤⟩] ~Q <Q [⟨𝑧, 𝑤⟩] ~Q )
141, 4, 13ecoptocl 6643 . . . . 5 (𝑥Q → ¬ 𝑥 <Q 𝑥)
1514adantl 277 . . . 4 ((⊤ ∧ 𝑥Q) → ¬ 𝑥 <Q 𝑥)
16 breq1 4021 . . . . . . . 8 ([⟨𝑎, 𝑏⟩] ~Q = 𝑥 → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q ))
1716anbi1d 465 . . . . . . 7 ([⟨𝑎, 𝑏⟩] ~Q = 𝑥 → (([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ (𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )))
18 breq1 4021 . . . . . . 7 ([⟨𝑎, 𝑏⟩] ~Q = 𝑥 → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q ))
1917, 18imbi12d 234 . . . . . 6 ([⟨𝑎, 𝑏⟩] ~Q = 𝑥 → ((([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) → [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ ((𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) → 𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q )))
20 breq2 4022 . . . . . . . 8 ([⟨𝑐, 𝑑⟩] ~Q = 𝑦 → (𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q𝑥 <Q 𝑦))
21 breq1 4021 . . . . . . . 8 ([⟨𝑐, 𝑑⟩] ~Q = 𝑦 → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q ))
2220, 21anbi12d 473 . . . . . . 7 ([⟨𝑐, 𝑑⟩] ~Q = 𝑦 → ((𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ (𝑥 <Q 𝑦𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q )))
2322imbi1d 231 . . . . . 6 ([⟨𝑐, 𝑑⟩] ~Q = 𝑦 → (((𝑥 <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) → 𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ ((𝑥 <Q 𝑦𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q ) → 𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q )))
24 breq2 4022 . . . . . . . 8 ([⟨𝑒, 𝑓⟩] ~Q = 𝑧 → (𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q𝑦 <Q 𝑧))
2524anbi2d 464 . . . . . . 7 ([⟨𝑒, 𝑓⟩] ~Q = 𝑧 → ((𝑥 <Q 𝑦𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ (𝑥 <Q 𝑦𝑦 <Q 𝑧)))
26 breq2 4022 . . . . . . 7 ([⟨𝑒, 𝑓⟩] ~Q = 𝑧 → (𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q𝑥 <Q 𝑧))
2725, 26imbi12d 234 . . . . . 6 ([⟨𝑒, 𝑓⟩] ~Q = 𝑧 → (((𝑥 <Q 𝑦𝑦 <Q [⟨𝑒, 𝑓⟩] ~Q ) → 𝑥 <Q [⟨𝑒, 𝑓⟩] ~Q ) ↔ ((𝑥 <Q 𝑦𝑦 <Q 𝑧) → 𝑥 <Q 𝑧)))
28 ordpipqqs 7398 . . . . . . . . . . . . . . . 16 (((𝑎N𝑏N) ∧ (𝑐N𝑑N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ↔ (𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐)))
29283adant3 1019 . . . . . . . . . . . . . . 15 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ↔ (𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐)))
30 simp1l 1023 . . . . . . . . . . . . . . . . 17 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑎N)
31 simp2r 1026 . . . . . . . . . . . . . . . . 17 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑑N)
32 mulclpi 7352 . . . . . . . . . . . . . . . . 17 ((𝑎N𝑑N) → (𝑎 ·N 𝑑) ∈ N)
3330, 31, 32syl2anc 411 . . . . . . . . . . . . . . . 16 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑎 ·N 𝑑) ∈ N)
34 simp1r 1024 . . . . . . . . . . . . . . . . 17 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑏N)
35 simp2l 1025 . . . . . . . . . . . . . . . . 17 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑐N)
36 mulclpi 7352 . . . . . . . . . . . . . . . . 17 ((𝑏N𝑐N) → (𝑏 ·N 𝑐) ∈ N)
3734, 35, 36syl2anc 411 . . . . . . . . . . . . . . . 16 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑏 ·N 𝑐) ∈ N)
38 simp3r 1028 . . . . . . . . . . . . . . . . 17 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑓N)
39 mulclpi 7352 . . . . . . . . . . . . . . . . 17 ((𝑐N𝑓N) → (𝑐 ·N 𝑓) ∈ N)
4035, 38, 39syl2anc 411 . . . . . . . . . . . . . . . 16 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑐 ·N 𝑓) ∈ N)
41 ltmpig 7363 . . . . . . . . . . . . . . . 16 (((𝑎 ·N 𝑑) ∈ N ∧ (𝑏 ·N 𝑐) ∈ N ∧ (𝑐 ·N 𝑓) ∈ N) → ((𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐) ↔ ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐))))
4233, 37, 40, 41syl3anc 1249 . . . . . . . . . . . . . . 15 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑎 ·N 𝑑) <N (𝑏 ·N 𝑐) ↔ ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐))))
4329, 42bitrd 188 . . . . . . . . . . . . . 14 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ↔ ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐))))
4443biimpa 296 . . . . . . . . . . . . 13 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ) → ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐)))
4544adantrr 479 . . . . . . . . . . . 12 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐)))
46 mulcompig 7355 . . . . . . . . . . . . . 14 (((𝑐 ·N 𝑓) ∈ N ∧ (𝑏 ·N 𝑐) ∈ N) → ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐)) = ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)))
4740, 37, 46syl2anc 411 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐)) = ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)))
4847adantr 276 . . . . . . . . . . . 12 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑐 ·N 𝑓) ·N (𝑏 ·N 𝑐)) = ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)))
4945, 48breqtrd 4044 . . . . . . . . . . 11 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)))
50 ordpipqqs 7398 . . . . . . . . . . . . . . 15 (((𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ (𝑐 ·N 𝑓) <N (𝑑 ·N 𝑒)))
51503adant1 1017 . . . . . . . . . . . . . 14 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ (𝑐 ·N 𝑓) <N (𝑑 ·N 𝑒)))
52 simp3l 1027 . . . . . . . . . . . . . . . 16 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → 𝑒N)
53 mulclpi 7352 . . . . . . . . . . . . . . . 16 ((𝑑N𝑒N) → (𝑑 ·N 𝑒) ∈ N)
5431, 52, 53syl2anc 411 . . . . . . . . . . . . . . 15 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑑 ·N 𝑒) ∈ N)
55 ltmpig 7363 . . . . . . . . . . . . . . 15 (((𝑐 ·N 𝑓) ∈ N ∧ (𝑑 ·N 𝑒) ∈ N ∧ (𝑏 ·N 𝑐) ∈ N) → ((𝑐 ·N 𝑓) <N (𝑑 ·N 𝑒) ↔ ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
5640, 54, 37, 55syl3anc 1249 . . . . . . . . . . . . . 14 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑓) <N (𝑑 ·N 𝑒) ↔ ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
5751, 56bitrd 188 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
5857biimpa 296 . . . . . . . . . . . 12 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) → ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
5958adantrl 478 . . . . . . . . . . 11 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑏 ·N 𝑐) ·N (𝑐 ·N 𝑓)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
605, 6sotri 5039 . . . . . . . . . . 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 411 . . . . . . . . . 10 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
62 mulcompig 7355 . . . . . . . . . . . . . . 15 ((𝑥N𝑦N) → (𝑥 ·N 𝑦) = (𝑦 ·N 𝑥))
6362adantl 277 . . . . . . . . . . . . . 14 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ (𝑥N𝑦N)) → (𝑥 ·N 𝑦) = (𝑦 ·N 𝑥))
64 mulasspig 7356 . . . . . . . . . . . . . . 15 ((𝑥N𝑦N𝑧N) → ((𝑥 ·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦 ·N 𝑧)))
6564adantl 277 . . . . . . . . . . . . . 14 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ (𝑥N𝑦N𝑧N)) → ((𝑥 ·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦 ·N 𝑧)))
66 mulclpi 7352 . . . . . . . . . . . . . . 15 ((𝑥N𝑦N) → (𝑥 ·N 𝑦) ∈ N)
6766adantl 277 . . . . . . . . . . . . . 14 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ (𝑥N𝑦N)) → (𝑥 ·N 𝑦) ∈ N)
6835, 31, 30, 63, 65, 38, 67caov411d 6078 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) = ((𝑎 ·N 𝑑) ·N (𝑐 ·N 𝑓)))
6963, 33, 40caovcomd 6049 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑎 ·N 𝑑) ·N (𝑐 ·N 𝑓)) = ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)))
7068, 69eqtrd 2222 . . . . . . . . . . . 12 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) = ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)))
7135, 31, 34, 63, 65, 52, 67caov4d 6077 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)) = ((𝑐 ·N 𝑏) ·N (𝑑 ·N 𝑒)))
7263, 35, 34caovcomd 6049 . . . . . . . . . . . . . 14 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑐 ·N 𝑏) = (𝑏 ·N 𝑐))
7372oveq1d 5907 . . . . . . . . . . . . 13 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑏) ·N (𝑑 ·N 𝑒)) = ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
7471, 73eqtrd 2222 . . . . . . . . . . . 12 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)) = ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒)))
7570, 74breq12d 4031 . . . . . . . . . . 11 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)) ↔ ((𝑐 ·N 𝑓) ·N (𝑎 ·N 𝑑)) <N ((𝑏 ·N 𝑐) ·N (𝑑 ·N 𝑒))))
7675adantr 276 . . . . . . . . . 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 167 . . . . . . . . 9 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒)))
78 mulclpi 7352 . . . . . . . . . . . 12 ((𝑎N𝑓N) → (𝑎 ·N 𝑓) ∈ N)
7930, 38, 78syl2anc 411 . . . . . . . . . . 11 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑎 ·N 𝑓) ∈ N)
80 mulclpi 7352 . . . . . . . . . . . 12 ((𝑏N𝑒N) → (𝑏 ·N 𝑒) ∈ N)
8134, 52, 80syl2anc 411 . . . . . . . . . . 11 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑏 ·N 𝑒) ∈ N)
82 mulclpi 7352 . . . . . . . . . . . 12 ((𝑐N𝑑N) → (𝑐 ·N 𝑑) ∈ N)
8335, 31, 82syl2anc 411 . . . . . . . . . . 11 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (𝑐 ·N 𝑑) ∈ N)
84 ltmpig 7363 . . . . . . . . . . 11 (((𝑎 ·N 𝑓) ∈ N ∧ (𝑏 ·N 𝑒) ∈ N ∧ (𝑐 ·N 𝑑) ∈ N) → ((𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒) ↔ ((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒))))
8579, 81, 83, 84syl3anc 1249 . . . . . . . . . 10 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ((𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒) ↔ ((𝑐 ·N 𝑑) ·N (𝑎 ·N 𝑓)) <N ((𝑐 ·N 𝑑) ·N (𝑏 ·N 𝑒))))
8685adantr 276 . . . . . . . . 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 167 . . . . . . . 8 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → (𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒))
88 ordpipqqs 7398 . . . . . . . . . 10 (((𝑎N𝑏N) ∧ (𝑒N𝑓N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ (𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒)))
89883adant2 1018 . . . . . . . . 9 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ (𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒)))
9089adantr 276 . . . . . . . 8 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ↔ (𝑎 ·N 𝑓) <N (𝑏 ·N 𝑒)))
9187, 90mpbird 167 . . . . . . 7 ((((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) ∧ ([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )) → [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q )
9291ex 115 . . . . . 6 (((𝑎N𝑏N) ∧ (𝑐N𝑑N) ∧ (𝑒N𝑓N)) → (([⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑐, 𝑑⟩] ~Q ∧ [⟨𝑐, 𝑑⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ) → [⟨𝑎, 𝑏⟩] ~Q <Q [⟨𝑒, 𝑓⟩] ~Q ))
931, 19, 23, 27, 923ecoptocl 6645 . . . . 5 ((𝑥Q𝑦Q𝑧Q) → ((𝑥 <Q 𝑦𝑦 <Q 𝑧) → 𝑥 <Q 𝑧))
9493adantl 277 . . . 4 ((⊤ ∧ (𝑥Q𝑦Q𝑧Q)) → ((𝑥 <Q 𝑦𝑦 <Q 𝑧) → 𝑥 <Q 𝑧))
9515, 94ispod 4319 . . 3 (⊤ → <Q Po Q)
96 nqtri3or 7420 . . . 4 ((𝑥Q𝑦Q) → (𝑥 <Q 𝑦𝑥 = 𝑦𝑦 <Q 𝑥))
9796adantl 277 . . 3 ((⊤ ∧ (𝑥Q𝑦Q)) → (𝑥 <Q 𝑦𝑥 = 𝑦𝑦 <Q 𝑥))
9895, 97issod 4334 . 2 (⊤ → <Q Or Q)
9998mptru 1373 1 <Q Or Q
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  w3o 979  w3a 980   = wceq 1364  wtru 1365  wcel 2160  cop 3610   class class class wbr 4018   Or wor 4310  (class class class)co 5892  [cec 6552  Ncnpi 7296   ·N cmi 7298   <N clti 7299   ~Q ceq 7303  Qcnq 7304   <Q cltq 7309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-iinf 4602
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-eprel 4304  df-id 4308  df-po 4311  df-iso 4312  df-iord 4381  df-on 4383  df-suc 4386  df-iom 4605  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-res 4653  df-ima 4654  df-iota 5193  df-fun 5234  df-fn 5235  df-f 5236  df-f1 5237  df-fo 5238  df-f1o 5239  df-fv 5240  df-ov 5895  df-oprab 5896  df-mpo 5897  df-1st 6160  df-2nd 6161  df-recs 6325  df-irdg 6390  df-oadd 6440  df-omul 6441  df-er 6554  df-ec 6556  df-qs 6560  df-ni 7328  df-mi 7330  df-lti 7331  df-enq 7371  df-nqqs 7372  df-ltnqqs 7377
This theorem is referenced by:  nqtric  7423  lt2addnq  7428  lt2mulnq  7429  ltbtwnnqq  7439  prarloclemarch2  7443  genplt2i  7534  genpdisj  7547  addlocprlemgt  7558  nqprdisj  7568  nqprloc  7569  addnqprlemfl  7583  addnqprlemfu  7584  prmuloclemcalc  7589  mulnqprlemfl  7599  mulnqprlemfu  7600  distrlem4prl  7608  distrlem4pru  7609  ltsopr  7620  ltexprlemopl  7625  ltexprlemopu  7627  ltexprlemdisj  7630  ltexprlemru  7636  recexprlemlol  7650  recexprlemupu  7652  recexprlemdisj  7654  recexprlemss1l  7659  recexprlemss1u  7660  cauappcvgprlemopl  7670  cauappcvgprlemlol  7671  cauappcvgprlemupu  7673  cauappcvgprlemdisj  7675  cauappcvgprlemloc  7676  cauappcvgprlemladdfu  7678  cauappcvgprlemladdru  7680  cauappcvgprlemladdrl  7681  caucvgprlemk  7689  caucvgprlemnkj  7690  caucvgprlemnbj  7691  caucvgprlemm  7692  caucvgprlemopl  7693  caucvgprlemlol  7694  caucvgprlemupu  7696  caucvgprlemloc  7699  caucvgprlemladdfu  7701  caucvgprprlemloccalc  7708  caucvgprprlemml  7718  caucvgprprlemopl  7721  suplocexprlemru  7743
  Copyright terms: Public domain W3C validator