---

Step * of Lemma i-member-convex'

∀I:Interval. ∀a,b:ℝ.
  ((a ∈ I) ⇒ (b ∈ I) ⇒ (∀z:{z:ℝ| r0 < z} . ∀x,y:{z:ℝ| r0 ≤ z} .  (((x + y) = z) ⇒ (((x * a) + (y * b)/z) ∈ I))))
BY
{ (Auto THEN (InstLemma `i-member-convex` [⌜I⌝;⌜a⌝;⌜b⌝;⌜(x/z)⌝]⋅ THENA Auto)) }

1
.....antecedent..... 
1. I : Interval
2. a : ℝ
3. b : ℝ
4. a ∈ I
5. b ∈ I
6. z : {z:ℝ| r0 < z} 
7. x : {z:ℝ| r0 ≤ z} 
8. y : {z:ℝ| r0 ≤ z} 
9. (x + y) = z
⊢ r0 ≤ (x/z)

2
.....antecedent..... 
1. I : Interval
2. a : ℝ
3. b : ℝ
4. a ∈ I
5. b ∈ I
6. z : {z:ℝ| r0 < z} 
7. x : {z:ℝ| r0 ≤ z} 
8. y : {z:ℝ| r0 ≤ z} 
9. (x + y) = z
⊢ (x/z) ≤ r1

3
1. I : Interval
2. a : ℝ
3. b : ℝ
4. a ∈ I
5. b ∈ I
6. z : {z:ℝ| r0 < z} 
7. x : {z:ℝ| r0 ≤ z} 
8. y : {z:ℝ| r0 ≤ z} 
9. (x + y) = z
10. ((x/z) * a) + ((r1 - (x/z)) * b) ∈ I
⊢ ((x * a) + (y * b)/z) ∈ I

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}a,b:\mBbbR{}.
    ((a  \mmember{}  I)
    {}\mRightarrow{}  (b  \mmember{}  I)
    {}\mRightarrow{}  (\mforall{}z:\{z:\mBbbR{}|  r0  <  z\}  .  \mforall{}x,y:\{z:\mBbbR{}|  r0  \mleq{}  z\}  .    (((x  +  y)  =  z)  {}\mRightarrow{}  (((x  *  a)  +  (y  *  b)/z)  \mmember{}  I))))


By

---

Latex:
(Auto  THEN  (InstLemma  `i-member-convex`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}(x/z)\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index