Step * of Lemma fast-fib

n:ℕ(∃m:ℕ [(m fib(n) ∈ ℕ)])
BY
xxxAssert ⌜∀n:ℕ. ∀a,b:ℤ.
               (∃c:ℤ [(∀m:ℕ
                         ((a fib(m 1) ∈ ℤ)
                          (b fib(m) ∈ ℤ)
                          (c if 0 ≤then fib(n m) else fib(m) fi  ∈ ℤ)))])⌝
xxx }

1
.....assertion..... 
n:ℕ. ∀a,b:ℤ.
  (∃c:ℤ [(∀m:ℕ((a fib(m 1) ∈ ℤ (b fib(m) ∈ ℤ (c if 0 ≤then fib(n m) else fib(m) fi  ∈ ℤ)))])

2
1. ∀n:ℕ. ∀a,b:ℤ.
     (∃c:ℤ [(∀m:ℕ((a fib(m 1) ∈ ℤ (b fib(m) ∈ ℤ (c if 0 ≤then fib(n m) else fib(m) fi  ∈ ℤ)))])
⊢ ∀n:ℕ(∃m:ℕ [(m fib(n) ∈ ℕ)])


Latex:


Latex:
\mforall{}n:\mBbbN{}.  (\mexists{}m:\mBbbN{}  [(m  =  fib(n))])


By


Latex:
xxxAssert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}a,b:\mBbbZ{}.
                          (\mexists{}c:\mBbbZ{}  [(\mforall{}m:\mBbbN{}
                                              ((a  =  fib(m  +  1))
                                              {}\mRightarrow{}  (b  =  fib(m))
                                              {}\mRightarrow{}  (c  =  if  0  \mleq{}z  n  then  fib(n  +  m)  else  fib(m)  fi  )))])\mkleeneclose{}
\mcdot{}xxx




Home Index