Metamath Proof Explorer

Theorem nn0digval

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

Proof

Step Hyp Ref Expression
1 nn0z ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℤ )
2 digval ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 𝐾 ( digit ‘ 𝐵 ) 𝑅 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑅 ) ) mod 𝐵 ) )
3 1 2 syl3an2 ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 𝐾 ( digit ‘ 𝐵 ) 𝑅 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑅 ) ) mod 𝐵 ) )
4 nncn ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
5 4 anim1i ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐵 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) )
6 expneg ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐵 ↑ - 𝐾 ) = ( 1 / ( 𝐵 ↑ 𝐾 ) ) )
7 5 6 syl ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐵 ↑ - 𝐾 ) = ( 1 / ( 𝐵 ↑ 𝐾 ) ) )
8 7 3adant3 ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 𝐵 ↑ - 𝐾 ) = ( 1 / ( 𝐵 ↑ 𝐾 ) ) )
9 8 oveq1d ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( ( 𝐵 ↑ - 𝐾 ) · 𝑅 ) = ( ( 1 / ( 𝐵 ↑ 𝐾 ) ) · 𝑅 ) )
10 elrege0 ⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) ↔ ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) )
11 recn ⊢ ( 𝑅 ∈ ℝ → 𝑅 ∈ ℂ )
12 11 adantr ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → 𝑅 ∈ ℂ )
13 10 12 sylbi ⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → 𝑅 ∈ ℂ )
14 13 3ad2ant3 ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → 𝑅 ∈ ℂ )
15 5 3adant3 ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 𝐵 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) )
16 expcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐵 ↑ 𝐾 ) ∈ ℂ )
17 15 16 syl ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 𝐵 ↑ 𝐾 ) ∈ ℂ )
18 4 3ad2ant1 ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → 𝐵 ∈ ℂ )
19 nnne0 ⊢ ( 𝐵 ∈ ℕ → 𝐵 ≠ 0 )
20 19 3ad2ant1 ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → 𝐵 ≠ 0 )
21 1 3ad2ant2 ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → 𝐾 ∈ ℤ )
22 18 20 21 expne0d ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 𝐵 ↑ 𝐾 ) ≠ 0 )
23 14 17 22 divrec2d ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 𝑅 / ( 𝐵 ↑ 𝐾 ) ) = ( ( 1 / ( 𝐵 ↑ 𝐾 ) ) · 𝑅 ) )
24 9 23 eqtr4d ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( ( 𝐵 ↑ - 𝐾 ) · 𝑅 ) = ( 𝑅 / ( 𝐵 ↑ 𝐾 ) ) )
25 24 fveq2d ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑅 ) ) = ( ⌊ ‘ ( 𝑅 / ( 𝐵 ↑ 𝐾 ) ) ) )
26 25 oveq1d ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑅 ) ) mod 𝐵 ) = ( ( ⌊ ‘ ( 𝑅 / ( 𝐵 ↑ 𝐾 ) ) ) mod 𝐵 ) )
27 3 26 eqtrd ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 𝐾 ( digit ‘ 𝐵 ) 𝑅 ) = ( ( ⌊ ‘ ( 𝑅 / ( 𝐵 ↑ 𝐾 ) ) ) mod 𝐵 ) )