Metamath Proof Explorer

Theorem fiblem

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

Ref Expression
Assertion fiblem ⊢w∈Wordℕ0∩.-1ℤ≥2⟼w⁡w−2+w⁡w−1:Wordℕ0∩.-1ℤ≥⟨“01”⟩⟶ℕ0

Proof

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