Metamath Proof Explorer

Theorem fibp1

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

Ref Expression
Assertion fibp1 
|- ( N e. NN -> ( Fibci ` ( N + 1 ) ) = ( ( Fibci ` ( N - 1 ) ) + ( Fibci ` N ) ) )

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 ` ( N + 1 ) ) = ( ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) ` ( N + 1 ) )
3 2 a1i 
 |-  ( N e. NN -> ( Fibci ` ( N + 1 ) ) = ( ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) ` ( N + 1 ) ) )
4 nn0ex 
 |-  NN0 e. _V
5 4 a1i 
 |-  ( N e. NN -> NN0 e. _V )
6 0nn0 
 |-  0 e. NN0
7 6 a1i 
 |-  ( N e. NN -> 0 e. NN0 )
8 1nn0 
 |-  1 e. NN0
9 8 a1i 
 |-  ( N e. NN -> 1 e. NN0 )
10 7 9 s2cld 
 |-  ( N e. NN -> <" 0 1 "> e. Word NN0 )
11 eqid 
 |-  ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) = ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) )
12 fiblem 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) : ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) --> NN0
13 12 a1i 
 |-  ( N e. NN -> ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) : ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) --> NN0 )
14 eluzp1p1 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( N + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
15 nnuz 
 |-  NN = ( ZZ>= ` 1 )
16 14 15 eleq2s 
 |-  ( N e. NN -> ( N + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
17 s2len 
 |-  ( # ` <" 0 1 "> ) = 2
18 1p1e2 
 |-  ( 1 + 1 ) = 2
19 17 18 eqtr4i 
 |-  ( # ` <" 0 1 "> ) = ( 1 + 1 )
20 19 fveq2i 
 |-  ( ZZ>= ` ( # ` <" 0 1 "> ) ) = ( ZZ>= ` ( 1 + 1 ) )
21 16 20 eleqtrrdi 
 |-  ( N e. NN -> ( N + 1 ) e. ( ZZ>= ` ( # ` <" 0 1 "> ) ) )
22 5 10 11 13 21 sseqp1 
 |-  ( N e. NN -> ( ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) ` ( N + 1 ) ) = ( ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ` ( ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) |` ( 0 ..^ ( N + 1 ) ) ) ) )
23 id 
 |-  ( w = t -> w = t )
24 fveq2 
 |-  ( w = t -> ( # ` w ) = ( # ` t ) )
25 24 oveq1d 
 |-  ( w = t -> ( ( # ` w ) - 2 ) = ( ( # ` t ) - 2 ) )
26 23 25 fveq12d 
 |-  ( w = t -> ( w ` ( ( # ` w ) - 2 ) ) = ( t ` ( ( # ` t ) - 2 ) ) )
27 24 oveq1d 
 |-  ( w = t -> ( ( # ` w ) - 1 ) = ( ( # ` t ) - 1 ) )
28 23 27 fveq12d 
 |-  ( w = t -> ( w ` ( ( # ` w ) - 1 ) ) = ( t ` ( ( # ` t ) - 1 ) ) )
29 26 28 oveq12d 
 |-  ( w = t -> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) = ( ( t ` ( ( # ` t ) - 2 ) ) + ( t ` ( ( # ` t ) - 1 ) ) ) )
30 29 cbvmptv 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) = ( t e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( t ` ( ( # ` t ) - 2 ) ) + ( t ` ( ( # ` t ) - 1 ) ) ) )
31 30 a1i 
 |-  ( N e. NN -> ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) = ( t e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( t ` ( ( # ` t ) - 2 ) ) + ( t ` ( ( # ` t ) - 1 ) ) ) ) )
32 simpr 
 |-  ( ( N e. NN /\ t = ( ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) |` ( 0 ..^ ( N + 1 ) ) ) ) -> t = ( ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) |` ( 0 ..^ ( N + 1 ) ) ) )
33 1 a1i 
 |-  ( ( N e. NN /\ t = ( ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) |` ( 0 ..^ ( N + 1 ) ) ) ) -> Fibci = ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) )
34 33 reseq1d 
 |-  ( ( N e. NN /\ t = ( ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) = ( ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) |` ( 0 ..^ ( N + 1 ) ) ) )
35 32 34 eqtr4d 
 |-  ( ( N e. NN /\ t = ( ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) |` ( 0 ..^ ( N + 1 ) ) ) ) -> t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) )
36 simpr 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) )
37 36 fveq2d 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( # ` t ) = ( # ` ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) )
38 5 10 11 13 sseqf 
 |-  ( N e. NN -> ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) : NN0 --> NN0 )
39 1 a1i 
 |-  ( N e. NN -> Fibci = ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) )
40 39 feq1d 
 |-  ( N e. NN -> ( Fibci : NN0 --> NN0 <-> ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) : NN0 --> NN0 ) )
