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	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 0 ( digit ‘ 𝐵 ) 1 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		0z	⊢ 0 ∈ ℤ
2		dig1	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 0 ∈ ℤ ) → ( 0 ( digit ‘ 𝐵 ) 1 ) = if ( 0 = 0 , 1 , 0 ) )
3	1 2	mpan2	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 0 ( digit ‘ 𝐵 ) 1 ) = if ( 0 = 0 , 1 , 0 ) )
4		eqid	⊢ 0 = 0
5	4	iftruei	⊢ if ( 0 = 0 , 1 , 0 ) = 1
6	3 5	eqtrdi	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 0 ( digit ‘ 𝐵 ) 1 ) = 1 )