---

Step * 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)))
⊢ ∀x:ℝ. (f(x) = (x * f(r1)))
BY
{ ((Assert f(r0) = r0 BY
          ((InstHyp [⌜r0⌝;⌜r0⌝] (-1)⋅ THENA Auto) THEN nRNorm (-1) THEN nRAdd ⌜-(f(r0))⌝ (-1)⋅ THEN Auto))
   THEN (Assert ∀m:ℕ. ∀x:ℕm ⟶ ℝ.  (f(Σ{x[i] | 0≤i≤m - 1}) = Σ{f(x[i]) | 0≤i≤m - 1}) BY
               (InductionOnNat
                THEN Auto
                THEN (RWO "rsum_unroll" 0 THENA Auto)
                THEN RepeatFor 2 (AutoSplit)
                THEN RWW "3 -2" 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. 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)))

---

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)))
\mvdash{}  \mforall{}x:\mBbbR{}.  (f(x)  =  (x  *  f(r1)))


By

---

Latex:
((Assert  f(r0)  =  r0  BY
                ((InstHyp  [\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}r0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                  THEN  nRNorm  (-1)
                  THEN  nRAdd  \mkleeneopen{}-(f(r0))\mkleeneclose{}  (-1)\mcdot{}
                  THEN  Auto))
  THEN  (Assert  \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\})  BY
                          (InductionOnNat
                            THEN  Auto
                            THEN  (RWO  "rsum\_unroll"  0  THENA  Auto)
                            THEN  RepeatFor  2  (AutoSplit)
                            THEN  RWW  "3  -2"  0
                            THEN  Auto))
  )

---

Home Index