---

Step * 1 1 of Lemma inhabited-intersection-half-cubes


1. v4 : ℚ
2. v5 : ℚ
3. v6 : ℚ
4. v7 : ℚ
5. v8 : ℚ
6. v9 : ℚ
7. v10 : ℚ
8. v11 : ℚ
9. ((v8 ≤ v9) ∧ (v8 ≤ v11)) ∧ (v10 ≤ v9) ∧ (v10 ≤ v11)
10. (((v8 = v4 ∈ ℚ) ∧ (v9 = qavg(v4;v5) ∈ ℚ)) ∨ ((v8 = qavg(v4;v5) ∈ ℚ) ∧ (v9 = v5 ∈ ℚ)))
∧ (((v10 = v6 ∈ ℚ) ∧ (v11 = qavg(v6;v7) ∈ ℚ)) ∨ ((v10 = qavg(v6;v7) ∈ ℚ) ∧ (v11 = v7 ∈ ℚ)))
⊢ ((v4 ≤ v5) ∧ (v4 ≤ v7)) ∧ (v6 ≤ v5) ∧ (v6 ≤ v7)
BY
{ (D -1
   THEN (SplitOrHyps THEN ExRepD)
   THEN ((Eliminate ⌜v8⌝⋅ THENA Auto) THEN ThinVar `v8')
   THEN ((Eliminate ⌜v9⌝⋅ THENA Auto) THEN ThinVar `v9')
   THEN ((Eliminate ⌜v10⌝⋅ THENA Auto) THEN ThinVar `v10')
   THEN ((Eliminate ⌜v11⌝⋅ THENA Auto) THEN ThinVar `v11')
   THEN ∀h:hyp. (RWO "qle-qavg-iff-1 qavg-qle-iff-1" h THENA Auto) 
   THEN Auto
   THEN Try ((RWO "-4< -4" 0 THEN Auto))
   THEN Unfold `qavg` -4
   THEN QMul ⌜2⌝ (-4)⋅) }

1
1. v6 : ℚ
2. v7 : ℚ
3. v5 : ℚ
4. v4 : ℚ
5. v4 ≤ v5
6. (v4 + v5) ≤ (v6 + v7)
7. v6 ≤ v5
8. v6 ≤ v7
9. v4 ≤ v5
⊢ v4 ≤ v7

2
1. v7 : ℚ
2. v6 : ℚ
3. v4 : ℚ
4. v5 : ℚ
5. v4 ≤ v5
6. v4 ≤ v7
7. (v6 + v7) ≤ (v4 + v5)
8. v6 ≤ v7
9. v4 ≤ v5
10. v4 ≤ v7
⊢ v6 ≤ v5

---

Latex:

---

Latex:

1.  v4  :  \mBbbQ{}
2.  v5  :  \mBbbQ{}
3.  v6  :  \mBbbQ{}
4.  v7  :  \mBbbQ{}
5.  v8  :  \mBbbQ{}
6.  v9  :  \mBbbQ{}
7.  v10  :  \mBbbQ{}
8.  v11  :  \mBbbQ{}
9.  ((v8  \mleq{}  v9)  \mwedge{}  (v8  \mleq{}  v11))  \mwedge{}  (v10  \mleq{}  v9)  \mwedge{}  (v10  \mleq{}  v11)
10.  (((v8  =  v4)  \mwedge{}  (v9  =  qavg(v4;v5)))  \mvee{}  ((v8  =  qavg(v4;v5))  \mwedge{}  (v9  =  v5)))
\mwedge{}  (((v10  =  v6)  \mwedge{}  (v11  =  qavg(v6;v7)))  \mvee{}  ((v10  =  qavg(v6;v7))  \mwedge{}  (v11  =  v7)))
\mvdash{}  ((v4  \mleq{}  v5)  \mwedge{}  (v4  \mleq{}  v7))  \mwedge{}  (v6  \mleq{}  v5)  \mwedge{}  (v6  \mleq{}  v7)


By

---

Latex:
(D  -1
  THEN  (SplitOrHyps  THEN  ExRepD)
  THEN  ((Eliminate  \mkleeneopen{}v8\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `v8')
  THEN  ((Eliminate  \mkleeneopen{}v9\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `v9')
  THEN  ((Eliminate  \mkleeneopen{}v10\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `v10')
  THEN  ((Eliminate  \mkleeneopen{}v11\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `v11')
  THEN  \mforall{}h:hyp.  (RWO  "qle-qavg-iff-1  qavg-qle-iff-1"  h  THENA  Auto) 
  THEN  Auto
  THEN  Try  ((RWO  "-4<  -4"  0  THEN  Auto))
  THEN  Unfold  `qavg`  -4
  THEN  QMul  \mkleeneopen{}2\mkleeneclose{}  (-4)\mcdot{})

---

Home Index