---

Step * 1 1 1 of Lemma Cauchy-equation-1-iff


1. f : ℝ ⟶ ℝ
2. ∀x,y:ℝ.  ((x = y) ⇒ ((f x) = (f y)))
3. ∀x,y:ℝ.  (f(x + y) = (f(x) + f(y)))
4. f(r0) = r0
5. ∀m:ℕ. ∀x:ℕm ⟶ ℝ.  (f(Σ{x[i] | 0≤i≤m - 1}) = Σ{f(x[i]) | 0≤i≤m - 1})
⊢ ∀x:ℝ. (f(x) = (x * f(r1)))
BY
{ ((Assert ∀m:ℕ. ∀x:ℝ.  (f(r(m) * x) = (r(m) * f(x))) BY
          (ParallelLast
           THEN (D 0 THENA Auto)
           THEN InstHyp [⌜λ2i.x⌝] (-2)⋅
           THEN Auto
           THEN (RWO "rsum-constant2" (-1) THENA Auto)
           THEN SplitOnHypITE -1 
           THEN Auto
           THEN Subst' (m - 1 - 0) + 1 ~ m -2
           THEN Auto
           THEN (Assert (r(m) * x) = (x * r(m)) BY
                       Auto)
           THEN RWW "-1 -3" 0
           THEN Auto
           THEN Subst' m ~ 0 0
           THEN Auto))
   THEN PromoteHyp (-1) 4
   THEN (Assert ∀n:ℕ+. ∀x:ℝ.  (f((x/r(n))) = (f(x)/r(n))) BY
               (Auto
                THEN (InstHyp [⌜n⌝;⌜(x/r(n))⌝] 4⋅ THENA Auto)
                THEN (nRNorm (-1) THENA Auto)
                THEN nRMul ⌜r(n)⌝ 0⋅
                THEN Auto))) }

1
1. f : ℝ ⟶ ℝ
2. ∀x,y:ℝ.  ((x = y) ⇒ ((f x) = (f y)))
3. ∀x,y:ℝ.  (f(x + y) = (f(x) + f(y)))
4. ∀m:ℕ. ∀x:ℝ.  (f(r(m) * x) = (r(m) * f(x)))
5. f(r0) = r0
6. ∀m:ℕ. ∀x:ℕm ⟶ ℝ.  (f(Σ{x[i] | 0≤i≤m - 1}) = Σ{f(x[i]) | 0≤i≤m - 1})
7. ∀n:ℕ+. ∀x:ℝ.  (f((x/r(n))) = (f(x)/r(n)))
⊢ ∀x:ℝ. (f(x) = (x * f(r1)))

---

Latex:

---

Latex:

1.  f  :  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}
2.  \mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y)))
3.  \mforall{}x,y:\mBbbR{}.    (f(x  +  y)  =  (f(x)  +  f(y)))
4.  f(r0)  =  r0
5.  \mforall{}m:\mBbbN{}.  \mforall{}x:\mBbbN{}m  {}\mrightarrow{}  \mBbbR{}.    (f(\mSigma{}\{x[i]  |  0\mleq{}i\mleq{}m  -  1\})  =  \mSigma{}\{f(x[i])  |  0\mleq{}i\mleq{}m  -  1\})
\mvdash{}  \mforall{}x:\mBbbR{}.  (f(x)  =  (x  *  f(r1)))


By

---

Latex:
((Assert  \mforall{}m:\mBbbN{}.  \mforall{}x:\mBbbR{}.    (f(r(m)  *  x)  =  (r(m)  *  f(x)))  BY
                (ParallelLast
                  THEN  (D  0  THENA  Auto)
                  THEN  InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}i.x\mkleeneclose{}]  (-2)\mcdot{}
                  THEN  Auto
                  THEN  (RWO  "rsum-constant2"  (-1)  THENA  Auto)
                  THEN  SplitOnHypITE  -1 
                  THEN  Auto
                  THEN  Subst'  (m  -  1  -  0)  +  1  \msim{}  m  -2
                  THEN  Auto
                  THEN  (Assert  (r(m)  *  x)  =  (x  *  r(m))  BY
                                          Auto)
                  THEN  RWW  "-1  -3"  0
                  THEN  Auto
                  THEN  Subst'  m  \msim{}  0  0
                  THEN  Auto))
  THEN  PromoteHyp  (-1)  4
  THEN  (Assert  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x:\mBbbR{}.    (f((x/r(n)))  =  (f(x)/r(n)))  BY
                          (Auto
                            THEN  (InstHyp  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}(x/r(n))\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
                            THEN  (nRNorm  (-1)  THENA  Auto)
                            THEN  nRMul  \mkleeneopen{}r(n)\mkleeneclose{}  0\mcdot{}
                            THEN  Auto)))

---

Home Index