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

Theorem nqtri3or 6380
 Description: Trichotomy for positive fractions. (Contributed by Jim Kingdon, 21-Sep-2019.)
Assertion
Ref Expression
nqtri3or ((A Q B Q) → (A <Q B A = B B <Q A))

Proof of Theorem nqtri3or
Dummy variables u v w z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nqqs 6332 . 2 Q = ((N × N) / ~Q )
2 breq1 3758 . . 3 ([⟨z, w⟩] ~Q = A → ([⟨z, w⟩] ~Q <Q [⟨u, v⟩] ~QA <Q [⟨u, v⟩] ~Q ))
3 eqeq1 2043 . . 3 ([⟨z, w⟩] ~Q = A → ([⟨z, w⟩] ~Q = [⟨u, v⟩] ~QA = [⟨u, v⟩] ~Q ))
4 breq2 3759 . . 3 ([⟨z, w⟩] ~Q = A → ([⟨u, v⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ [⟨u, v⟩] ~Q <Q A))
52, 3, 43orbi123d 1205 . 2 ([⟨z, w⟩] ~Q = A → (([⟨z, w⟩] ~Q <Q [⟨u, v⟩] ~Q [⟨z, w⟩] ~Q = [⟨u, v⟩] ~Q [⟨u, v⟩] ~Q <Q [⟨z, w⟩] ~Q ) ↔ (A <Q [⟨u, v⟩] ~Q A = [⟨u, v⟩] ~Q [⟨u, v⟩] ~Q <Q A)))
6 breq2 3759 . . 3 ([⟨u, v⟩] ~Q = B → (A <Q [⟨u, v⟩] ~QA <Q B))
7 eqeq2 2046 . . 3 ([⟨u, v⟩] ~Q = B → (A = [⟨u, v⟩] ~QA = B))
8 breq1 3758 . . 3 ([⟨u, v⟩] ~Q = B → ([⟨u, v⟩] ~Q <Q AB <Q A))
96, 7, 83orbi123d 1205 . 2 ([⟨u, v⟩] ~Q = B → ((A <Q [⟨u, v⟩] ~Q A = [⟨u, v⟩] ~Q [⟨u, v⟩] ~Q <Q A) ↔ (A <Q B A = B B <Q A)))
10 mulclpi 6312 . . . . 5 ((z N v N) → (z ·N v) N)
1110ad2ant2rl 480 . . . 4 (((z N w N) (u N v N)) → (z ·N v) N)
12 mulclpi 6312 . . . . 5 ((w N u N) → (w ·N u) N)
1312ad2ant2lr 479 . . . 4 (((z N w N) (u N v N)) → (w ·N u) N)
14 pitri3or 6306 . . . 4 (((z ·N v) N (w ·N u) N) → ((z ·N v) <N (w ·N u) (z ·N v) = (w ·N u) (w ·N u) <N (z ·N v)))
1511, 13, 14syl2anc 391 . . 3 (((z N w N) (u N v N)) → ((z ·N v) <N (w ·N u) (z ·N v) = (w ·N u) (w ·N u) <N (z ·N v)))
16 ordpipqqs 6358 . . . 4 (((z N w N) (u N v N)) → ([⟨z, w⟩] ~Q <Q [⟨u, v⟩] ~Q ↔ (z ·N v) <N (w ·N u)))
17 enqeceq 6343 . . . 4 (((z N w N) (u N v N)) → ([⟨z, w⟩] ~Q = [⟨u, v⟩] ~Q ↔ (z ·N v) = (w ·N u)))
18 ordpipqqs 6358 . . . . . 6 (((u N v N) (z N w N)) → ([⟨u, v⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ (u ·N w) <N (v ·N z)))
1918ancoms 255 . . . . 5 (((z N w N) (u N v N)) → ([⟨u, v⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ (u ·N w) <N (v ·N z)))
20 mulcompig 6315 . . . . . . 7 ((w N u N) → (w ·N u) = (u ·N w))
2120ad2ant2lr 479 . . . . . 6 (((z N w N) (u N v N)) → (w ·N u) = (u ·N w))
22 mulcompig 6315 . . . . . . 7 ((z N v N) → (z ·N v) = (v ·N z))
2322ad2ant2rl 480 . . . . . 6 (((z N w N) (u N v N)) → (z ·N v) = (v ·N z))
2421, 23breq12d 3768 . . . . 5 (((z N w N) (u N v N)) → ((w ·N u) <N (z ·N v) ↔ (u ·N w) <N (v ·N z)))
2519, 24bitr4d 180 . . . 4 (((z N w N) (u N v N)) → ([⟨u, v⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ (w ·N u) <N (z ·N v)))
2616, 17, 253orbi123d 1205 . . 3 (((z N w N) (u N v N)) → (([⟨z, w⟩] ~Q <Q [⟨u, v⟩] ~Q [⟨z, w⟩] ~Q = [⟨u, v⟩] ~Q [⟨u, v⟩] ~Q <Q [⟨z, w⟩] ~Q ) ↔ ((z ·N v) <N (w ·N u) (z ·N v) = (w ·N u) (w ·N u) <N (z ·N v))))
2715, 26mpbird 156 . 2 (((z N w N) (u N v N)) → ([⟨z, w⟩] ~Q <Q [⟨u, v⟩] ~Q [⟨z, w⟩] ~Q = [⟨u, v⟩] ~Q [⟨u, v⟩] ~Q <Q [⟨z, w⟩] ~Q ))
281, 5, 9, 272ecoptocl 6130 1 ((A Q B Q) → (A <Q B A = B B <Q A))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∨ w3o 883   = wceq 1242   ∈ wcel 1390  ⟨cop 3370   class class class wbr 3755  (class class class)co 5455  [cec 6040  Ncnpi 6256   ·N cmi 6258
 Copyright terms: Public domain W3C validator