Theorem dig0

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

	Ref	Expression
Assertion	dig0	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ( digit ‘ 𝐵 ) 0 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		0e0icopnf	⊢ 0 ∈ ( 0 [,) +∞ )
2		digval	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 0 ∈ ( 0 [,) +∞ ) ) → ( 𝐾 ( digit ‘ 𝐵 ) 0 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 0 ) ) mod 𝐵 ) )
3	1 2	mp3an3	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ( digit ‘ 𝐵 ) 0 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 0 ) ) mod 𝐵 ) )
4		nncn	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
5	4	adantr	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → 𝐵 ∈ ℂ )
6		nnne0	⊢ ( 𝐵 ∈ ℕ → 𝐵 ≠ 0 )
7	6	adantr	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → 𝐵 ≠ 0 )
8		znegcl	⊢ ( 𝐾 ∈ ℤ → - 𝐾 ∈ ℤ )
9	8	adantl	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → - 𝐾 ∈ ℤ )
10	5 7 9	expclzd	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( 𝐵 ↑ - 𝐾 ) ∈ ℂ )
11	10	mul01d	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐵 ↑ - 𝐾 ) · 0 ) = 0 )
12	11	fveq2d	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 0 ) ) = ( ⌊ ‘ 0 ) )
13		0zd	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → 0 ∈ ℤ )
14		flid	⊢ ( 0 ∈ ℤ → ( ⌊ ‘ 0 ) = 0 )
15	13 14	syl	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ⌊ ‘ 0 ) = 0 )
16	12 15	eqtrd	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 0 ) ) = 0 )
17	16	oveq1d	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 0 ) ) mod 𝐵 ) = ( 0 mod 𝐵 ) )
18		nnrp	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ+ )
19		0mod	⊢ ( 𝐵 ∈ ℝ+ → ( 0 mod 𝐵 ) = 0 )
20	18 19	syl	⊢ ( 𝐵 ∈ ℕ → ( 0 mod 𝐵 ) = 0 )
21	20	adantr	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( 0 mod 𝐵 ) = 0 )
22	17 21	eqtrd	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 0 ) ) mod 𝐵 ) = 0 )
23	3 22	eqtrd	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ( digit ‘ 𝐵 ) 0 ) = 0 )