---

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


1. v13 : ℚ
2. v14 : ℚ
3. v11 : ℚ
4. v12 : ℚ
5. v9 : ℚ
6. v10 : ℚ
7. v7 : ℚ
8. v8 : ℚ
9. v5 : ℚ
10. v6 : ℚ
11. ((v11 = v5 ∈ ℚ) ∧ (v12 = v5 ∈ ℚ)) ∨ ((v11 = v6 ∈ ℚ) ∧ (v12 = v6 ∈ ℚ)) ∨ ((v11 = v5 ∈ ℚ) ∧ (v12 = v6 ∈ ℚ))
12. ((v7 = v9 ∈ ℚ) ∧ (v8 = v9 ∈ ℚ)) ∨ ((v7 = v10 ∈ ℚ) ∧ (v8 = v10 ∈ ℚ)) ∨ ((v7 = v9 ∈ ℚ) ∧ (v8 = v10 ∈ ℚ))
13. ((v7 = v11 ∈ ℚ) ∧ (v8 = qavg(v11;v12) ∈ ℚ)) ∨ ((v7 = qavg(v11;v12) ∈ ℚ) ∧ (v8 = v12 ∈ ℚ))
14. ((v9 = v13 ∈ ℚ) ∧ (v10 = qavg(v13;v14) ∈ ℚ)) ∨ ((v9 = qavg(v13;v14) ∈ ℚ) ∧ (v10 = v14 ∈ ℚ))
15. v13 ≤ v14
16. ((qmax(v13;v5) = v13 ∈ ℚ) ∧ (qmin(v14;v6) = v13 ∈ ℚ))
∨ ((qmax(v13;v5) = v14 ∈ ℚ) ∧ (qmin(v14;v6) = v14 ∈ ℚ))
∨ ((qmax(v13;v5) = v13 ∈ ℚ) ∧ (qmin(v14;v6) = v14 ∈ ℚ))
17. ((qmax(v13;v5) = v5 ∈ ℚ) ∧ (qmin(v14;v6) = v5 ∈ ℚ))
∨ ((qmax(v13;v5) = v6 ∈ ℚ) ∧ (qmin(v14;v6) = v6 ∈ ℚ))
∨ ((qmax(v13;v5) = v5 ∈ ℚ) ∧ (qmin(v14;v6) = v6 ∈ ℚ))
⊢ ((v11 = v13 ∈ ℚ) ∧ (v12 = v13 ∈ ℚ)) ∨ ((v11 = v14 ∈ ℚ) ∧ (v12 = v14 ∈ ℚ)) ∨ ((v11 = v13 ∈ ℚ) ∧ (v12 = v14 ∈ ℚ))
BY
{ (RepeatFor 2 (MoveToConcl (-1))
   THEN SplitOrHyps
   THEN (ExRepD THENA Auto)
   THEN RationalElim ⌜v9⌝⋅
   THEN RationalElim ⌜v8⌝⋅
   THEN RationalElim ⌜v11⌝⋅
   THEN RationalElim ⌜v10⌝⋅
   THEN All QavgSimp
   THEN (Try ((RationalElim ⌜v6⌝⋅ THEN All QavgSimp))
         THEN Try ((RationalElim ⌜v7⌝⋅ THEN All QavgSimp))
         THEN Try ((RationalElim ⌜v5⌝⋅ THEN All QavgSimp)))
   THEN Auto
   THEN (All (RWO "qmax-eq-iff-1 qmax-eq-iff-2 qmin-eq-iff-1 qmin-eq-iff-2") THENA Auto)
   THEN (All (RWO "qmax-eq-iff qmin-eq-iff") THENA Auto)
   THEN Try (Complete (((RationalElim ⌜v12⌝⋅ ORELSE (Thin 5 THEN RationalElim ⌜v12⌝⋅))
                        THEN All QavgSimp
                        THEN SplitOrHyps
                        THEN Auto)))) }

1
1. v5 : ℚ
2. v12 : ℚ
3. v13 : ℚ
4. v14 : ℚ
5. qavg(v5;v12) = v13 ∈ ℚ
6. v12 = qavg(v13;v14) ∈ ℚ
7. v13 ≤ v14
8. ((v5 ≤ v13) ∧ ((v12 ≤ v14) ⇒ (v13 = v12 ∈ ℚ)) ∧ ((v14 ≤ v12) ⇒ (v13 = v14 ∈ ℚ)))
∨ ((((v5 ≤ v13) ⇒ (v14 = v13 ∈ ℚ)) ∧ ((v13 ≤ v5) ⇒ (v14 = v5 ∈ ℚ))) ∧ (v14 ≤ v12))
∨ ((v5 ≤ v13) ∧ (v14 ≤ v12))
9. ((v13 ≤ v5) ∧ ((v12 ≤ v14) ⇒ (v5 = v12 ∈ ℚ)) ∧ ((v14 ≤ v12) ⇒ (v5 = v14 ∈ ℚ)))
∨ ((((v5 ≤ v13) ⇒ (v12 = v13 ∈ ℚ)) ∧ ((v13 ≤ v5) ⇒ (v12 = v5 ∈ ℚ))) ∧ (v12 ≤ v14))
∨ ((v13 ≤ v5) ∧ (v12 ≤ v14))
⊢ ((v5 = v13 ∈ ℚ) ∧ (v12 = v13 ∈ ℚ)) ∨ ((v5 = v14 ∈ ℚ) ∧ (v12 = v14 ∈ ℚ)) ∨ ((v5 = v13 ∈ ℚ) ∧ (v12 = v14 ∈ ℚ))

