---

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


1. v6 : ℚ
2. v4 : ℚ
3. v3 : ℚ
4. ∀a,b,c,d:ℚ.  (<a, b> = <c, d> ∈ ℚInterval ⇐⇒ (a = c ∈ ℚ) ∧ (b = d ∈ ℚ))
5. v3 ≤ v4
6. qavg(v3;v4) = v6 ∈ ℚ
7. v4 = v6 ∈ ℚ
8. (v6 ≤ v3) ⇒ (v4 = v3 ∈ ℚ)
9. v4 ≤ v6
10. v3 ≤ v6
11. v6 ≤ v4
12. v6 = v4 ∈ ℚ
⊢ v3 = v6 ∈ ℚ
BY
{ (ThinTrivial THEN RationalElim ⌜v6⌝⋅ THEN All QavgSimp THEN Auto) }

---

Latex:

---

Latex:

1.  v6  :  \mBbbQ{}
2.  v4  :  \mBbbQ{}
3.  v3  :  \mBbbQ{}
4.  \mforall{}a,b,c,d:\mBbbQ{}.    (<a,  b>  =  <c,  d>  \mLeftarrow{}{}\mRightarrow{}  (a  =  c)  \mwedge{}  (b  =  d))
5.  v3  \mleq{}  v4
6.  qavg(v3;v4)  =  v6
7.  v4  =  v6
8.  (v6  \mleq{}  v3)  {}\mRightarrow{}  (v4  =  v3)
9.  v4  \mleq{}  v6
10.  v3  \mleq{}  v6
11.  v6  \mleq{}  v4
12.  v6  =  v4
\mvdash{}  v3  =  v6


By

---

Latex:
(ThinTrivial  THEN  RationalElim  \mkleeneopen{}v6\mkleeneclose{}\mcdot{}  THEN  All  QavgSimp  THEN  Auto)

---

Home Index