41 38 40 mpbird 
 |-  ( N e. NN -> Fibci : NN0 --> NN0 )
42 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
43 42 9 nn0addcld 
 |-  ( N e. NN -> ( N + 1 ) e. NN0 )
44 5 41 43 subiwrdlen 
 |-  ( N e. NN -> ( # ` ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) = ( N + 1 ) )
45 44 adantr 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( # ` ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) = ( N + 1 ) )
46 37 45 eqtrd 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( # ` t ) = ( N + 1 ) )
47 46 oveq1d 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( ( # ` t ) - 2 ) = ( ( N + 1 ) - 2 ) )
48 nncn 
 |-  ( N e. NN -> N e. CC )
49 1cnd 
 |-  ( N e. NN -> 1 e. CC )
50 2cnd 
 |-  ( N e. NN -> 2 e. CC )
51 48 49 50 addsubassd 
 |-  ( N e. NN -> ( ( N + 1 ) - 2 ) = ( N + ( 1 - 2 ) ) )
52 48 50 49 subsub2d 
 |-  ( N e. NN -> ( N - ( 2 - 1 ) ) = ( N + ( 1 - 2 ) ) )
53 2m1e1 
 |-  ( 2 - 1 ) = 1
54 53 oveq2i 
 |-  ( N - ( 2 - 1 ) ) = ( N - 1 )
55 54 a1i 
 |-  ( N e. NN -> ( N - ( 2 - 1 ) ) = ( N - 1 ) )
56 51 52 55 3eqtr2d 
 |-  ( N e. NN -> ( ( N + 1 ) - 2 ) = ( N - 1 ) )
57 56 adantr 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( ( N + 1 ) - 2 ) = ( N - 1 ) )
58 47 57 eqtrd 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( ( # ` t ) - 2 ) = ( N - 1 ) )
59 58 fveq2d 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( t ` ( ( # ` t ) - 2 ) ) = ( t ` ( N - 1 ) ) )
60 36 fveq1d 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( t ` ( N - 1 ) ) = ( ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ` ( N - 1 ) ) )
61 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
62 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
63 nnre 
 |-  ( N e. NN -> N e. RR )
64 2re 
 |-  2 e. RR
65 64 a1i 
 |-  ( N e. NN -> 2 e. RR )
66 63 65 readdcld 
 |-  ( N e. NN -> ( N + 2 ) e. RR )
67 1red 
 |-  ( N e. NN -> 1 e. RR )
68 2rp 
 |-  2 e. RR+
69 68 a1i 
 |-  ( N e. NN -> 2 e. RR+ )
70 63 69 ltaddrpd 
 |-  ( N e. NN -> N < ( N + 2 ) )
71 63 66 67 70 ltsub1dd 
 |-  ( N e. NN -> ( N - 1 ) < ( ( N + 2 ) - 1 ) )
72 48 50 49 addsubassd 
 |-  ( N e. NN -> ( ( N + 2 ) - 1 ) = ( N + ( 2 - 1 ) ) )
73 53 oveq2i 
 |-  ( N + ( 2 - 1 ) ) = ( N + 1 )
74 72 73 eqtrdi 
 |-  ( N e. NN -> ( ( N + 2 ) - 1 ) = ( N + 1 ) )
75 71 74 breqtrd 
 |-  ( N e. NN -> ( N - 1 ) < ( N + 1 ) )
76 elfzo0 
 |-  ( ( N - 1 ) e. ( 0 ..^ ( N + 1 ) ) <-> ( ( N - 1 ) e. NN0 /\ ( N + 1 ) e. NN /\ ( N - 1 ) < ( N + 1 ) ) )
77 61 62 75 76 syl3anbrc 
 |-  ( N e. NN -> ( N - 1 ) e. ( 0 ..^ ( N + 1 ) ) )
78 77 adantr 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( N - 1 ) e. ( 0 ..^ ( N + 1 ) ) )
79 fvres 
 |-  ( ( N - 1 ) e. ( 0 ..^ ( N + 1 ) ) -> ( ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ` ( N - 1 ) ) = ( Fibci ` ( N - 1 ) ) )
80 78 79 syl 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ` ( N - 1 ) ) = ( Fibci ` ( N - 1 ) ) )
81 59 60 80 3eqtrd 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( t ` ( ( # ` t ) - 2 ) ) = ( Fibci ` ( N - 1 ) ) )
82 46 oveq1d 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( ( # ` t ) - 1 ) = ( ( N + 1 ) - 1 ) )
83 simpl 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> N e. NN )
84 83 nncnd 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> N e. CC )
85 1cnd 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> 1 e. CC )
86 84 85 pncand 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( ( N + 1 ) - 1 ) = N )
87 82 86 eqtrd 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( ( # ` t ) - 1 ) = N )
88 87 fveq2d 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( t ` ( ( # ` t ) - 1 ) ) = ( t ` N ) )
89 36 fveq1d 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( t ` N ) = ( ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ` N ) )
90 nn0fz0 
 |-  ( N e. NN0 <-> N e. ( 0 ... N ) )
91 42 90 sylib 
 |-  ( N e. NN -> N e. ( 0 ... N ) )
92 nnz 
 |-  ( N e. NN -> N e. ZZ )
93 fzval3 
 |-  ( N e. ZZ -> ( 0 ... N ) = ( 0 ..^ ( N + 1 ) ) )
94 92 93 syl 
 |-  ( N e. NN -> ( 0 ... N ) = ( 0 ..^ ( N + 1 ) ) )
95 91 94 eleqtrd 
 |-  ( N e. NN -> N e. ( 0 ..^ ( N + 1 ) ) )
96 95 adantr 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> N e. ( 0 ..^ ( N + 1 ) ) )
97 fvres 
 |-  ( N e. ( 0 ..^ ( N + 1 ) ) -> ( ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ` N ) = ( Fibci ` N ) )
98 96 97 syl 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ` N ) = ( Fibci ` N ) )
99 88 89 98 3eqtrd 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( t ` ( ( # ` t ) - 1 ) ) = ( Fibci ` N ) )
100 81 99 oveq12d 
 |-  ( ( N e. NN /\ t = ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( ( t ` ( ( # ` t ) - 2 ) ) + ( t ` ( ( # ` t ) - 1 ) ) ) = ( ( Fibci ` ( N - 1 ) ) + ( Fibci ` N ) ) )
101 35 100 syldan 
 |-  ( ( N e. NN /\ t = ( ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) |` ( 0 ..^ ( N + 1 ) ) ) ) -> ( ( t ` ( ( # ` t ) - 2 ) ) + ( t ` ( ( # ` t ) - 1 ) ) ) = ( ( Fibci ` ( N - 1 ) ) + ( Fibci ` N ) ) )
102 39 reseq1d 
 |-  ( N e. NN -> ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) = ( ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) |` ( 0 ..^ ( N + 1 ) ) ) )
103 5 41 43 subiwrd 
 |-  ( N e. NN -> ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) e. Word NN0 )
104 ovex 
 |-  ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) e. _V
105 1 104 eqeltri 
 |-  Fibci e. _V
106 105 resex 
 |-  ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) e. _V
107 106 a1i 
 |-  ( N e. NN -> ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) e. _V )
108 18 fveq2i 
 |-  ( ZZ>= ` ( 1 + 1 ) ) = ( ZZ>= ` 2 )
109 16 108 eleqtrdi 
 |-  ( N e. NN -> ( N + 1 ) e. ( ZZ>= ` 2 ) )
110 44 109 eqeltrd 
 |-  ( N e. NN -> ( # ` ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) e. ( ZZ>= ` 2 ) )
111 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
112 ffn 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> # Fn _V )
113 elpreima 
 |-  ( # Fn _V -> ( ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) e. ( `' # " ( ZZ>= ` 2 ) ) <-> ( ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) e. _V /\ ( # ` ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) e. ( ZZ>= ` 2 ) ) ) )
114 111 112 113 mp2b 
 |-  ( ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) e. ( `' # " ( ZZ>= ` 2 ) ) <-> ( ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) e. _V /\ ( # ` ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) ) e. ( ZZ>= ` 2 ) ) )
115 107 110 114 sylanbrc 
 |-  ( N e. NN -> ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) e. ( `' # " ( ZZ>= ` 2 ) ) )
116 103 115 elind 
 |-  ( N e. NN -> ( Fibci |` ( 0 ..^ ( N + 1 ) ) ) e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) )
117 102 116 eqeltrrd 
 |-  ( N e. NN -> ( ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) |` ( 0 ..^ ( N + 1 ) ) ) e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) )
118 ovex 
 |-  ( ( Fibci ` ( N - 1 ) ) + ( Fibci ` N ) ) e. _V
119 118 a1i 
 |-  ( N e. NN -> ( ( Fibci ` ( N - 1 ) ) + ( Fibci ` N ) ) e. _V )
120 31 101 117 119 fvmptd 
 |-  ( N e. NN -> ( ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ` ( ( <" 0 1 "> seqstr ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) ) |` ( 0 ..^ ( N + 1 ) ) ) ) = ( ( Fibci ` ( N - 1 ) ) + ( Fibci ` N ) ) )
121 3 22 120 3eqtrd 
 |-  ( N e. NN -> ( Fibci ` ( N + 1 ) ) = ( ( Fibci ` ( N - 1 ) ) + ( Fibci ` N ) ) )