Theorem 0dig1

Description: The 0 th digit of 1 is 1 in any positional system. (Contributed by AV, 28-May-2020)

	Ref	Expression
Assertion	0dig1	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to 0\mathrm{digit}\left(B\right)1=1$$

Proof

Step	Hyp	Ref	Expression
1		0z	$$⊢0\in \mathbb{Z}$$
2		dig1	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge 0\in \mathbb{Z}\right)\to 0\mathrm{digit}\left(B\right)1=if\left(0=0,1,0\right)$$
3	1 2	mpan2	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to 0\mathrm{digit}\left(B\right)1=if\left(0=0,1,0\right)$$
4		eqid	$$⊢0=0$$
5	4	iftruei	$$⊢if\left(0=0,1,0\right)=1$$
6	3 5	eqtrdi	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to 0\mathrm{digit}\left(B\right)1=1$$