---

Step * 1 of Lemma less-fast-fib

.....assertion..... 
∀n,a,b:ℕ.
  {m:ℕ| 
   ∀k:ℕ. ((a = fib(k) ∈ ℤ) ⇒ ((k ≤ 0) ⇒ (b = 0 ∈ ℤ)) ⇒ (0 < k ⇒ (b = fib(k - 1) ∈ ℤ)) ⇒ (m = fib(n + k) ∈ ℕ))} 
BY
{ TACTIC:(InductionOnNat THEN Auto') }

1
1. a : ℕ
2. b : ℕ
⊢ {m:ℕ| 
   ∀k:ℕ. ((a = fib(k) ∈ ℤ) ⇒ ((k ≤ 0) ⇒ (b = 0 ∈ ℤ)) ⇒ (0 < k ⇒ (b = fib(k - 1) ∈ ℤ)) ⇒ (m = fib(0 + k) ∈ ℕ))} 

2
1. n : ℤ
2. [%1] : 0 < n
3. ∀a,b:ℕ.
     {m:ℕ| 
      ∀k:ℕ
        ((a = fib(k) ∈ ℤ)
        ⇒ ((k ≤ 0) ⇒ (b = 0 ∈ ℤ))
        ⇒ (0 < k ⇒ (b = fib(k - 1) ∈ ℤ))
        ⇒ (m = fib((n - 1) + k) ∈ ℕ))} 
4. a : ℕ
5. b : ℕ
⊢ {m:ℕ| 
   ∀k:ℕ. ((a = fib(k) ∈ ℤ) ⇒ ((k ≤ 0) ⇒ (b = 0 ∈ ℤ)) ⇒ (0 < k ⇒ (b = fib(k - 1) ∈ ℤ)) ⇒ (m = fib(n + k) ∈ ℕ))} 

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}n,a,b:\mBbbN{}.
    \{m:\mBbbN{}| 
      \mforall{}k:\mBbbN{}.  ((a  =  fib(k))  {}\mRightarrow{}  ((k  \mleq{}  0)  {}\mRightarrow{}  (b  =  0))  {}\mRightarrow{}  (0  <  k  {}\mRightarrow{}  (b  =  fib(k  -  1)))  {}\mRightarrow{}  (m  =  fib(n  +  k)))\} 


By

---

Latex:
TACTIC:(InductionOnNat  THEN  Auto')

---

Home Index