dig0

		Ref	Expression
	Assertion	dig0	$⊢ (B \in ℕ \land K \in ℤ) \to K digit (B) 0 = 0$

Step	Hyp	Ref	Expression
1		0e0icopnf	$⊢ 0 \in [0, +∞)$
2		digval	$⊢ (B \in ℕ \land K \in ℤ \land 0 \in [0, +∞)) \to K digit (B) 0 = ⌊B^{- K} \cdot 0⌋ \mod B$
3	1 2	mp3an3	$⊢ (B \in ℕ \land K \in ℤ) \to K digit (B) 0 = ⌊B^{- K} \cdot 0⌋ \mod B$
4		nncn	$⊢ B \in ℕ \to B \in ℂ$
5	4	adantr	$⊢ (B \in ℕ \land K \in ℤ) \to B \in ℂ$
6		nnne0	$⊢ B \in ℕ \to B \neq 0$
7	6	adantr	$⊢ (B \in ℕ \land K \in ℤ) \to B \neq 0$
8		znegcl	$⊢ K \in ℤ \to - K \in ℤ$
9	8	adantl	$⊢ (B \in ℕ \land K \in ℤ) \to - K \in ℤ$
10	5 7 9	expclzd	$⊢ (B \in ℕ \land K \in ℤ) \to B^{- K} \in ℂ$
11	10	mul01d	$⊢ (B \in ℕ \land K \in ℤ) \to B^{- K} \cdot 0 = 0$
12	11	fveq2d	$⊢ (B \in ℕ \land K \in ℤ) \to ⌊B^{- K} \cdot 0⌋ = ⌊0⌋$
13		0zd	$⊢ (B \in ℕ \land K \in ℤ) \to 0 \in ℤ$
14		flid	$⊢ 0 \in ℤ \to ⌊0⌋ = 0$
15	13 14	syl	$⊢ (B \in ℕ \land K \in ℤ) \to ⌊0⌋ = 0$
16	12 15	eqtrd	$⊢ (B \in ℕ \land K \in ℤ) \to ⌊B^{- K} \cdot 0⌋ = 0$
17	16	oveq1d	$⊢ (B \in ℕ \land K \in ℤ) \to ⌊B^{- K} \cdot 0⌋ \mod B = 0 \mod B$
18		nnrp	$⊢ B \in ℕ \to B \in ℝ^{+}$
19		0mod	$⊢ B \in ℝ^{+} \to 0 \mod B = 0$
20	18 19	syl	$⊢ B \in ℕ \to 0 \mod B = 0$
21	20	adantr	$⊢ (B \in ℕ \land K \in ℤ) \to 0 \mod B = 0$
22	17 21	eqtrd	$⊢ (B \in ℕ \land K \in ℤ) \to ⌊B^{- K} \cdot 0⌋ \mod B = 0$
23	3 22	eqtrd	$⊢ (B \in ℕ \land K \in ℤ) \to K digit (B) 0 = 0$

Metamath Proof Explorer