---

Step * 1 1 1 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. ∀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)))
8. ∀n:ℕ+. ∀m:ℕ.  (f((r(m)/r(n))) = ((r(m)/r(n)) * f(r1)))
9. ∀x:ℝ. (f(-(x)) = -(f(x)))
10. ∀n:ℕ+. ∀m:ℤ.  (f((r(m)/r(n))) = ((r(m)/r(n)) * f(r1)))
⊢ ∀x:ℝ. (f(x) = (x * f(r1)))
BY
{ ((InstLemma `functions-equal-on-rationals` [⌜(-∞, ∞)⌝;⌜f⌝;⌜λx.(x * f(r1))⌝]⋅
   THENM (ParallelLast THEN RepUR ``r-ap`` -1 THEN Fold `r-ap` (-1) THEN Auto)
   )
   THENA (Auto THEN Try ((InstConcl [⌜r0⌝;⌜r1⌝]⋅ THEN Auto)) THEN RepUR ``r-ap`` 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)))
8. ∀n:ℕ+. ∀m:ℕ.  (f((r(m)/r(n))) = ((r(m)/r(n)) * f(r1)))
9. ∀x:ℝ. (f(-(x)) = -(f(x)))
10. ∀n:ℕ+. ∀m:ℤ.  (f((r(m)/r(n))) = ((r(m)/r(n)) * f(r1)))
11. z : ℤ
12. d : ℕ+
13. (r(z)/r(d)) ∈ (-∞, ∞)
⊢ (f (r(z)/r(d))) = ((r(z)/r(d)) * 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.  \mforall{}m:\mBbbN{}.  \mforall{}x:\mBbbR{}.    (f(r(m)  *  x)  =  (r(m)  *  f(x)))
5.  f(r0)  =  r0
6.  \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\})
7.  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x:\mBbbR{}.    (f((x/r(n)))  =  (f(x)/r(n)))
8.  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}m:\mBbbN{}.    (f((r(m)/r(n)))  =  ((r(m)/r(n))  *  f(r1)))
9.  \mforall{}x:\mBbbR{}.  (f(-(x))  =  -(f(x)))
10.  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}m:\mBbbZ{}.    (f((r(m)/r(n)))  =  ((r(m)/r(n))  *  f(r1)))
\mvdash{}  \mforall{}x:\mBbbR{}.  (f(x)  =  (x  *  f(r1)))


By

---

Latex:
((InstLemma  `functions-equal-on-rationals`  [\mkleeneopen{}(-\minfty{},  \minfty{})\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(x  *  f(r1))\mkleeneclose{}]\mcdot{}
  THENM  (ParallelLast  THEN  RepUR  ``r-ap``  -1  THEN  Fold  `r-ap`  (-1)  THEN  Auto)
  )
  THENA  (Auto  THEN  Try  ((InstConcl  [\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}r1\mkleeneclose{}]\mcdot{}  THEN  Auto))  THEN  RepUR  ``r-ap``  0  THEN  Auto)
  )

---

Home Index