---

Step * 1 1 2 1 1 1 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. (fix((λf,n. if 4 <z |r0 (n + 1)| then 1 else f (n + 1) fi )) 0) = 1 ∈ partial(ℤ)
3. j : ℤ
4. j ≠ 0
5. 0 < j
6. ∀t:ℕ. (λf,n. if 4 <z |r0 (n + 1)| then 1 else f (n + 1) fi ^j - 1 ⊥ t ≤ ⊥)
7. t : ℕ
8. 4 < |r0 (t + 1)|
⊢ 1 ≤ ⊥
BY
{ (RepUR ``int-to-real`` -1 THEN (Subst' 2 * (t + 1) * 0 ~ 0 -1 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. (fix((λf,n. if 4 <z |r0 (n + 1)| then 1 else f (n + 1) fi )) 0) = 1 ∈ partial(ℤ)
3. j : ℤ
4. j ≠ 0
5. 0 < j
6. ∀t:ℕ. (λf,n. if 4 <z |r0 (n + 1)| then 1 else f (n + 1) fi ^j - 1 ⊥ t ≤ ⊥)
7. t : ℕ
8. 4 < |0|
⊢ 1 ≤ ⊥

---

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.  (fix((\mlambda{}f,n.  if  4  <z  |r0  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0)  =  1
3.  j  :  \mBbbZ{}
4.  j  \mneq{}  0
5.  0  <  j
6.  \mforall{}t:\mBbbN{}.  (\mlambda{}f,n.  if  4  <z  |r0  (n  +  1)|  then  1  else  f  (n  +  1)  fi  \^{}j  -  1  \mbot{}  t  \mleq{}  \mbot{})
7.  t  :  \mBbbN{}
8.  4  <  |r0  (t  +  1)|
\mvdash{}  1  \mleq{}  \mbot{}


By

---

Latex:
(RepUR  ``int-to-real``  -1  THEN  (Subst'  2  *  (t  +  1)  *  0  \msim{}  0  -1  THENA  Auto))

---

Home Index