---

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

.....assertion..... 
1. k : ℕ
2. a : ℚCube(k)
3. b : ℚCube(k)
4. c : ℚCube(k)
5. d : ℚCube(k)
6. e : ℚCube(k)
7. i : ℕk
8. a1 : ℚ
9. a2 : ℚ
10. b1 : ℚ
11. b2 : ℚ
12. c1 : ℚ
13. c2 : ℚ
14. d1 : ℚ
15. d2 : ℚ
16. e1 : ℚ
17. e2 : ℚ
18. ((b1 = e1 ∈ ℚ) ∧ (b2 = e1 ∈ ℚ)) ∨ ((b1 = e2 ∈ ℚ) ∧ (b2 = e2 ∈ ℚ)) ∨ ((b1 = e1 ∈ ℚ) ∧ (b2 = e2 ∈ ℚ))
19. ((d1 = c1 ∈ ℚ) ∧ (d2 = c1 ∈ ℚ)) ∨ ((d1 = c2 ∈ ℚ) ∧ (d2 = c2 ∈ ℚ)) ∨ ((d1 = c1 ∈ ℚ) ∧ (d2 = c2 ∈ ℚ))
20. ((d1 = b1 ∈ ℚ) ∧ (d2 = qavg(b1;b2) ∈ ℚ)) ∨ ((d1 = qavg(b1;b2) ∈ ℚ) ∧ (d2 = b2 ∈ ℚ))
21. ((c1 = a1 ∈ ℚ) ∧ (c2 = qavg(a1;a2) ∈ ℚ)) ∨ ((c1 = qavg(a1;a2) ∈ ℚ) ∧ (c2 = a2 ∈ ℚ))
22. a1 ≤ a2
23. e1 ≤ e2
⊢ (a1 ≤ e2) ∧ (e1 ≤ a2)
BY
{ (SplitOrHyps
   THEN ExRepD
   THEN Repeat (((RationalElim ⌜b1⌝⋅
                  ORELSE RationalElim ⌜b2⌝⋅
                  ORELSE RationalElim ⌜d1⌝⋅
                  ORELSE RationalElim ⌜d2⌝⋅
                  ORELSE RationalElim ⌜c1⌝⋅
                  ORELSE RationalElim ⌜c2⌝⋅
                  ORELSE RationalElim ⌜e1⌝⋅
                  ORELSE RationalElim ⌜e2⌝⋅)
                 THEN All QavgSimp
                 ))
   THEN Auto
   THEN Try (((RWO "13 13<" 0 THENM QavgSimp 0) THEN Auto))) }

---

Latex:

---

Latex:
.....assertion..... 
1.  k  :  \mBbbN{}
2.  a  :  \mBbbQ{}Cube(k)
3.  b  :  \mBbbQ{}Cube(k)
4.  c  :  \mBbbQ{}Cube(k)
5.  d  :  \mBbbQ{}Cube(k)
6.  e  :  \mBbbQ{}Cube(k)
7.  i  :  \mBbbN{}k
8.  a1  :  \mBbbQ{}
9.  a2  :  \mBbbQ{}
10.  b1  :  \mBbbQ{}
11.  b2  :  \mBbbQ{}
12.  c1  :  \mBbbQ{}
13.  c2  :  \mBbbQ{}
14.  d1  :  \mBbbQ{}
15.  d2  :  \mBbbQ{}
16.  e1  :  \mBbbQ{}
17.  e2  :  \mBbbQ{}
18.  ((b1  =  e1)  \mwedge{}  (b2  =  e1))  \mvee{}  ((b1  =  e2)  \mwedge{}  (b2  =  e2))  \mvee{}  ((b1  =  e1)  \mwedge{}  (b2  =  e2))
19.  ((d1  =  c1)  \mwedge{}  (d2  =  c1))  \mvee{}  ((d1  =  c2)  \mwedge{}  (d2  =  c2))  \mvee{}  ((d1  =  c1)  \mwedge{}  (d2  =  c2))
20.  ((d1  =  b1)  \mwedge{}  (d2  =  qavg(b1;b2)))  \mvee{}  ((d1  =  qavg(b1;b2))  \mwedge{}  (d2  =  b2))
21.  ((c1  =  a1)  \mwedge{}  (c2  =  qavg(a1;a2)))  \mvee{}  ((c1  =  qavg(a1;a2))  \mwedge{}  (c2  =  a2))
22.  a1  \mleq{}  a2
23.  e1  \mleq{}  e2
\mvdash{}  (a1  \mleq{}  e2)  \mwedge{}  (e1  \mleq{}  a2)


By

---

Latex:
(SplitOrHyps
  THEN  ExRepD
  THEN  Repeat  (((RationalElim  \mkleeneopen{}b1\mkleeneclose{}\mcdot{}
                                ORELSE  RationalElim  \mkleeneopen{}b2\mkleeneclose{}\mcdot{}
                                ORELSE  RationalElim  \mkleeneopen{}d1\mkleeneclose{}\mcdot{}
                                ORELSE  RationalElim  \mkleeneopen{}d2\mkleeneclose{}\mcdot{}
                                ORELSE  RationalElim  \mkleeneopen{}c1\mkleeneclose{}\mcdot{}
                                ORELSE  RationalElim  \mkleeneopen{}c2\mkleeneclose{}\mcdot{}
                                ORELSE  RationalElim  \mkleeneopen{}e1\mkleeneclose{}\mcdot{}
                                ORELSE  RationalElim  \mkleeneopen{}e2\mkleeneclose{}\mcdot{})
                              THEN  All  QavgSimp
                              ))
  THEN  Auto
  THEN  Try  (((RWO  "13  13<"  0  THENM  QavgSimp  0)  THEN  Auto)))

---

Home Index