Metamath Proof Explorer

Theorem digvalnn0

Description: The K th digit of a nonnegative real number R in the positional system with base B is a nonnegative integer. (Contributed by AV, 28-May-2020)

		Ref	Expression
	Assertion	digvalnn0	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to K digit (B) R \in ℕ_{0}$

Proof

Step	Hyp	Ref	Expression
1		digval	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to K digit (B) R = ⌊B^{- K} R⌋ \mod B$
2		nnre	$⊢ B \in ℕ \to B \in ℝ$
3	2	3ad2ant1	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to B \in ℝ$
4		nnne0	$⊢ B \in ℕ \to B \neq 0$
5	4	3ad2ant1	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to B \neq 0$
6		znegcl	$⊢ K \in ℤ \to - K \in ℤ$
7	6	3ad2ant2	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to - K \in ℤ$
8	3 5 7	reexpclzd	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to B^{- K} \in ℝ$
9		elrege0	$⊢ R \in [0, +∞) \leftrightarrow (R \in ℝ \land 0 \leq R)$
10	9	simplbi	$⊢ R \in [0, +∞) \to R \in ℝ$
11	10	3ad2ant3	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to R \in ℝ$
12	8 11	remulcld	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to B^{- K} R \in ℝ$
13	12	flcld	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to ⌊B^{- K} R⌋ \in ℤ$
14		simp1	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to B \in ℕ$
15	13 14	zmodcld	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to ⌊B^{- K} R⌋ \mod B \in ℕ_{0}$
16	1 15	eqeltrd	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to K digit (B) R \in ℕ_{0}$