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

Proof

Step	Hyp	Ref	Expression
1		digfval	⊢ ( 𝐵 ∈ ℕ → ( digit ‘ 𝐵 ) = ( 𝑘 ∈ ℤ , 𝑟 ∈ ( 0 [,) +∞ ) ↦ ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝐵 ) ) )
2	1	3ad2ant1	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( digit ‘ 𝐵 ) = ( 𝑘 ∈ ℤ , 𝑟 ∈ ( 0 [,) +∞ ) ↦ ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝐵 ) ) )
3		negeq	⊢ ( 𝑘 = 𝐾 → - 𝑘 = - 𝐾 )
4	3	oveq2d	⊢ ( 𝑘 = 𝐾 → ( 𝐵 ↑ - 𝑘 ) = ( 𝐵 ↑ - 𝐾 ) )
5	4	adantr	⊢ ( ( 𝑘 = 𝐾 ∧ 𝑟 = 𝑅 ) → ( 𝐵 ↑ - 𝑘 ) = ( 𝐵 ↑ - 𝐾 ) )
6		simpr	⊢ ( ( 𝑘 = 𝐾 ∧ 𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
7	5 6	oveq12d	⊢ ( ( 𝑘 = 𝐾 ∧ 𝑟 = 𝑅 ) → ( ( 𝐵 ↑ - 𝑘 ) · 𝑟 ) = ( ( 𝐵 ↑ - 𝐾 ) · 𝑅 ) )
8	7	fveq2d	⊢ ( ( 𝑘 = 𝐾 ∧ 𝑟 = 𝑅 ) → ( ⌊ ‘ ( ( 𝐵 ↑ - 𝑘 ) · 𝑟 ) ) = ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑅 ) ) )
9	8	oveq1d	⊢ ( ( 𝑘 = 𝐾 ∧ 𝑟 = 𝑅 ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝐵 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑅 ) ) mod 𝐵 ) )
10	9	adantl	⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑘 = 𝐾 ∧ 𝑟 = 𝑅 ) ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝑘 ) · 𝑟 ) ) mod 𝐵 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑅 ) ) mod 𝐵 ) )
11		simp2	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → 𝐾 ∈ ℤ )
12		simp3	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → 𝑅 ∈ ( 0 [,) +∞ ) )
13		ovexd	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑅 ) ) mod 𝐵 ) ∈ V )
14	2 10 11 12 13	ovmpod	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 𝐾 ( digit ‘ 𝐵 ) 𝑅 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑅 ) ) mod 𝐵 ) )