---

Step * 2 1 2 of Lemma half-cube-of-face


1. v13 : ℚ
2. v14 : ℚ
3. v12 : ℚ
4. qavg(qavg(v13;v14);v12) = v14 ∈ ℚ
5. v13 ≤ v14
6. ((qavg(v13;v14) ≤ v13) ∧ ((v12 ≤ v14) ⇒ (v13 = v12 ∈ ℚ)) ∧ ((v14 ≤ v12) ⇒ (v13 = v14 ∈ ℚ)))
∨ ((((qavg(v13;v14) ≤ v13) ⇒ (v14 = v13 ∈ ℚ)) ∧ ((v13 ≤ qavg(v13;v14)) ⇒ (v14 = qavg(v13;v14) ∈ ℚ))) ∧ (v14 ≤ v12))
∨ ((qavg(v13;v14) ≤ v13) ∧ (v14 ≤ v12))
7. ((v13 ≤ qavg(v13;v14)) ∧ ((v12 ≤ v14) ⇒ (qavg(v13;v14) = v12 ∈ ℚ)) ∧ ((v14 ≤ v12) ⇒ (qavg(v13;v14) = v14 ∈ ℚ)))
∨ ((((qavg(v13;v14) ≤ v13) ⇒ (v12 = v13 ∈ ℚ)) ∧ ((v13 ≤ qavg(v13;v14)) ⇒ (v12 = qavg(v13;v14) ∈ ℚ))) ∧ (v12 ≤ v14))
∨ ((v13 ≤ qavg(v13;v14)) ∧ (v12 ≤ v14))
⊢ ((v13 = v14 ∈ ℚ) ∧ (v12 = v13 ∈ ℚ)) ∨ ((v14 = v13 ∈ ℚ) ∧ (v12 = v14 ∈ ℚ)) ∨ ((v13 = v14 ∈ ℚ) ∧ (v12 = v14 ∈ ℚ))
BY
{ (All QavgSimp
   THEN SplitOrHyps
   THEN Auto
   THEN (Assert (v12 ≤ v14) ∨ (v14 ≤ v12) BY
               EAuto 1)
   THEN D -1
   THEN ThinTrivial
   THEN RationalElim ⌜v13⌝⋅
   THEN All QavgSimp
   THEN Auto) }

---

Latex:

---

Latex:

1.  v13  :  \mBbbQ{}
2.  v14  :  \mBbbQ{}
3.  v12  :  \mBbbQ{}
4.  qavg(qavg(v13;v14);v12)  =  v14
5.  v13  \mleq{}  v14
6.  ((qavg(v13;v14)  \mleq{}  v13)  \mwedge{}  ((v12  \mleq{}  v14)  {}\mRightarrow{}  (v13  =  v12))  \mwedge{}  ((v14  \mleq{}  v12)  {}\mRightarrow{}  (v13  =  v14)))
\mvee{}  ((((qavg(v13;v14)  \mleq{}  v13)  {}\mRightarrow{}  (v14  =  v13))  \mwedge{}  ((v13  \mleq{}  qavg(v13;v14))  {}\mRightarrow{}  (v14  =  qavg(v13;v14))))
    \mwedge{}  (v14  \mleq{}  v12))
\mvee{}  ((qavg(v13;v14)  \mleq{}  v13)  \mwedge{}  (v14  \mleq{}  v12))
7.  ((v13  \mleq{}  qavg(v13;v14))
      \mwedge{}  ((v12  \mleq{}  v14)  {}\mRightarrow{}  (qavg(v13;v14)  =  v12))
      \mwedge{}  ((v14  \mleq{}  v12)  {}\mRightarrow{}  (qavg(v13;v14)  =  v14)))
\mvee{}  ((((qavg(v13;v14)  \mleq{}  v13)  {}\mRightarrow{}  (v12  =  v13))  \mwedge{}  ((v13  \mleq{}  qavg(v13;v14))  {}\mRightarrow{}  (v12  =  qavg(v13;v14))))
    \mwedge{}  (v12  \mleq{}  v14))
\mvee{}  ((v13  \mleq{}  qavg(v13;v14))  \mwedge{}  (v12  \mleq{}  v14))
\mvdash{}  ((v13  =  v14)  \mwedge{}  (v12  =  v13))  \mvee{}  ((v14  =  v13)  \mwedge{}  (v12  =  v14))  \mvee{}  ((v13  =  v14)  \mwedge{}  (v12  =  v14))


By

---

Latex:
(All  QavgSimp
  THEN  SplitOrHyps
  THEN  Auto
  THEN  (Assert  (v12  \mleq{}  v14)  \mvee{}  (v14  \mleq{}  v12)  BY
                          EAuto  1)
  THEN  D  -1
  THEN  ThinTrivial
  THEN  RationalElim  \mkleeneopen{}v13\mkleeneclose{}\mcdot{}
  THEN  All  QavgSimp
  THEN  Auto)

---

Home Index