Theorem fib1

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

	Ref	Expression
Assertion	fib1	$$⊢\mathrm{Fibci}\left(1\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		df-fib	$$⊢\mathrm{Fibci}=⟨“01”⟩{\mathrm{seq}}_{str}\left(w\in \left(\mathrm{Word}{\mathbb{N}}_0\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge 2}\right]\right)⟼w\left(\left|w\right|-2\right)+w\left(\left|w\right|-1\right)\right)$$
2	1	fveq1i	$$⊢\mathrm{Fibci}\left(1\right)=\left(⟨“01”⟩{\mathrm{seq}}_{str}\left(w\in \left(\mathrm{Word}{\mathbb{N}}_0\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge 2}\right]\right)⟼w\left(\left|w\right|-2\right)+w\left(\left|w\right|-1\right)\right)\right)\left(1\right)$$
3		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
4	3	a1i	$$⊢\top \to {\mathbb{N}}_0\in \mathrm{V}$$
5		0nn0	$$⊢0\in {\mathbb{N}}_0$$
6	5	a1i	$$⊢\top \to 0\in {\mathbb{N}}_0$$
7		1nn0	$$⊢1\in {\mathbb{N}}_0$$
8	7	a1i	$$⊢\top \to 1\in {\mathbb{N}}_0$$
9	6 8	s2cld	$$⊢\top \to ⟨“01”⟩\in \mathrm{Word}{\mathbb{N}}_0$$
10		eqid	$$⊢\mathrm{Word}{\mathbb{N}}_0\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|⟨“01”⟩\right|}\right]=\mathrm{Word}{\mathbb{N}}_0\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|⟨“01”⟩\right|}\right]$$
11		fiblem	$$⊢\left(w\in \left(\mathrm{Word}{\mathbb{N}}_0\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge 2}\right]\right)⟼w\left(\left|w\right|-2\right)+w\left(\left|w\right|-1\right)\right):\mathrm{Word}{\mathbb{N}}_0\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|⟨“01”⟩\right|}\right]⟶{\mathbb{N}}_0$$
12	11	a1i	$$⊢\top \to \left(w\in \left(\mathrm{Word}{\mathbb{N}}_0\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge 2}\right]\right)⟼w\left(\left|w\right|-2\right)+w\left(\left|w\right|-1\right)\right):\mathrm{Word}{\mathbb{N}}_0\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|⟨“01”⟩\right|}\right]⟶{\mathbb{N}}_0$$
13		2nn	$$⊢2\in \mathbb{N}$$
14		1lt2	$$⊢1<2$$
15		elfzo0	$$⊢1\in \left(0..^2\right)\leftrightarrow \left(1\in {\mathbb{N}}_0\wedge 2\in \mathbb{N}\wedge 1<2\right)$$
16	7 13 14 15	mpbir3an	$$⊢1\in \left(0..^2\right)$$
17		s2len	$$⊢\left|⟨“01”⟩\right|=2$$
18	17	oveq2i	$$⊢\left(0..^\left|⟨“01”⟩\right|\right)=\left(0..^2\right)$$
19	16 18	eleqtrri	$$⊢1\in \left(0..^\left|⟨“01”⟩\right|\right)$$
20	19	a1i	$$⊢\top \to 1\in \left(0..^\left|⟨“01”⟩\right|\right)$$
21	4 9 10 12 20	sseqfv1	$$⊢\top \to \left(⟨“01”⟩{\mathrm{seq}}_{str}\left(w\in \left(\mathrm{Word}{\mathbb{N}}_0\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge 2}\right]\right)⟼w\left(\left|w\right|-2\right)+w\left(\left|w\right|-1\right)\right)\right)\left(1\right)=⟨“01”⟩\left(1\right)$$
22	21	mptru	$$⊢\left(⟨“01”⟩{\mathrm{seq}}_{str}\left(w\in \left(\mathrm{Word}{\mathbb{N}}_0\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge 2}\right]\right)⟼w\left(\left|w\right|-2\right)+w\left(\left|w\right|-1\right)\right)\right)\left(1\right)=⟨“01”⟩\left(1\right)$$
23		s2fv1	$$⊢1\in {\mathbb{N}}_0\to ⟨“01”⟩\left(1\right)=1$$
24	7 23	ax-mp	$$⊢⟨“01”⟩\left(1\right)=1$$
25	2 22 24	3eqtri	$$⊢\mathrm{Fibci}\left(1\right)=1$$