Theorem 0dig2pr01

Description: The integers 0 and 1 correspond to their last bit. (Contributed by AV, 28-May-2010)

	Ref	Expression
Assertion	0dig2pr01	$$⊢N\in \left\{0,1\right\}\to 0\mathrm{digit}\left(2\right)N=N$$

Proof

Step	Hyp	Ref	Expression
1		elpri	$$⊢N\in \left\{0,1\right\}\to \left(N=0\vee N=1\right)$$
2		2nn	$$⊢2\in \mathbb{N}$$
3		0z	$$⊢0\in \mathbb{Z}$$
4		dig0	$$⊢\left(2\in \mathbb{N}\wedge 0\in \mathbb{Z}\right)\to 0\mathrm{digit}\left(2\right)0=0$$
5	2 3 4	mp2an	$$⊢0\mathrm{digit}\left(2\right)0=0$$
6		oveq2	$$⊢N=0\to 0\mathrm{digit}\left(2\right)N=0\mathrm{digit}\left(2\right)0$$
7		id	$$⊢N=0\to N=0$$
8	5 6 7	3eqtr4a	$$⊢N=0\to 0\mathrm{digit}\left(2\right)N=N$$
9		2z	$$⊢2\in \mathbb{Z}$$
10		uzid	$$⊢2\in \mathbb{Z}\to 2\in {\mathbb{Z}}_{\ge 2}$$
11		0dig1	$$⊢2\in {\mathbb{Z}}_{\ge 2}\to 0\mathrm{digit}\left(2\right)1=1$$
12	9 10 11	mp2b	$$⊢0\mathrm{digit}\left(2\right)1=1$$
13		oveq2	$$⊢N=1\to 0\mathrm{digit}\left(2\right)N=0\mathrm{digit}\left(2\right)1$$
14		id	$$⊢N=1\to N=1$$
15	12 13 14	3eqtr4a	$$⊢N=1\to 0\mathrm{digit}\left(2\right)N=N$$
16	8 15	jaoi	$$⊢\left(N=0\vee N=1\right)\to 0\mathrm{digit}\left(2\right)N=N$$
17	1 16	syl	$$⊢N\in \left\{0,1\right\}\to 0\mathrm{digit}\left(2\right)N=N$$