---

Step * 1 of Lemma functions-equal-on-rationals


1. I : Interval
2. ∃u,v:{a:ℝ| a ∈ I} . u ≠ v
3. f : I ⟶ℝ
4. g : I ⟶ℝ
5. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f(x) = f(y)))
6. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g(x) = g(y)))
7. ∀z:ℤ. ∀d:ℕ+.  (((r(z)/r(d)) ∈ I) ⇒ (f((r(z)/r(d))) = g((r(z)/r(d)))))
8. a : {x:ℝ| x ∈ I} 
9. x : {x:ℝ| x ∈ I} 
10. (λr.∃z:ℤ. ∃d:ℕ+. (r = (r(z)/r(d)))) x
⊢ f(x) = g(x)
BY
{ (Reduce -1 THEN ExRepD) }

1
1. I : Interval
2. u : {a:ℝ| a ∈ I} 
3. v : {a:ℝ| a ∈ I} 
4. u ≠ v
5. f : I ⟶ℝ
6. g : I ⟶ℝ
7. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f(x) = f(y)))
8. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g(x) = g(y)))
9. ∀z:ℤ. ∀d:ℕ+.  (((r(z)/r(d)) ∈ I) ⇒ (f((r(z)/r(d))) = g((r(z)/r(d)))))
10. a : {x:ℝ| x ∈ I} 
11. x : {x:ℝ| x ∈ I} 
12. z : ℤ
13. d : ℕ+
14. x = (r(z)/r(d))
⊢ f(x) = g(x)

---

Latex:

---

Latex:

1.  I  :  Interval
2.  \mexists{}u,v:\{a:\mBbbR{}|  a  \mmember{}  I\}  .  u  \mneq{}  v
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  g  :  I  {}\mrightarrow{}\mBbbR{}
5.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y)))
6.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (g(x)  =  g(y)))
7.  \mforall{}z:\mBbbZ{}.  \mforall{}d:\mBbbN{}\msupplus{}.    (((r(z)/r(d))  \mmember{}  I)  {}\mRightarrow{}  (f((r(z)/r(d)))  =  g((r(z)/r(d)))))
8.  a  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
9.  x  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
10.  (\mlambda{}r.\mexists{}z:\mBbbZ{}.  \mexists{}d:\mBbbN{}\msupplus{}.  (r  =  (r(z)/r(d))))  x
\mvdash{}  f(x)  =  g(x)


By

---

Latex:
(Reduce  -1  THEN  ExRepD)

---

Home Index