2
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 ∈ ℚ))

---

Latex:

---

Latex:

1.  v13  :  \mBbbQ{}
2.  v14  :  \mBbbQ{}
3.  v11  :  \mBbbQ{}
4.  v12  :  \mBbbQ{}
5.  v9  :  \mBbbQ{}
6.  v10  :  \mBbbQ{}
7.  v7  :  \mBbbQ{}
8.  v8  :  \mBbbQ{}
9.  v5  :  \mBbbQ{}
10.  v6  :  \mBbbQ{}
11.  ((v11  =  v5)  \mwedge{}  (v12  =  v5))  \mvee{}  ((v11  =  v6)  \mwedge{}  (v12  =  v6))  \mvee{}  ((v11  =  v5)  \mwedge{}  (v12  =  v6))
12.  ((v7  =  v9)  \mwedge{}  (v8  =  v9))  \mvee{}  ((v7  =  v10)  \mwedge{}  (v8  =  v10))  \mvee{}  ((v7  =  v9)  \mwedge{}  (v8  =  v10))
13.  ((v7  =  v11)  \mwedge{}  (v8  =  qavg(v11;v12)))  \mvee{}  ((v7  =  qavg(v11;v12))  \mwedge{}  (v8  =  v12))
14.  ((v9  =  v13)  \mwedge{}  (v10  =  qavg(v13;v14)))  \mvee{}  ((v9  =  qavg(v13;v14))  \mwedge{}  (v10  =  v14))
15.  v13  \mleq{}  v14
16.  ((qmax(v13;v5)  =  v13)  \mwedge{}  (qmin(v14;v6)  =  v13))
\mvee{}  ((qmax(v13;v5)  =  v14)  \mwedge{}  (qmin(v14;v6)  =  v14))
\mvee{}  ((qmax(v13;v5)  =  v13)  \mwedge{}  (qmin(v14;v6)  =  v14))
17.  ((qmax(v13;v5)  =  v5)  \mwedge{}  (qmin(v14;v6)  =  v5))
\mvee{}  ((qmax(v13;v5)  =  v6)  \mwedge{}  (qmin(v14;v6)  =  v6))
\mvee{}  ((qmax(v13;v5)  =  v5)  \mwedge{}  (qmin(v14;v6)  =  v6))
\mvdash{}  ((v11  =  v13)  \mwedge{}  (v12  =  v13))  \mvee{}  ((v11  =  v14)  \mwedge{}  (v12  =  v14))  \mvee{}  ((v11  =  v13)  \mwedge{}  (v12  =  v14))


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))
  THEN  SplitOrHyps
  THEN  (ExRepD  THENA  Auto)
  THEN  RationalElim  \mkleeneopen{}v9\mkleeneclose{}\mcdot{}
  THEN  RationalElim  \mkleeneopen{}v8\mkleeneclose{}\mcdot{}
  THEN  RationalElim  \mkleeneopen{}v11\mkleeneclose{}\mcdot{}
  THEN  RationalElim  \mkleeneopen{}v10\mkleeneclose{}\mcdot{}
  THEN  All  QavgSimp
  THEN  (Try  ((RationalElim  \mkleeneopen{}v6\mkleeneclose{}\mcdot{}  THEN  All  QavgSimp))
              THEN  Try  ((RationalElim  \mkleeneopen{}v7\mkleeneclose{}\mcdot{}  THEN  All  QavgSimp))
              THEN  Try  ((RationalElim  \mkleeneopen{}v5\mkleeneclose{}\mcdot{}  THEN  All  QavgSimp)))
  THEN  Auto
  THEN  (All  (RWO  "qmax-eq-iff-1  qmax-eq-iff-2  qmin-eq-iff-1  qmin-eq-iff-2")  THENA  Auto)
  THEN  (All  (RWO  "qmax-eq-iff  qmin-eq-iff")  THENA  Auto)
  THEN  Try  (Complete  (((RationalElim  \mkleeneopen{}v12\mkleeneclose{}\mcdot{}  ORELSE  (Thin  5  THEN  RationalElim  \mkleeneopen{}v12\mkleeneclose{}\mcdot{}))
                                            THEN  All  QavgSimp
                                            THEN  SplitOrHyps
                                            THEN  Auto))))

---

Home Index