Metamath Proof Explorer

Theorem fiblem

Description: Lemma for fib0 , fib1 and fibp1 . (Contributed by Thierry Arnoux, 25-Apr-2019)

Ref Expression
Assertion fiblem 
|- ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) : ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) --> NN0

Proof

Step Hyp Ref Expression
1 s2len 
 |-  ( # ` <" 0 1 "> ) = 2
2 1 eqcomi 
 |-  2 = ( # ` <" 0 1 "> )
3 2 fveq2i 
 |-  ( ZZ>= ` 2 ) = ( ZZ>= ` ( # ` <" 0 1 "> ) )
4 3 imaeq2i 
 |-  ( `' # " ( ZZ>= ` 2 ) ) = ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) )
5 4 ineq2i 
 |-  ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) = ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) )
6 eqid 
 |-  ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) = ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) )
7 5 6 mpteq12i 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) = ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) )
8 elin 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) <-> ( w e. Word NN0 /\ w e. ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) )
9 8 simplbi 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> w e. Word NN0 )
10 wrdf 
 |-  ( w e. Word NN0 -> w : ( 0 ..^ ( # ` w ) ) --> NN0 )
11 9 10 syl 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> w : ( 0 ..^ ( # ` w ) ) --> NN0 )
12 8 simprbi 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> w e. ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) )
13 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
14 ffn 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> # Fn _V )
15 elpreima 
 |-  ( # Fn _V -> ( w e. ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) <-> ( w e. _V /\ ( # ` w ) e. ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) )
16 13 14 15 mp2b 
 |-  ( w e. ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) <-> ( w e. _V /\ ( # ` w ) e. ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) )
17 12 16 sylib 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> ( w e. _V /\ ( # ` w ) e. ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) )
18 17 simprd 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> ( # ` w ) e. ( ZZ>= ` ( # ` <" 0 1 "> ) ) )
19 18 3 eleqtrrdi 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> ( # ` w ) e. ( ZZ>= ` 2 ) )
20 uznn0sub 
 |-  ( ( # ` w ) e. ( ZZ>= ` 2 ) -> ( ( # ` w ) - 2 ) e. NN0 )
21 19 20 syl 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> ( ( # ` w ) - 2 ) e. NN0 )
22 1zzd 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> 1 e. ZZ )
23 1p1e2 
 |-  ( 1 + 1 ) = 2
24 23 fveq2i 
 |-  ( ZZ>= ` ( 1 + 1 ) ) = ( ZZ>= ` 2 )
25 19 24 eleqtrrdi 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> ( # ` w ) e. ( ZZ>= ` ( 1 + 1 ) ) )
26 peano2uzr 
 |-  ( ( 1 e. ZZ /\ ( # ` w ) e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( # ` w ) e. ( ZZ>= ` 1 ) )
27 22 25 26 syl2anc 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> ( # ` w ) e. ( ZZ>= ` 1 ) )
28 nnuz 
 |-  NN = ( ZZ>= ` 1 )
29 27 28 eleqtrrdi 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> ( # ` w ) e. NN )
30 29 nnred 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> ( # ` w ) e. RR )
31 2rp 
 |-  2 e. RR+
32 31 a1i 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> 2 e. RR+ )
33 30 32 ltsubrpd 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> ( ( # ` w ) - 2 ) < ( # ` w ) )
34 elfzo0 
 |-  ( ( ( # ` w ) - 2 ) e. ( 0 ..^ ( # ` w ) ) <-> ( ( ( # ` w ) - 2 ) e. NN0 /\ ( # ` w ) e. NN /\ ( ( # ` w ) - 2 ) < ( # ` w ) ) )
35 21 29 33 34 syl3anbrc 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> ( ( # ` w ) - 2 ) e. ( 0 ..^ ( # ` w ) ) )
36 11 35 ffvelrnd 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> ( w ` ( ( # ` w ) - 2 ) ) e. NN0 )
37 fzo0end 
 |-  ( ( # ` w ) e. NN -> ( ( # ` w ) - 1 ) e. ( 0 ..^ ( # ` w ) ) )
38 29 37 syl 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> ( ( # ` w ) - 1 ) e. ( 0 ..^ ( # ` w ) ) )
39 11 38 ffvelrnd 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> ( w ` ( ( # ` w ) - 1 ) ) e. NN0 )
40 36 39 nn0addcld 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) -> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) e. NN0 )
41 7 40 fmpti 
 |-  ( w e. ( Word NN0 i^i ( `' # " ( ZZ>= ` 2 ) ) ) |-> ( ( w ` ( ( # ` w ) - 2 ) ) + ( w ` ( ( # ` w ) - 1 ) ) ) ) : ( Word NN0 i^i ( `' # " ( ZZ>= ` ( # ` <" 0 1 "> ) ) ) ) --> NN0