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

Theorem prarloclemup 6651
 Description: Contracting the upper side of an interval which straddles a Dedekind cut. Lemma for prarloc 6659. (Contributed by Jim Kingdon, 10-Nov-2019.)
Assertion
Ref Expression
prarloclemup +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0

Proof of Theorem prarloclemup
StepHypRef Expression
1 simpllr 494 . . 3 +Q0 ~Q0 ·Q0
2 simprl 491 . . 3 +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0
3 simplr 490 . . 3 +Q0 ~Q0 ·Q0
4 rspe 2387 . . 3 +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0
51, 2, 3, 4syl12anc 1144 . 2 +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0
65exp31 350 1 +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0
 Colors of variables: wff set class Syntax hints:   wi 4   wa 101   w3a 896   wcel 1409  wrex 2324  cop 3406   csuc 4130  com 4341  (class class class)co 5540  c1o 6025  c2o 6026   coa 6029  cec 6135   ceq 6435  cnq 6436   cplq 6438   cmq 6439   ~Q0 ceq0 6442   +Q0 cplq0 6445   ·Q0 cmq0 6446  cnp 6447 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416 This theorem depends on definitions:  df-bi 114  df-rex 2329 This theorem is referenced by:  prarloclem3step  6652
 Copyright terms: Public domain W3C validator