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	⊢ ( 𝐵 ∈ ℕ → ( digit ‘ 𝐵 ) = ( 𝑘 ∈ ℤ , 𝑟 ∈ ( 0 [,) +∞ ) ↦ ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-dig	⊢ digit = ( 𝑏 ∈ ℕ ↦ ( 𝑘 ∈ ℤ , 𝑟 ∈ ( 0 [,) +∞ ) ↦ ( ( ⌊ ‘ ( ( 𝑏 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝑏 ) ) )
2		oveq1	⊢ ( 𝑏 = 𝐵 → ( 𝑏 ↑ - 𝑘 ) = ( 𝐵 ↑ - 𝑘 ) )
3	2	fvoveq1d	⊢ ( 𝑏 = 𝐵 → ( ⌊ ‘ ( ( 𝑏 ↑ - 𝑘 ) · 𝑟 ) ) = ( ⌊ ‘ ( ( 𝐵 ↑ - 𝑘 ) · 𝑟 ) ) )
4		id	⊢ ( 𝑏 = 𝐵 → 𝑏 = 𝐵 )
5	3 4	oveq12d	⊢ ( 𝑏 = 𝐵 → ( ( ⌊ ‘ ( ( 𝑏 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝑏 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝐵 ) )
6	5	mpoeq3dv	⊢ ( 𝑏 = 𝐵 → ( 𝑘 ∈ ℤ , 𝑟 ∈ ( 0 [,) +∞ ) ↦ ( ( ⌊ ‘ ( ( 𝑏 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝑏 ) ) = ( 𝑘 ∈ ℤ , 𝑟 ∈ ( 0 [,) +∞ ) ↦ ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝐵 ) ) )
7		id	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℕ )
8		zex	⊢ ℤ ∈ V
9		ovex	⊢ ( 0 [,) +∞ ) ∈ V
10	8 9	pm3.2i	⊢ ( ℤ ∈ V ∧ ( 0 [,) +∞ ) ∈ V )
11		eqid	⊢ ( 𝑘 ∈ ℤ , 𝑟 ∈ ( 0 [,) +∞ ) ↦ ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝐵 ) ) = ( 𝑘 ∈ ℤ , 𝑟 ∈ ( 0 [,) +∞ ) ↦ ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝐵 ) )
12	11	mpoexg	⊢ ( ( ℤ ∈ V ∧ ( 0 [,) +∞ ) ∈ V ) → ( 𝑘 ∈ ℤ , 𝑟 ∈ ( 0 [,) +∞ ) ↦ ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝐵 ) ) ∈ V )
13	10 12	mp1i	⊢ ( 𝐵 ∈ ℕ → ( 𝑘 ∈ ℤ , 𝑟 ∈ ( 0 [,) +∞ ) ↦ ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝐵 ) ) ∈ V )
14	1 6 7 13	fvmptd3	⊢ ( 𝐵 ∈ ℕ → ( digit ‘ 𝐵 ) = ( 𝑘 ∈ ℤ , 𝑟 ∈ ( 0 [,) +∞ ) ↦ ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝐵 ) ) )