Metamath Proof Explorer

Theorem dig1

Description: All but one digits of 1 are 0. (Contributed by AV, 24-May-2020)

Ref Expression
Assertion dig1 
|- ( ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) -> ( K ( digit ` B ) 1 ) = if ( K = 0 , 1 , 0 ) )

Proof

Step Hyp Ref Expression
1 eluzelcn 
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. CC )
2 1 exp0d 
 |-  ( B e. ( ZZ>= ` 2 ) -> ( B ^ 0 ) = 1 )
3 2 eqcomd 
 |-  ( B e. ( ZZ>= ` 2 ) -> 1 = ( B ^ 0 ) )
4 3 ad2antrl 
 |-  ( ( 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> 1 = ( B ^ 0 ) )
5 4 oveq2d 
 |-  ( ( 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> ( K ( digit ` B ) 1 ) = ( K ( digit ` B ) ( B ^ 0 ) ) )
6 simprl 
 |-  ( ( 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> B e. ( ZZ>= ` 2 ) )
7 simpr 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) -> K e. ZZ )
8 7 anim2i 
 |-  ( ( 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> ( 0 <_ K /\ K e. ZZ ) )
9 8 ancomd 
 |-  ( ( 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> ( K e. ZZ /\ 0 <_ K ) )
10 elnn0z 
 |-  ( K e. NN0 <-> ( K e. ZZ /\ 0 <_ K ) )
11 9 10 sylibr 
 |-  ( ( 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> K e. NN0 )
12 0nn0 
 |-  0 e. NN0
13 12 a1i 
 |-  ( ( 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> 0 e. NN0 )
14 digexp 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ K e. NN0 /\ 0 e. NN0 ) -> ( K ( digit ` B ) ( B ^ 0 ) ) = if ( K = 0 , 1 , 0 ) )
15 6 11 13 14 syl3anc 
 |-  ( ( 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> ( K ( digit ` B ) ( B ^ 0 ) ) = if ( K = 0 , 1 , 0 ) )
16 5 15 eqtrd 
 |-  ( ( 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> ( K ( digit ` B ) 1 ) = if ( K = 0 , 1 , 0 ) )
17 eluz2nn 
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. NN )
18 17 ad2antrl 
 |-  ( ( -. 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> B e. NN )
19 simprr 
 |-  ( ( -. 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> K e. ZZ )
20 nn0ge0 
 |-  ( K e. NN0 -> 0 <_ K )
21 20 a1i 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) -> ( K e. NN0 -> 0 <_ K ) )
22 21 con3d 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) -> ( -. 0 <_ K -> -. K e. NN0 ) )
23 22 impcom 
 |-  ( ( -. 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> -. K e. NN0 )
24 19 23 eldifd 
 |-  ( ( -. 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> K e. ( ZZ \ NN0 ) )
25 1nn0 
 |-  1 e. NN0
26 25 a1i 
 |-  ( ( -. 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> 1 e. NN0 )
27 dignn0fr 
 |-  ( ( B e. NN /\ K e. ( ZZ \ NN0 ) /\ 1 e. NN0 ) -> ( K ( digit ` B ) 1 ) = 0 )
28 18 24 26 27 syl3anc 
 |-  ( ( -. 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> ( K ( digit ` B ) 1 ) = 0 )
29 0le0 
 |-  0 <_ 0
30 breq2 
 |-  ( K = 0 -> ( 0 <_ K <-> 0 <_ 0 ) )
31 29 30 mpbiri 
 |-  ( K = 0 -> 0 <_ K )
32 31 a1i 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) -> ( K = 0 -> 0 <_ K ) )
33 32 con3d 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) -> ( -. 0 <_ K -> -. K = 0 ) )
34 33 impcom 
 |-  ( ( -. 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> -. K = 0 )
35 34 iffalsed 
 |-  ( ( -. 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> if ( K = 0 , 1 , 0 ) = 0 )
36 28 35 eqtr4d 
 |-  ( ( -. 0 <_ K /\ ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) ) -> ( K ( digit ` B ) 1 ) = if ( K = 0 , 1 , 0 ) )
37 16 36 pm2.61ian 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ K e. ZZ ) -> ( K ( digit ` B ) 1 ) = if ( K = 0 , 1 , 0 ) )