Step * of Lemma less-fast-fib

n:ℕ{m:ℕfib(n) ∈ ℕ
BY
TACTIC:Assert ⌜∀n,a,b:ℕ.
                   {m:ℕ
                    ∀k:ℕ
                      ((a fib(k) ∈ ℤ)
                       ((k ≤ 0)  (b 0 ∈ ℤ))
                       (0 <  (b fib(k 1) ∈ ℤ))
                       (m fib(n k) ∈ ℕ))} ⌝
⋅ }

1
.....assertion..... 
n,a,b:ℕ.
  {m:ℕ
   ∀k:ℕ((a fib(k) ∈ ℤ ((k ≤ 0)  (b 0 ∈ ℤ))  (0 <  (b fib(k 1) ∈ ℤ))  (m fib(n k) ∈ ℕ))} 

2
1. ∀n,a,b:ℕ.
     {m:ℕ
      ∀k:ℕ((a fib(k) ∈ ℤ ((k ≤ 0)  (b 0 ∈ ℤ))  (0 <  (b fib(k 1) ∈ ℤ))  (m fib(n k) ∈ ℕ))} 
⊢ ∀n:ℕ{m:ℕfib(n) ∈ ℕ


Latex:


Latex:
\mforall{}n:\mBbbN{}.  \{m:\mBbbN{}|  m  =  fib(n)\} 


By


Latex:
TACTIC:Assert  \mkleeneopen{}\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)))\}  \mkleeneclose{}
\mcdot{}




Home Index