---

Step * of Lemma weighted-mean-properties_wf

∀[I:Interval]. ∀[F:{x:ℝ| x ∈ I}  ⟶ {x:ℝ| x ∈ I}  ⟶ r:{r:ℝ| r0 ≤ r}  ⟶ {s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))}  ⟶ {x:ℝ| x ∈ \000CI} ].
  (weighted-mean-properties(I;F) ∈ ℙ)
BY
{ (ProveWfLemma
   THEN MemTypeCD
   THEN Auto
   THEN Try (((RWO "-1<" 0 THEN Auto) THEN nRNorm 0 THEN Auto THEN BLemma `rmul-is-positive` THEN Complete (Auto)))) }

1
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)

---

Latex:

---

Latex:
\mforall{}[I:Interval].  \mforall{}[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\}  ].
    (weighted-mean-properties(I;F)  \mmember{}  \mBbbP{})


By

---

Latex:
(ProveWfLemma
  THEN  MemTypeCD
  THEN  Auto
  THEN  Try  (((RWO  "-1<"  0  THEN  Auto)
                        THEN  nRNorm  0
                        THEN  Auto
                        THEN  BLemma  `rmul-is-positive`
                        THEN  Complete  (Auto))))

---

Home Index