---

Step * 1 1 of Lemma same-half-cube-of-compatible


1. v3 : ℚ
2. v4 : ℚ
3. v5 : ℚ
4. v6 : ℚ
5. v7 : ℚ
6. v8 : ℚ
7. ∀a,b,c,d:ℚ.  (<a, b> = <c, d> ∈ ℚInterval ⇐⇒ (a = c ∈ ℚ) ∧ (b = d ∈ ℚ))
⊢ (v7 ≤ v8)
⇒ (((v7 = v3 ∈ ℚ) ∧ (v8 = qavg(v3;v4) ∈ ℚ)) ∨ ((v7 = qavg(v3;v4) ∈ ℚ) ∧ (v8 = v4 ∈ ℚ)))
⇒ (((v7 = v5 ∈ ℚ) ∧ (v8 = qavg(v5;v6) ∈ ℚ)) ∨ ((v7 = qavg(v5;v6) ∈ ℚ) ∧ (v8 = v6 ∈ ℚ)))
⇒ (((v5 ≤ v3) ∧ ((v6 ≤ v4) ⇒ (v3 = v6 ∈ ℚ)) ∧ ((v4 ≤ v6) ⇒ (v3 = v4 ∈ ℚ)))
   ∨ ((((v5 ≤ v3) ⇒ (v4 = v3 ∈ ℚ)) ∧ ((v3 ≤ v5) ⇒ (v4 = v5 ∈ ℚ))) ∧ (v4 ≤ v6))
   ∨ ((v5 ≤ v3) ∧ (v4 ≤ v6)))
⇒ (((v3 ≤ v5) ∧ ((v6 ≤ v4) ⇒ (v5 = v6 ∈ ℚ)) ∧ ((v4 ≤ v6) ⇒ (v5 = v4 ∈ ℚ)))
   ∨ ((((v5 ≤ v3) ⇒ (v6 = v3 ∈ ℚ)) ∧ ((v3 ≤ v5) ⇒ (v6 = v5 ∈ ℚ))) ∧ (v6 ≤ v4))
   ∨ ((v3 ≤ v5) ∧ (v6 ≤ v4)))
⇒ ((v3 = v5 ∈ ℚ) ∧ (v4 = v6 ∈ ℚ))
BY
{ (RepeatFor 5 ((D 0 THENA Auto))
   THEN SplitOrHyps
   THEN (ExRepD THENW Auto)
   THEN RationalElim ⌜v7⌝⋅
   THEN RationalElim ⌜v8⌝⋅
   THEN Try ((Repeat ((ThinTrivial
                       THEN (RationalElim ⌜v3⌝⋅ ORELSE RationalElim ⌜v4⌝⋅ ORELSE RationalElim ⌜v5⌝⋅)
                       THEN All QavgSimp))
              THEN QuickAuto
              ))) }

1
1. v4 : ℚ
2. v3 : ℚ
3. v5 : ℚ
4. v6 : ℚ
5. ∀a,b,c,d:ℚ.  (<a, b> = <c, d> ∈ ℚInterval ⇐⇒ (a = c ∈ ℚ) ∧ (b = d ∈ ℚ))
6. qavg(v3;v4) ≤ v4
7. qavg(v3;v4) = v5 ∈ ℚ
8. v4 = qavg(v5;v6) ∈ ℚ
9. (v5 ≤ v3) ⇒ (v4 = v3 ∈ ℚ)
10. (v3 ≤ v5) ⇒ (v4 = v5 ∈ ℚ)
11. v4 ≤ v6
12. v3 ≤ v5
13. (v6 ≤ v4) ⇒ (v5 = v6 ∈ ℚ)
14. (v4 ≤ v6) ⇒ (v5 = v4 ∈ ℚ)
⊢ (v3 = v5 ∈ ℚ) ∧ (v4 = v6 ∈ ℚ)

2
1. v4 : ℚ
2. v3 : ℚ
3. v5 : ℚ
4. v6 : ℚ
5. ∀a,b,c,d:ℚ.  (<a, b> = <c, d> ∈ ℚInterval ⇐⇒ (a = c ∈ ℚ) ∧ (b = d ∈ ℚ))
6. qavg(v3;v4) ≤ v4
7. qavg(v3;v4) = v5 ∈ ℚ
8. v4 = qavg(v5;v6) ∈ ℚ
9. (v5 ≤ v3) ⇒ (v4 = v3 ∈ ℚ)
10. (v3 ≤ v5) ⇒ (v4 = v5 ∈ ℚ)
11. v4 ≤ v6
12. (v5 ≤ v3) ⇒ (v6 = v3 ∈ ℚ)
13. (v3 ≤ v5) ⇒ (v6 = v5 ∈ ℚ)
14. v6 ≤ v4
⊢ (v3 = v5 ∈ ℚ) ∧ (v4 = v6 ∈ ℚ)

