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

Theorem prubl 6461
 Description: A positive fraction not in a lower cut is an upper bound. (Contributed by Jim Kingdon, 29-Sep-2019.)
Assertion
Ref Expression
prubl (((⟨𝐿, 𝑈 P B 𝐿) 𝐶 Q) → (¬ 𝐶 𝐿B <Q 𝐶))

Proof of Theorem prubl
StepHypRef Expression
1 eleq1 2097 . . . . . . 7 (B = 𝐶 → (B 𝐿𝐶 𝐿))
21biimpcd 148 . . . . . 6 (B 𝐿 → (B = 𝐶𝐶 𝐿))
32adantl 262 . . . . 5 ((⟨𝐿, 𝑈 P B 𝐿) → (B = 𝐶𝐶 𝐿))
4 prcdnql 6459 . . . . 5 ((⟨𝐿, 𝑈 P B 𝐿) → (𝐶 <Q B𝐶 𝐿))
53, 4jaod 636 . . . 4 ((⟨𝐿, 𝑈 P B 𝐿) → ((B = 𝐶 𝐶 <Q B) → 𝐶 𝐿))
65con3d 560 . . 3 ((⟨𝐿, 𝑈 P B 𝐿) → (¬ 𝐶 𝐿 → ¬ (B = 𝐶 𝐶 <Q B)))
76adantr 261 . 2 (((⟨𝐿, 𝑈 P B 𝐿) 𝐶 Q) → (¬ 𝐶 𝐿 → ¬ (B = 𝐶 𝐶 <Q B)))
8 elprnql 6456 . . 3 ((⟨𝐿, 𝑈 P B 𝐿) → B Q)
9 nqtric 6376 . . 3 ((B Q 𝐶 Q) → (B <Q 𝐶 ↔ ¬ (B = 𝐶 𝐶 <Q B)))
108, 9sylan 267 . 2 (((⟨𝐿, 𝑈 P B 𝐿) 𝐶 Q) → (B <Q 𝐶 ↔ ¬ (B = 𝐶 𝐶 <Q B)))
117, 10sylibrd 158 1 (((⟨𝐿, 𝑈 P B 𝐿) 𝐶 Q) → (¬ 𝐶 𝐿B <Q 𝐶))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 628   = wceq 1242   ∈ wcel 1390  ⟨cop 3369   class class class wbr 3754  Qcnq 6257
 Copyright terms: Public domain W3C validator