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 ℤ ≥ ⟨“ 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 ⊢ . -1 ℤ ≥ 2 = . -1 ℤ ≥ ⟨“ 0 1 ”⟩
5 4 ineq2i ⊢ Word ℕ 0 ∩ . -1 ℤ ≥ 2 = Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩
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 ℤ ≥ ⟨“ 0 1 ”⟩ ⟼ w ⁡ w − 2 + w ⁡ w − 1
8 elin ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ ↔ w ∈ Word ℕ 0 ∧ w ∈ . -1 ℤ ≥ ⟨“ 0 1 ”⟩
9 8 simplbi ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → w ∈ Word ℕ 0
10 wrdf ⊢ w ∈ Word ℕ 0 → w : 0 ..^ w ⟶ ℕ 0
11 9 10 syl ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → w : 0 ..^ w ⟶ ℕ 0
12 8 simprbi ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → w ∈ . -1 ℤ ≥ ⟨“ 0 1 ”⟩
13 hashf ⊢ . : V ⟶ ℕ 0 ∪ +∞
14 ffn ⊢ . : V ⟶ ℕ 0 ∪ +∞ → . Fn V
15 elpreima ⊢ . Fn V → w ∈ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ ↔ w ∈ V ∧ w ∈ ℤ ≥ ⟨“ 0 1 ”⟩
16 13 14 15 mp2b ⊢ w ∈ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ ↔ w ∈ V ∧ w ∈ ℤ ≥ ⟨“ 0 1 ”⟩
17 12 16 sylib ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → w ∈ V ∧ w ∈ ℤ ≥ ⟨“ 0 1 ”⟩
18 17 simprd ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → w ∈ ℤ ≥ ⟨“ 0 1 ”⟩
19 18 3 eleqtrrdi ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → w ∈ ℤ ≥ 2
20 uznn0sub ⊢ w ∈ ℤ ≥ 2 → w − 2 ∈ ℕ 0
21 19 20 syl ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → w − 2 ∈ ℕ 0
22 1zzd ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → 1 ∈ ℤ
23 1p1e2 ⊢ 1 + 1 = 2
24 23 fveq2i ⊢ ℤ ≥ 1 + 1 = ℤ ≥ 2
25 19 24 eleqtrrdi ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → w ∈ ℤ ≥ 1 + 1
26 peano2uzr ⊢ 1 ∈ ℤ ∧ w ∈ ℤ ≥ 1 + 1 → w ∈ ℤ ≥ 1
27 22 25 26 syl2anc ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → w ∈ ℤ ≥ 1
28 nnuz ⊢ ℕ = ℤ ≥ 1
29 27 28 eleqtrrdi ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → w ∈ ℕ
30 29 nnred ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → w ∈ ℝ
31 2rp ⊢ 2 ∈ ℝ +
32 31 a1i ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → 2 ∈ ℝ +
33 30 32 ltsubrpd ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → 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 ℤ ≥ ⟨“ 0 1 ”⟩ → w − 2 ∈ 0 ..^ w
36 11 35 ffvelrnd ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → w ⁡ w − 2 ∈ ℕ 0
37 fzo0end ⊢ w ∈ ℕ → w − 1 ∈ 0 ..^ w
38 29 37 syl ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → w − 1 ∈ 0 ..^ w
39 11 38 ffvelrnd ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → w ⁡ w − 1 ∈ ℕ 0
40 36 39 nn0addcld ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ → 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 ℤ ≥ ⟨“ 0 1 ”⟩ ⟶ ℕ 0