---

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


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))
15. (r(z)/r(d)) ∈ I
⊢ f(x) = g(x)
BY
{ ((Assert f(x) = f((r(z)/r(d))) BY
          (BackThruSomeHyp THEN Auto))
   THEN (Assert g(x) = g((r(z)/r(d))) BY
               (BackThruSomeHyp THEN Auto))
   THEN (Assert f((r(z)/r(d))) = g((r(z)/r(d))) BY
               (BackThruSomeHyp THEN Auto))) }

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))
15. (r(z)/r(d)) ∈ I
16. f(x) = f((r(z)/r(d)))
17. g(x) = g((r(z)/r(d)))
18. f((r(z)/r(d))) = g((r(z)/r(d)))
⊢ f(x) = g(x)

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  f(x)  =  f((r(z)/r(d)))  BY
                (BackThruSomeHyp  THEN  Auto))
  THEN  (Assert  g(x)  =  g((r(z)/r(d)))  BY
                          (BackThruSomeHyp  THEN  Auto))
  THEN  (Assert  f((r(z)/r(d)))  =  g((r(z)/r(d)))  BY
                          (BackThruSomeHyp  THEN  Auto)))

---

Home Index