Metamath Proof Explorer

Theorem fiblem

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

Ref Expression
Assertion fiblem ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) ) ↦ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) : ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) ⟶ ℕ0

Proof

Step Hyp Ref Expression
1 s2len ⊢ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) = 2
2 1 eqcomi ⊢ 2 = ( ♯ ‘ ⟨“ 0 1 ”⟩ )
3 2 fveq2i ⊢ ( ℤ≥ ‘ 2 ) = ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) )
4 3 imaeq2i ⊢ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) = ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) )
5 4 ineq2i ⊢ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) ) = ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) )
6 eqid ⊢ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) = ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) )
7 5 6 mpteq12i ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) ) ↦ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) = ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) ↦ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) )
8 elin ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) ↔ ( 𝑤 ∈ Word ℕ0 ∧ 𝑤 ∈ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) )
9 8 simplbi ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → 𝑤 ∈ Word ℕ0 )
10 wrdf ⊢ ( 𝑤 ∈ Word ℕ0 → 𝑤 : ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ⟶ ℕ0 )
11 9 10 syl ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → 𝑤 : ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ⟶ ℕ0 )
12 8 simprbi ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → 𝑤 ∈ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) )
13 hashf ⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
14 ffn ⊢ ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) → ♯ Fn V )
15 elpreima ⊢ ( ♯ Fn V → ( 𝑤 ∈ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ↔ ( 𝑤 ∈ V ∧ ( ♯ ‘ 𝑤 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) )
16 13 14 15 mp2b ⊢ ( 𝑤 ∈ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ↔ ( 𝑤 ∈ V ∧ ( ♯ ‘ 𝑤 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) )
17 12 16 sylib ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → ( 𝑤 ∈ V ∧ ( ♯ ‘ 𝑤 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) )
18 17 simprd ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) )
19 18 3 eleqtrrdi ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ( ℤ≥ ‘ 2 ) )
20 uznn0sub ⊢ ( ( ♯ ‘ 𝑤 ) ∈ ( ℤ≥ ‘ 2 ) → ( ( ♯ ‘ 𝑤 ) − 2 ) ∈ ℕ0 )
21 19 20 syl ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → ( ( ♯ ‘ 𝑤 ) − 2 ) ∈ ℕ0 )
22 1zzd ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → 1 ∈ ℤ )
23 1p1e2 ⊢ ( 1 + 1 ) = 2
24 23 fveq2i ⊢ ( ℤ≥ ‘ ( 1 + 1 ) ) = ( ℤ≥ ‘ 2 )
25 19 24 eleqtrrdi ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
26 peano2uzr ⊢ ( ( 1 ∈ ℤ ∧ ( ♯ ‘ 𝑤 ) ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ( ℤ≥ ‘ 1 ) )
27 22 25 26 syl2anc ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ( ℤ≥ ‘ 1 ) )
28 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
29 27 28 eleqtrrdi ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ℕ )
30 29 nnred ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ℝ )
31 2rp ⊢ 2 ∈ ℝ+
32 31 a1i ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → 2 ∈ ℝ+ )
33 30 32 ltsubrpd ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → ( ( ♯ ‘ 𝑤 ) − 2 ) < ( ♯ ‘ 𝑤 ) )
34 elfzo0 ⊢ ( ( ( ♯ ‘ 𝑤 ) − 2 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↔ ( ( ( ♯ ‘ 𝑤 ) − 2 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑤 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝑤 ) − 2 ) < ( ♯ ‘ 𝑤 ) ) )
35 21 29 33 34 syl3anbrc ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → ( ( ♯ ‘ 𝑤 ) − 2 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) )
36 11 35 ffvelrnd ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) ∈ ℕ0 )
37 fzo0end ⊢ ( ( ♯ ‘ 𝑤 ) ∈ ℕ → ( ( ♯ ‘ 𝑤 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) )
38 29 37 syl ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → ( ( ♯ ‘ 𝑤 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) )
39 11 38 ffvelrnd ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ∈ ℕ0 )
40 36 39 nn0addcld ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) → ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∈ ℕ0 )
41 7 40 fmpti ⊢ ( 𝑤 ∈ ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ 2 ) ) ) ↦ ( ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 2 ) ) + ( 𝑤 ‘ ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) : ( Word ℕ0 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ ⟨“ 0 1 ”⟩ ) ) ) ) ⟶ ℕ0