---

Step * 1 1 1 1 1 1 1 1 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. n : ℕ+
5. 4 < |x| n
6. ∀k:ℕ. (fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k ∈ partial(ℤ))
7. d : ℤ
8. 0 < d
9. ∀k:ℕ
     (((k ≤ (n - 1)) ∧ ((n - 1) ≤ (k + (d - 1))))
     ⇒ ((fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k) = 1 ∈ partial(ℤ)))
10. k : ℕ
11. k ≤ (n - 1)
12. (n - 1) ≤ (k + d)
⊢ if 4 <z |x (k + 1)| then 1 else fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) (k + 1) fi  = 1 ∈ partial(ℤ\000C)
BY
{ AutoSplit }

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. n : ℕ+
5. 4 < |x| n
6. ∀k:ℕ. (fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k ∈ partial(ℤ))
7. d : ℤ
8. 0 < d
9. ∀k:ℕ
     (((k ≤ (n - 1)) ∧ ((n - 1) ≤ (k + (d - 1))))
     ⇒ ((fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k) = 1 ∈ partial(ℤ)))
10. k : ℕ
11. ¬4 < |x (k + 1)|
12. k ≤ (n - 1)
13. (n - 1) ≤ (k + d)
⊢ (fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) (k + 1)) = 1 ∈ partial(ℤ)

---

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.  n  :  \mBbbN{}\msupplus{}
5.  4  <  |x|  n
6.  \mforall{}k:\mBbbN{}.  (fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  k  \mmember{}  partial(\mBbbZ{}))
7.  d  :  \mBbbZ{}
8.  0  <  d
9.  \mforall{}k:\mBbbN{}
          (((k  \mleq{}  (n  -  1))  \mwedge{}  ((n  -  1)  \mleq{}  (k  +  (d  -  1))))
          {}\mRightarrow{}  ((fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  k)  =  1))
10.  k  :  \mBbbN{}
11.  k  \mleq{}  (n  -  1)
12.  (n  -  1)  \mleq{}  (k  +  d)
\mvdash{}  if  4  <z  |x  (k  +  1)|  then  1  else  fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  (k  +  1)\000C  fi 
=  1


By

---

Latex:
AutoSplit

---

Home Index