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 ∈ ℕ → digit ⁡ B = k ∈ ℤ , r ∈ 0 +∞ ⟼ B − k ⁢ r mod B

Proof

Step Hyp Ref Expression
1 df-dig ⊢ digit = b ∈ ℕ ⟼ k ∈ ℤ , r ∈ 0 +∞ ⟼ b − k ⁢ r mod b
2 oveq1 ⊢ b = B → b − k = B − k
3 2 fvoveq1d ⊢ b = B → b − k ⁢ r = B − k ⁢ r
4 id ⊢ b = B → b = B
5 3 4 oveq12d ⊢ b = B → b − k ⁢ r mod b = B − k ⁢ r mod B
6 5 mpoeq3dv ⊢ b = B → k ∈ ℤ , r ∈ 0 +∞ ⟼ b − k ⁢ r mod b = k ∈ ℤ , r ∈ 0 +∞ ⟼ B − k ⁢ r mod B
7 id ⊢ B ∈ ℕ → B ∈ ℕ
8 zex ⊢ ℤ ∈ V
9 ovex ⊢ 0 +∞ ∈ V
10 8 9 pm3.2i ⊢ ℤ ∈ V ∧ 0 +∞ ∈ V
11 eqid ⊢ k ∈ ℤ , r ∈ 0 +∞ ⟼ B − k ⁢ r mod B = k ∈ ℤ , r ∈ 0 +∞ ⟼ B − k ⁢ r mod B
12 11 mpoexg ⊢ ℤ ∈ V ∧ 0 +∞ ∈ V → k ∈ ℤ , r ∈ 0 +∞ ⟼ B − k ⁢ r mod B ∈ V
13 10 12 mp1i ⊢ B ∈ ℕ → k ∈ ℤ , r ∈ 0 +∞ ⟼ B − k ⁢ r mod B ∈ V
14 1 6 7 13 fvmptd3 ⊢ B ∈ ℕ → digit ⁡ B = k ∈ ℤ , r ∈ 0 +∞ ⟼ B − k ⁢ r mod B