---

Step * 1 of Lemma weighted-mean-properties_wf


1. I : Interval
2. F : {x:ℝ| x ∈ I}  ⟶ {x:ℝ| x ∈ I}  ⟶ r:{r:ℝ| r0 ≤ r}  ⟶ {s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))}  ⟶ {x:ℝ| x ∈ I} 
3. ∀x:{x:ℝ| x ∈ I} . ∀r:{r:ℝ| r0 ≤ r} . ∀s:{s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))} .  ((F x x r s) = x)
4. ∀a:{a:ℝ| a ∈ I} . ∀b:{b:ℝ| (b ∈ I) ∧ (a < b)} . ∀r,s:{s:ℝ| r0 < s} .
     ((a = (F a b r1 r0)) ∧ ((F a b r1 r0) < (F a b r s)) ∧ ((F a b r s) < (F a b r0 r1)) ∧ ((F a b r0 r1) = b))
5. ∀a,b:{b:ℝ| b ∈ I} . ∀r:{r:ℝ| r0 < r} . ∀s:{s:ℝ| (r0 < s) ∧ (r0 < (r + s))} . ∀t:{t:ℝ| r0 < t} .
     ((F a b (r * t) (s * t)) = (F a b r s))
6. ∀x,y:{x:ℝ| x ∈ I} . ∀r:{r:ℝ| r0 ≤ r} . ∀s:{s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))} . ∀X,Y:{x:ℝ| x ∈ I} . ∀R:{R:ℝ| 
                                                                                                    (r0 ≤ R)
                                                                                                    ∧ (r0 < (r + R))} .
   ∀S:{S:ℝ| ((r0 ≤ S) ∧ (r0 < (s + S))) ∧ (r0 < (R + S))} .
     ((F (F x y r s) (F X Y R S) (r + s) (R + S)) = (F (F x X r R) (F y Y s S) (r + R) (s + S)))
7. ∀a:{a:ℝ| a ∈ I} . ∀b:{b:ℝ| (b ∈ I) ∧ (a < b)} . ∀r:{r:ℝ| r0 < r} . ∀s:{s:ℝ| r0 ≤ s} . ∀t:{t:ℝ| s < t} .
     ((F a b r s) < (F a b r t))
8. ∀x:ℝ. (x ∈ I ∈ Type)
9. x : ℝ
10. x ∈ I
11. ∀x:ℝ. (x ∈ I ∈ Type)
12. y : ℝ
13. y ∈ I
14. ∀z:ℝ. ((z ∈ I) ∧ (y < z) ∈ Type)
15. z : ℝ
16. z ∈ I
17. y < z
18. ∀r:ℝ. (r0 ≤ r ∈ Type)
19. r : ℝ
20. r0 ≤ r
21. ∀s:ℝ. (r0 < s ∈ Type)
22. s : ℝ
23. r0 < s
24. r0 ≤ s
⊢ r0 < (r + s)
BY
{ (RWO "-5" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  F  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
{}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  I\} 
{}\mrightarrow{}  r:\{r:\mBbbR{}|  r0  \mleq{}  r\} 
{}\mrightarrow{}  \{s:\mBbbR{}|  (r0  \mleq{}  s)  \mwedge{}  (r0  <  (r  +  s))\} 
{}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  I\} 
3.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  \mforall{}r:\{r:\mBbbR{}|  r0  \mleq{}  r\}  .  \mforall{}s:\{s:\mBbbR{}|  (r0  \mleq{}  s)  \mwedge{}  (r0  <  (r  +  s))\}  .    ((F  x  x  r  s)  =  x)
4.  \mforall{}a:\{a:\mBbbR{}|  a  \mmember{}  I\}  .  \mforall{}b:\{b:\mBbbR{}|  (b  \mmember{}  I)  \mwedge{}  (a  <  b)\}  .  \mforall{}r,s:\{s:\mBbbR{}|  r0  <  s\}  .
          ((a  =  (F  a  b  r1  r0))
          \mwedge{}  ((F  a  b  r1  r0)  <  (F  a  b  r  s))
          \mwedge{}  ((F  a  b  r  s)  <  (F  a  b  r0  r1))
          \mwedge{}  ((F  a  b  r0  r1)  =  b))
5.  \mforall{}a,b:\{b:\mBbbR{}|  b  \mmember{}  I\}  .  \mforall{}r:\{r:\mBbbR{}|  r0  <  r\}  .  \mforall{}s:\{s:\mBbbR{}|  (r0  <  s)  \mwedge{}  (r0  <  (r  +  s))\}  .  \mforall{}t:\{t:\mBbbR{}|  r0  <  t\}  .
          ((F  a  b  (r  *  t)  (s  *  t))  =  (F  a  b  r  s))
6.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  \mforall{}r:\{r:\mBbbR{}|  r0  \mleq{}  r\}  .  \mforall{}s:\{s:\mBbbR{}|  (r0  \mleq{}  s)  \mwedge{}  (r0  <  (r  +  s))\}  .  \mforall{}X,Y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .
      \mforall{}R:\{R:\mBbbR{}|  (r0  \mleq{}  R)  \mwedge{}  (r0  <  (r  +  R))\}  .  \mforall{}S:\{S:\mBbbR{}|  ((r0  \mleq{}  S)  \mwedge{}  (r0  <  (s  +  S)))  \mwedge{}  (r0  <  (R  +  S))\}  .
          ((F  (F  x  y  r  s)  (F  X  Y  R  S)  (r  +  s)  (R  +  S))  =  (F  (F  x  X  r  R)  (F  y  Y  s  S)  (r  +  R)  (s  +  S)))
7.  \mforall{}a:\{a:\mBbbR{}|  a  \mmember{}  I\}  .  \mforall{}b:\{b:\mBbbR{}|  (b  \mmember{}  I)  \mwedge{}  (a  <  b)\}  .  \mforall{}r:\{r:\mBbbR{}|  r0  <  r\}  .  \mforall{}s:\{s:\mBbbR{}|  r0  \mleq{}  s\}  .
      \mforall{}t:\{t:\mBbbR{}|  s  <  t\}  .
          ((F  a  b  r  s)  <  (F  a  b  r  t))
8.  \mforall{}x:\mBbbR{}.  (x  \mmember{}  I  \mmember{}  Type)
9.  x  :  \mBbbR{}
10.  x  \mmember{}  I
11.  \mforall{}x:\mBbbR{}.  (x  \mmember{}  I  \mmember{}  Type)
12.  y  :  \mBbbR{}
13.  y  \mmember{}  I
14.  \mforall{}z:\mBbbR{}.  ((z  \mmember{}  I)  \mwedge{}  (y  <  z)  \mmember{}  Type)
15.  z  :  \mBbbR{}
16.  z  \mmember{}  I
17.  y  <  z
18.  \mforall{}r:\mBbbR{}.  (r0  \mleq{}  r  \mmember{}  Type)
19.  r  :  \mBbbR{}
20.  r0  \mleq{}  r
21.  \mforall{}s:\mBbbR{}.  (r0  <  s  \mmember{}  Type)
22.  s  :  \mBbbR{}
23.  r0  <  s
24.  r0  \mleq{}  s
\mvdash{}  r0  <  (r  +  s)


By

---

Latex:
(RWO  "-5"  0  THEN  Auto)

---

Home Index