Metamath Proof Explorer

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 e. ( ZZ>= ` 2 ) -> ( 0 ( digit ` B ) 1 ) = 1 )

Proof

Step Hyp Ref Expression
1 0z 
 |-  0 e. ZZ
2 dig1 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ 0 e. ZZ ) -> ( 0 ( digit ` B ) 1 ) = if ( 0 = 0 , 1 , 0 ) )
3 1 2 mpan2 
 |-  ( B e. ( ZZ>= ` 2 ) -> ( 0 ( digit ` B ) 1 ) = if ( 0 = 0 , 1 , 0 ) )
4 eqid 
 |-  0 = 0
5 4 iftruei 
 |-  if ( 0 = 0 , 1 , 0 ) = 1
6 3 5 eqtrdi 
 |-  ( B e. ( ZZ>= ` 2 ) -> ( 0 ( digit ` B ) 1 ) = 1 )