---

Step * 1 1 1 2 1 2 1 1 1 of Lemma partial-int-not-discrete


1. ∀k:ℕ. (λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k) ∈ ℝ ⟶ partial(ℤ))
2. λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0) ∈ ℝ ⟶ partial(ℤ)
3. x : ℝ
4. y : ℝ
5. x = y
6. v : ℝ ⟶ partial(ℤ)
7. (λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) = v ∈ (ℝ ⟶ partial(ℤ))
8. ∀x:ℝ. ((v x)↓ ⇐⇒ r0 < |x|)
9. ∀x:ℝ. ((v x)↓ ⇒ ((v x) = 1 ∈ ℤ))
10. uiff((v x)↓;(v y)↓)
11. (v x)↓
12. (v y)↓
⊢ (v x) = (v y) ∈ ℤ
BY
{ ((FHyp (-4) [-2] THENA Auto) THEN (FHyp (-5) [-2] THENA Auto)) }

1
1. ∀k:ℕ. (λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k) ∈ ℝ ⟶ partial(ℤ))
2. λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0) ∈ ℝ ⟶ partial(ℤ)
3. x : ℝ
4. y : ℝ
5. x = y
6. v : ℝ ⟶ partial(ℤ)
7. (λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) = v ∈ (ℝ ⟶ partial(ℤ))
8. ∀x:ℝ. ((v x)↓ ⇐⇒ r0 < |x|)
9. ∀x:ℝ. ((v x)↓ ⇒ ((v x) = 1 ∈ ℤ))
10. uiff((v x)↓;(v y)↓)
11. (v x)↓
12. (v y)↓
13. (v x) = 1 ∈ ℤ
14. (v y) = 1 ∈ ℤ
⊢ (v x) = (v y) ∈ ℤ

---

Latex:

---

Latex:

1.  \mforall{}k:\mBbbN{}.  (\mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  k)  \mmember{}  \mBbbR{}  {}\mrightarrow{}  partial(\mBbbZ{}))
2.  \mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0)  \mmember{}  \mBbbR{}  {}\mrightarrow{}  partial(\mBbbZ{})
3.  x  :  \mBbbR{}
4.  y  :  \mBbbR{}
5.  x  =  y
6.  v  :  \mBbbR{}  {}\mrightarrow{}  partial(\mBbbZ{})
7.  (\mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0))  =  v
8.  \mforall{}x:\mBbbR{}.  ((v  x)\mdownarrow{}  \mLeftarrow{}{}\mRightarrow{}  r0  <  |x|)
9.  \mforall{}x:\mBbbR{}.  ((v  x)\mdownarrow{}  {}\mRightarrow{}  ((v  x)  =  1))
10.  uiff((v  x)\mdownarrow{};(v  y)\mdownarrow{})
11.  (v  x)\mdownarrow{}
12.  (v  y)\mdownarrow{}
\mvdash{}  (v  x)  =  (v  y)


By

---

Latex:
((FHyp  (-4)  [-2]  THENA  Auto)  THEN  (FHyp  (-5)  [-2]  THENA  Auto))

---

Home Index