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 )