3
1. v4 : ℚ
2. v3 : ℚ
3. v5 : ℚ
4. v6 : ℚ
5. ∀a,b,c,d:ℚ.  (<a, b> = <c, d> ∈ ℚInterval ⇐⇒ (a = c ∈ ℚ) ∧ (b = d ∈ ℚ))
6. qavg(v3;v4) ≤ v4
7. qavg(v3;v4) = v5 ∈ ℚ
8. v4 = qavg(v5;v6) ∈ ℚ
9. (v5 ≤ v3) ⇒ (v4 = v3 ∈ ℚ)
10. (v3 ≤ v5) ⇒ (v4 = v5 ∈ ℚ)
11. v4 ≤ v6
12. v3 ≤ v5
13. v6 ≤ v4
⊢ (v3 = v5 ∈ ℚ) ∧ (v4 = v6 ∈ ℚ)

---

Latex:

---

Latex:

1.  v3  :  \mBbbQ{}
2.  v4  :  \mBbbQ{}
3.  v5  :  \mBbbQ{}
4.  v6  :  \mBbbQ{}
5.  v7  :  \mBbbQ{}
6.  v8  :  \mBbbQ{}
7.  \mforall{}a,b,c,d:\mBbbQ{}.    (<a,  b>  =  <c,  d>  \mLeftarrow{}{}\mRightarrow{}  (a  =  c)  \mwedge{}  (b  =  d))
\mvdash{}  (v7  \mleq{}  v8)
{}\mRightarrow{}  (((v7  =  v3)  \mwedge{}  (v8  =  qavg(v3;v4)))  \mvee{}  ((v7  =  qavg(v3;v4))  \mwedge{}  (v8  =  v4)))
{}\mRightarrow{}  (((v7  =  v5)  \mwedge{}  (v8  =  qavg(v5;v6)))  \mvee{}  ((v7  =  qavg(v5;v6))  \mwedge{}  (v8  =  v6)))
{}\mRightarrow{}  (((v5  \mleq{}  v3)  \mwedge{}  ((v6  \mleq{}  v4)  {}\mRightarrow{}  (v3  =  v6))  \mwedge{}  ((v4  \mleq{}  v6)  {}\mRightarrow{}  (v3  =  v4)))
      \mvee{}  ((((v5  \mleq{}  v3)  {}\mRightarrow{}  (v4  =  v3))  \mwedge{}  ((v3  \mleq{}  v5)  {}\mRightarrow{}  (v4  =  v5)))  \mwedge{}  (v4  \mleq{}  v6))
      \mvee{}  ((v5  \mleq{}  v3)  \mwedge{}  (v4  \mleq{}  v6)))
{}\mRightarrow{}  (((v3  \mleq{}  v5)  \mwedge{}  ((v6  \mleq{}  v4)  {}\mRightarrow{}  (v5  =  v6))  \mwedge{}  ((v4  \mleq{}  v6)  {}\mRightarrow{}  (v5  =  v4)))
      \mvee{}  ((((v5  \mleq{}  v3)  {}\mRightarrow{}  (v6  =  v3))  \mwedge{}  ((v3  \mleq{}  v5)  {}\mRightarrow{}  (v6  =  v5)))  \mwedge{}  (v6  \mleq{}  v4))
      \mvee{}  ((v3  \mleq{}  v5)  \mwedge{}  (v6  \mleq{}  v4)))
{}\mRightarrow{}  ((v3  =  v5)  \mwedge{}  (v4  =  v6))


By

---

Latex:
(RepeatFor  5  ((D  0  THENA  Auto))
  THEN  SplitOrHyps
  THEN  (ExRepD  THENW  Auto)
  THEN  RationalElim  \mkleeneopen{}v7\mkleeneclose{}\mcdot{}
  THEN  RationalElim  \mkleeneopen{}v8\mkleeneclose{}\mcdot{}
  THEN  Try  ((Repeat  ((ThinTrivial
                                          THEN  (RationalElim  \mkleeneopen{}v3\mkleeneclose{}\mcdot{}  ORELSE  RationalElim  \mkleeneopen{}v4\mkleeneclose{}\mcdot{}  ORELSE  RationalElim  \mkleeneopen{}v5\mkleeneclose{}\mcdot{})
                                          THEN  All  QavgSimp))
                        THEN  QuickAuto
                        )))

---

Home Index