Metamath Proof Explorer


Theorem digvalnn0

Description: The K th digit of a nonnegative real number R in the positional system with base B is a nonnegative integer. (Contributed by AV, 28-May-2020)

Ref Expression
Assertion digvalnn0 ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 𝐾 ( digit ‘ 𝐵 ) 𝑅 ) ∈ ℕ0 )

Proof

Step Hyp Ref Expression
1 digval ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 𝐾 ( digit ‘ 𝐵 ) 𝑅 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑅 ) ) mod 𝐵 ) )
2 nnre ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
3 2 3ad2ant1 ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → 𝐵 ∈ ℝ )
4 nnne0 ( 𝐵 ∈ ℕ → 𝐵 ≠ 0 )
5 4 3ad2ant1 ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → 𝐵 ≠ 0 )
6 znegcl ( 𝐾 ∈ ℤ → - 𝐾 ∈ ℤ )
7 6 3ad2ant2 ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → - 𝐾 ∈ ℤ )
8 3 5 7 reexpclzd ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 𝐵 ↑ - 𝐾 ) ∈ ℝ )
9 elrege0 ( 𝑅 ∈ ( 0 [,) +∞ ) ↔ ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) )
10 9 simplbi ( 𝑅 ∈ ( 0 [,) +∞ ) → 𝑅 ∈ ℝ )
11 10 3ad2ant3 ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → 𝑅 ∈ ℝ )
12 8 11 remulcld ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( ( 𝐵 ↑ - 𝐾 ) · 𝑅 ) ∈ ℝ )
13 12 flcld ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑅 ) ) ∈ ℤ )
14 simp1 ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → 𝐵 ∈ ℕ )
15 13 14 zmodcld ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑅 ) ) mod 𝐵 ) ∈ ℕ0 )
16 1 15 eqeltrd ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ ( 0 [,) +∞ ) ) → ( 𝐾 ( digit ‘ 𝐵 ) 𝑅 ) ∈ ℕ0 )