---

Step * 1 1 1 1 2 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. ∀x:ℝ. ((r0 < |x|) ⇒ ((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x ~ 1))
⊢ (∀x:ℝ. (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x)↓ ⇐⇒ r0 < |x|))
∧ (∀x:ℝ
     (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x)↓
     ⇒ (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x) = 1 ∈ ℤ)))
BY
{ BetterSplitAndConcl }

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. ∀x:ℝ. ((r0 < |x|) ⇒ ((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x ~ 1))
⊢ ∀x:ℝ. (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x)↓ ⇐⇒ r0 < |x|)

2
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. ∀x:ℝ. ((r0 < |x|) ⇒ ((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x ~ 1))
7. ∀x:ℝ. (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x)↓ ⇐⇒ r0 < |x|)
⊢ ∀x:ℝ
    (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x)↓
    ⇒ (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x) = 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.  \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.  \mforall{}x:\mBbbR{}.  ((r0  <  |x|)  {}\mRightarrow{}  ((\mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0))  x  \msim{}  1))
\mvdash{}  (\mforall{}x:\mBbbR{}.  (((\mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0))  x)\mdownarrow{}  \mLeftarrow{}{}\mRightarrow{}  r0  <  |x|))
\mwedge{}  (\mforall{}x:\mBbbR{}
          (((\mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0))  x)\mdownarrow{}
          {}\mRightarrow{}  (((\mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0))  x)  =  1)))


By

---

Latex:
BetterSplitAndConcl

---

Home Index