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 ) |