Metamath Proof Explorer

Theorem digfval

Description: Operation to obtain 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	digfval	$⊢ B \in ℕ \to digit (B) = (k \in ℤ, r \in [0, +∞) ⟼ ⌊B^{- k} r⌋ \mod B)$

Proof

Step	Hyp	Ref	Expression
1		df-dig	$⊢ digit = (b \in ℕ ⟼ (k \in ℤ, r \in [0, +∞) ⟼ ⌊b^{- k} r⌋ \mod b))$
2		oveq1	$⊢ b = B \to b^{- k} = B^{- k}$
3	2	fvoveq1d	$⊢ b = B \to ⌊b^{- k} r⌋ = ⌊B^{- k} r⌋$
4		id	$⊢ b = B \to b = B$
5	3 4	oveq12d	$⊢ b = B \to ⌊b^{- k} r⌋ \mod b = ⌊B^{- k} r⌋ \mod B$
6	5	mpoeq3dv	$⊢ b = B \to (k \in ℤ, r \in [0, +∞) ⟼ ⌊b^{- k} r⌋ \mod b) = (k \in ℤ, r \in [0, +∞) ⟼ ⌊B^{- k} r⌋ \mod B)$
7		id	$⊢ B \in ℕ \to B \in ℕ$
8		zex	$⊢ ℤ \in V$
9		ovex	$⊢ [0, +∞) \in V$
10	8 9	pm3.2i	$⊢ (ℤ \in V \land [0, +∞) \in V)$
11		eqid	$⊢ (k \in ℤ, r \in [0, +∞) ⟼ ⌊B^{- k} r⌋ \mod B) = (k \in ℤ, r \in [0, +∞) ⟼ ⌊B^{- k} r⌋ \mod B)$
12	11	mpoexg	$⊢ (ℤ \in V \land [0, +∞) \in V) \to (k \in ℤ, r \in [0, +∞) ⟼ ⌊B^{- k} r⌋ \mod B) \in V$
13	10 12	mp1i	$⊢ B \in ℕ \to (k \in ℤ, r \in [0, +∞) ⟼ ⌊B^{- k} r⌋ \mod B) \in V$
14	1 6 7 13	fvmptd3	$⊢ B \in ℕ \to digit (B) = (k \in ℤ, r \in [0, +∞) ⟼ ⌊B^{- k} r⌋ \mod B)$