Theorem dig0

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

	Ref	Expression
Assertion	dig0	|- ( ( B e. NN /\ K e. ZZ ) -> ( K ( digit ` B ) 0 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		0e0icopnf	|- 0 e. ( 0 [,) +oo )
2		digval	|- ( ( B e. NN /\ K e. ZZ /\ 0 e. ( 0 [,) +oo ) ) -> ( K ( digit ` B ) 0 ) = ( ( |_ ` ( ( B ^ -u K ) x. 0 ) ) mod B ) )
3	1 2	mp3an3	|- ( ( B e. NN /\ K e. ZZ ) -> ( K ( digit ` B ) 0 ) = ( ( |_ ` ( ( B ^ -u K ) x. 0 ) ) mod B ) )
4		nncn	|- ( B e. NN -> B e. CC )
5	4	adantr	|- ( ( B e. NN /\ K e. ZZ ) -> B e. CC )
6		nnne0	|- ( B e. NN -> B =/= 0 )
7	6	adantr	|- ( ( B e. NN /\ K e. ZZ ) -> B =/= 0 )
8		znegcl	|- ( K e. ZZ -> -u K e. ZZ )
9	8	adantl	|- ( ( B e. NN /\ K e. ZZ ) -> -u K e. ZZ )
10	5 7 9	expclzd	|- ( ( B e. NN /\ K e. ZZ ) -> ( B ^ -u K ) e. CC )
11	10	mul01d	|- ( ( B e. NN /\ K e. ZZ ) -> ( ( B ^ -u K ) x. 0 ) = 0 )
12	11	fveq2d	|- ( ( B e. NN /\ K e. ZZ ) -> ( |_ ` ( ( B ^ -u K ) x. 0 ) ) = ( |_ ` 0 ) )
13		0zd	|- ( ( B e. NN /\ K e. ZZ ) -> 0 e. ZZ )
14		flid	|- ( 0 e. ZZ -> ( |_ ` 0 ) = 0 )
15	13 14	syl	|- ( ( B e. NN /\ K e. ZZ ) -> ( |_ ` 0 ) = 0 )
16	12 15	eqtrd	|- ( ( B e. NN /\ K e. ZZ ) -> ( |_ ` ( ( B ^ -u K ) x. 0 ) ) = 0 )
17	16	oveq1d	|- ( ( B e. NN /\ K e. ZZ ) -> ( ( |_ ` ( ( B ^ -u K ) x. 0 ) ) mod B ) = ( 0 mod B ) )
18		nnrp	|- ( B e. NN -> B e. RR+ )
19		0mod	|- ( B e. RR+ -> ( 0 mod B ) = 0 )
20	18 19	syl	|- ( B e. NN -> ( 0 mod B ) = 0 )
21	20	adantr	|- ( ( B e. NN /\ K e. ZZ ) -> ( 0 mod B ) = 0 )
22	17 21	eqtrd	|- ( ( B e. NN /\ K e. ZZ ) -> ( ( |_ ` ( ( B ^ -u K ) x. 0 ) ) mod B ) = 0 )
23	3 22	eqtrd	|- ( ( B e. NN /\ K e. ZZ ) -> ( K ( digit ` B ) 0 ) = 0 )