digval

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

		Ref	Expression
	Assertion	digval	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to K digit (B) R = ⌊B^{- K} R⌋ \mod B$

Step	Hyp	Ref	Expression
1		digfval	$⊢ B \in ℕ \to digit (B) = (k \in ℤ, r \in [0, +∞) ⟼ ⌊B^{- k} r⌋ \mod B)$
2	1	3ad2ant1	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to digit (B) = (k \in ℤ, r \in [0, +∞) ⟼ ⌊B^{- k} r⌋ \mod B)$
3		negeq	$⊢ k = K \to - k = - K$
4	3	oveq2d	$⊢ k = K \to B^{- k} = B^{- K}$
5	4	adantr	$⊢ (k = K \land r = R) \to B^{- k} = B^{- K}$
6		simpr	$⊢ (k = K \land r = R) \to r = R$
7	5 6	oveq12d	$⊢ (k = K \land r = R) \to B^{- k} r = B^{- K} R$
8	7	fveq2d	$⊢ (k = K \land r = R) \to ⌊B^{- k} r⌋ = ⌊B^{- K} R⌋$
9	8	oveq1d	$⊢ (k = K \land r = R) \to ⌊B^{- k} r⌋ \mod B = ⌊B^{- K} R⌋ \mod B$
10	9	adantl	$⊢ ((B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \land (k = K \land r = R)) \to ⌊B^{- k} r⌋ \mod B = ⌊B^{- K} R⌋ \mod B$
11		simp2	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to K \in ℤ$
12		simp3	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to R \in [0, +∞)$
13		ovexd	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to ⌊B^{- K} R⌋ \mod B \in V$
14	2 10 11 12 13	ovmpod	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to K digit (B) R = ⌊B^{- K} R⌋ \mod B$

Metamath Proof Explorer