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

Theorem ltdcnq 6250
 Description: Less-than for positive fractions is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
Assertion
Ref Expression
ltdcnq ((A Q B Q) → DECID A <Q B)

Proof of Theorem ltdcnq
Dummy variables w x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nqpi 6231 . . . 4 (A Qxy((x N y N) A = [⟨x, y⟩] ~Q ))
2 nqpi 6231 . . . 4 (B Qzw((z N w N) B = [⟨z, w⟩] ~Q ))
31, 2anim12i 321 . . 3 ((A Q B Q) → (xy((x N y N) A = [⟨x, y⟩] ~Q ) zw((z N w N) B = [⟨z, w⟩] ~Q )))
4 ee4anv 1787 . . 3 (xyzw(((x N y N) A = [⟨x, y⟩] ~Q ) ((z N w N) B = [⟨z, w⟩] ~Q )) ↔ (xy((x N y N) A = [⟨x, y⟩] ~Q ) zw((z N w N) B = [⟨z, w⟩] ~Q )))
53, 4sylibr 137 . 2 ((A Q B Q) → xyzw(((x N y N) A = [⟨x, y⟩] ~Q ) ((z N w N) B = [⟨z, w⟩] ~Q )))
6 mulclpi 6182 . . . . . . . . 9 ((x N w N) → (x ·N w) N)
7 mulclpi 6182 . . . . . . . . 9 ((y N z N) → (y ·N z) N)
8 ltdcpi 6177 . . . . . . . . 9 (((x ·N w) N (y ·N z) N) → DECID (x ·N w) <N (y ·N z))
96, 7, 8syl2an 273 . . . . . . . 8 (((x N w N) (y N z N)) → DECID (x ·N w) <N (y ·N z))
109an42s 510 . . . . . . 7 (((x N y N) (z N w N)) → DECID (x ·N w) <N (y ·N z))
11 ordpipqqs 6227 . . . . . . . 8 (((x N y N) (z N w N)) → ([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ (x ·N w) <N (y ·N z)))
1211dcbid 736 . . . . . . 7 (((x N y N) (z N w N)) → (DECID [⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~QDECID (x ·N w) <N (y ·N z)))
1310, 12mpbird 156 . . . . . 6 (((x N y N) (z N w N)) → DECID [⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q )
1413ad2ant2r 466 . . . . 5 ((((x N y N) A = [⟨x, y⟩] ~Q ) ((z N w N) B = [⟨z, w⟩] ~Q )) → DECID [⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q )
15 breq12 3739 . . . . . . 7 ((A = [⟨x, y⟩] ~Q B = [⟨z, w⟩] ~Q ) → (A <Q B ↔ [⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ))
1615ad2ant2l 465 . . . . . 6 ((((x N y N) A = [⟨x, y⟩] ~Q ) ((z N w N) B = [⟨z, w⟩] ~Q )) → (A <Q B ↔ [⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ))
1716dcbid 736 . . . . 5 ((((x N y N) A = [⟨x, y⟩] ~Q ) ((z N w N) B = [⟨z, w⟩] ~Q )) → (DECID A <Q BDECID [⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ))
1814, 17mpbird 156 . . . 4 ((((x N y N) A = [⟨x, y⟩] ~Q ) ((z N w N) B = [⟨z, w⟩] ~Q )) → DECID A <Q B)
1918exlimivv 1754 . . 3 (zw(((x N y N) A = [⟨x, y⟩] ~Q ) ((z N w N) B = [⟨z, w⟩] ~Q )) → DECID A <Q B)
2019exlimivv 1754 . 2 (xyzw(((x N y N) A = [⟨x, y⟩] ~Q ) ((z N w N) B = [⟨z, w⟩] ~Q )) → DECID A <Q B)
215, 20syl 14 1 ((A Q B Q) → DECID A <Q B)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98  DECID wdc 730   = wceq 1226  ∃wex 1358   ∈ wcel 1370  ⟨cop 3349   class class class wbr 3734  (class class class)co 5432  [cec 6011  Ncnpi 6126   ·N cmi 6128
 Copyright terms: Public domain W3C validator