Metamath Proof Explorer

Theorem fib1

Description: Value of the Fibonacci sequence at index 1. (Contributed by Thierry Arnoux, 25-Apr-2019)

Ref Expression
Assertion fib1 
|- ( Fibci ` 1 ) = 1

Proof

Step Hyp Ref Expression
1 df-fib 
 |-  Fibci = ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) )
2 1 fveq1i 
 |-  ( Fibci ` 1 ) = ( ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) ` 1 )
3 nn0ex 
 |-  NN0 e. _V
4 3 a1i 
 |-  ( T. -> NN0 e. _V )
5 0nn0 
 |-  0 e. NN0
6 5 a1i 
 |-  ( T. -> 0 e. NN0 )
7 1nn0 
 |-  1 e. NN0
8 7 a1i 
 |-  ( T. -> 1 e. NN0 )
9 6 8 s2cld 
 |-  ( T. -> <" 0 1 "> e. Word NN0 )
10 eqid 
 |-  ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) = ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) )
11 fiblem 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) : ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) --> NN0
12 11 a1i 
 |-  ( T. -> ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) : ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) --> NN0 )
13 2nn 
 |-  2 e. NN
14 1lt2 
 |-  1 < 2
15 elfzo0 
 |-  ( 1 e. ( 0 ..^ 2 ) <-> ( 1 e. NN0 /\ 2 e. NN /\ 1 < 2 ) )
16 7 13 14 15 mpbir3an 
 |-  1 e. ( 0 ..^ 2 )
17 s2len 
 |-  ( # ` <" 0 1 "> ) = 2
18 17 oveq2i 
 |-  ( 0 ..^ ( # ` <" 0 1 "> ) ) = ( 0 ..^ 2 )
19 16 18 eleqtrri 
 |-  1 e. ( 0 ..^ ( # ` <" 0 1 "> ) )
20 19 a1i 
 |-  ( T. -> 1 e. ( 0 ..^ ( # ` <" 0 1 "> ) ) )
21 4 9 10 12 20 sseqfv1 
 |-  ( T. -> ( ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) ` 1 ) = ( <" 0 1 "> ` 1 ) )
22 21 mptru 
 |-  ( ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) ` 1 ) = ( <" 0 1 "> ` 1 )
23 s2fv1 
 |-  ( 1 e. NN0 -> ( <" 0 1 "> ` 1 ) = 1 )
24 7 23 ax-mp 
 |-  ( <" 0 1 "> ` 1 ) = 1
25 2 22 24 3eqtri 
 |-  ( Fibci ` 1 ) = 1