Theorem fib0

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

	Ref	Expression
Assertion	fib0	$$⊢\mathrm{Fibci}\left(0\right)=0$$

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(0\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(0\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		lbfzo0	$$⊢0\in \left(0..^2\right)\leftrightarrow 2\in \mathbb{N}$$
15	13 14	mpbir	$$⊢0\in \left(0..^2\right)$$
16		s2len	$$⊢\left|⟨“01”⟩\right|=2$$
17	16	oveq2i	$$⊢\left(0..^\left|⟨“01”⟩\right|\right)=\left(0..^2\right)$$
18	15 17	eleqtrri	$$⊢0\in \left(0..^\left|⟨“01”⟩\right|\right)$$
19	18	a1i	$$⊢\top \to 0\in \left(0..^\left|⟨“01”⟩\right|\right)$$
20	4 9 10 12 19	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(0\right)=⟨“01”⟩\left(0\right)$$
21	20	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(0\right)=⟨“01”⟩\left(0\right)$$
22		s2fv0	$$⊢0\in {\mathbb{N}}_0\to ⟨“01”⟩\left(0\right)=0$$
23	5 22	ax-mp	$$⊢⟨“01”⟩\left(0\right)=0$$
24	2 21 23	3eqtri	$$⊢\mathrm{Fibci}\left(0\right)=0$$