---

Step * 1 2 1 2 1 1 of Lemma less-fast-fib

.....antecedent..... 
1. n : ℤ
2. 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 : ℕ
6. ∀b@0:ℕ
     {m:ℕ| 
      ∀k:ℕ
        (((a + b) = fib(k) ∈ ℤ)
        ⇒ ((k ≤ 0) ⇒ (b@0 = 0 ∈ ℤ))
        ⇒ (0 < k ⇒ (b@0 = fib(k - 1) ∈ ℤ))
        ⇒ (m = fib((n - 1) + k) ∈ ℕ))} 
7. m : ℕ
8. ∀k:ℕ
     (((a + b) = fib(k) ∈ ℤ)
     ⇒ ((k ≤ 0) ⇒ (a = 0 ∈ ℤ))
     ⇒ (0 < k ⇒ (a = fib(k - 1) ∈ ℤ))
     ⇒ (m = fib((n - 1) + k) ∈ ℕ))
9. k : ℕ
10. a = fib(k) ∈ ℤ
11. (k ≤ 0) ⇒ (b = 0 ∈ ℤ)
12. 0 < k ⇒ (b = fib(k - 1) ∈ ℤ)
⊢ (a + b) = fib(k + 1) ∈ ℤ
BY
{ TACTIC:CaseNat 0 `k' }

1
1. n : ℤ
2. 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 : ℕ
6. ∀b@0:ℕ
     {m:ℕ| 
      ∀k:ℕ
        (((a + b) = fib(k) ∈ ℤ)
        ⇒ ((k ≤ 0) ⇒ (b@0 = 0 ∈ ℤ))
        ⇒ (0 < k ⇒ (b@0 = fib(k - 1) ∈ ℤ))
        ⇒ (m = fib((n - 1) + k) ∈ ℕ))} 
7. m : ℕ
8. ∀k:ℕ
     (((a + b) = fib(k) ∈ ℤ)
     ⇒ ((k ≤ 0) ⇒ (a = 0 ∈ ℤ))
     ⇒ (0 < k ⇒ (a = fib(k - 1) ∈ ℤ))
     ⇒ (m = fib((n - 1) + k) ∈ ℕ))
9. k : ℕ
10. a = fib(k) ∈ ℤ
11. (k ≤ 0) ⇒ (b = 0 ∈ ℤ)
12. 0 < k ⇒ (b = fib(k - 1) ∈ ℤ)
13. k = 0 ∈ ℤ
⊢ (a + b) = fib(0 + 1) ∈ ℤ

2
1. n : ℤ
2. 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 : ℕ
6. ∀b@0:ℕ
     {m:ℕ| 
      ∀k:ℕ
        (((a + b) = fib(k) ∈ ℤ)
        ⇒ ((k ≤ 0) ⇒ (b@0 = 0 ∈ ℤ))
        ⇒ (0 < k ⇒ (b@0 = fib(k - 1) ∈ ℤ))
        ⇒ (m = fib((n - 1) + k) ∈ ℕ))} 
7. m : ℕ
8. ∀k:ℕ
     (((a + b) = fib(k) ∈ ℤ)
     ⇒ ((k ≤ 0) ⇒ (a = 0 ∈ ℤ))
     ⇒ (0 < k ⇒ (a = fib(k - 1) ∈ ℤ))
     ⇒ (m = fib((n - 1) + k) ∈ ℕ))
9. k : ℕ
10. a = fib(k) ∈ ℤ
11. (k ≤ 0) ⇒ (b = 0 ∈ ℤ)
12. 0 < k ⇒ (b = fib(k - 1) ∈ ℤ)
13. ¬(k = 0 ∈ ℤ)
⊢ (a + b) = fib(k + 1) ∈ ℤ

---

Latex:

---

Latex:
.....antecedent..... 
1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}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  -  1)  +  k)))\} 
4.  a  :  \mBbbN{}
5.  b  :  \mBbbN{}
6.  \mforall{}b@0:\mBbbN{}
          \{m:\mBbbN{}| 
            \mforall{}k:\mBbbN{}
                (((a  +  b)  =  fib(k))
                {}\mRightarrow{}  ((k  \mleq{}  0)  {}\mRightarrow{}  (b@0  =  0))
                {}\mRightarrow{}  (0  <  k  {}\mRightarrow{}  (b@0  =  fib(k  -  1)))
                {}\mRightarrow{}  (m  =  fib((n  -  1)  +  k)))\} 
7.  m  :  \mBbbN{}
8.  \mforall{}k:\mBbbN{}
          (((a  +  b)  =  fib(k))
          {}\mRightarrow{}  ((k  \mleq{}  0)  {}\mRightarrow{}  (a  =  0))
          {}\mRightarrow{}  (0  <  k  {}\mRightarrow{}  (a  =  fib(k  -  1)))
          {}\mRightarrow{}  (m  =  fib((n  -  1)  +  k)))
9.  k  :  \mBbbN{}
10.  a  =  fib(k)
11.  (k  \mleq{}  0)  {}\mRightarrow{}  (b  =  0)
12.  0  <  k  {}\mRightarrow{}  (b  =  fib(k  -  1))
\mvdash{}  (a  +  b)  =  fib(k  +  1)


By

---

Latex:
TACTIC:CaseNat  0  `k'

---

Home Index