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	$⊢ (B \in ℕ \land K \in ℕ_{0} \land R \in [0, +∞)) \to K digit (B) R = ⌊\frac{R}{B^{K}}⌋ \mod B$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$⊢ K \in ℕ_{0} \to K \in ℤ$
2		digval	$⊢ (B \in ℕ \land K \in ℤ \land R \in [0, +∞)) \to K digit (B) R = ⌊B^{- K} R⌋ \mod B$
3	1 2	syl3an2	$⊢ (B \in ℕ \land K \in ℕ_{0} \land R \in [0, +∞)) \to K digit (B) R = ⌊B^{- K} R⌋ \mod B$
4		nncn	$⊢ B \in ℕ \to B \in ℂ$
5	4	anim1i	$⊢ (B \in ℕ \land K \in ℕ_{0}) \to (B \in ℂ \land K \in ℕ_{0})$
6		expneg	$⊢ (B \in ℂ \land K \in ℕ_{0}) \to B^{- K} = \frac{1}{B^{K}}$
7	5 6	syl	$⊢ (B \in ℕ \land K \in ℕ_{0}) \to B^{- K} = \frac{1}{B^{K}}$
8	7	3adant3	$⊢ (B \in ℕ \land K \in ℕ_{0} \land R \in [0, +∞)) \to B^{- K} = \frac{1}{B^{K}}$
9	8	oveq1d	$⊢ (B \in ℕ \land K \in ℕ_{0} \land R \in [0, +∞)) \to B^{- K} R = (\frac{1}{B^{K}}) R$
10		elrege0	$⊢ R \in [0, +∞) \leftrightarrow (R \in ℝ \land 0 \leq R)$
11		recn	$⊢ R \in ℝ \to R \in ℂ$
12	11	adantr	$⊢ (R \in ℝ \land 0 \leq R) \to R \in ℂ$
13	10 12	sylbi	$⊢ R \in [0, +∞) \to R \in ℂ$
14	13	3ad2ant3	$⊢ (B \in ℕ \land K \in ℕ_{0} \land R \in [0, +∞)) \to R \in ℂ$
15	5	3adant3	$⊢ (B \in ℕ \land K \in ℕ_{0} \land R \in [0, +∞)) \to (B \in ℂ \land K \in ℕ_{0})$
16		expcl	$⊢ (B \in ℂ \land K \in ℕ_{0}) \to B^{K} \in ℂ$
17	15 16	syl	$⊢ (B \in ℕ \land K \in ℕ_{0} \land R \in [0, +∞)) \to B^{K} \in ℂ$
18	4	3ad2ant1	$⊢ (B \in ℕ \land K \in ℕ_{0} \land R \in [0, +∞)) \to B \in ℂ$
19		nnne0	$⊢ B \in ℕ \to B \neq 0$
20	19	3ad2ant1	$⊢ (B \in ℕ \land K \in ℕ_{0} \land R \in [0, +∞)) \to B \neq 0$
21	1	3ad2ant2	$⊢ (B \in ℕ \land K \in ℕ_{0} \land R \in [0, +∞)) \to K \in ℤ$
22	18 20 21	expne0d	$⊢ (B \in ℕ \land K \in ℕ_{0} \land R \in [0, +∞)) \to B^{K} \neq 0$
23	14 17 22	divrec2d	$⊢ (B \in ℕ \land K \in ℕ_{0} \land R \in [0, +∞)) \to \frac{R}{B^{K}} = (\frac{1}{B^{K}}) R$
24	9 23	eqtr4d	$⊢ (B \in ℕ \land K \in ℕ_{0} \land R \in [0, +∞)) \to B^{- K} R = \frac{R}{B^{K}}$
25	24	fveq2d	$⊢ (B \in ℕ \land K \in ℕ_{0} \land R \in [0, +∞)) \to ⌊B^{- K} R⌋ = ⌊\frac{R}{B^{K}}⌋$
26	25	oveq1d	$⊢ (B \in ℕ \land K \in ℕ_{0} \land R \in [0, +∞)) \to ⌊B^{- K} R⌋ \mod B = ⌊\frac{R}{B^{K}}⌋ \mod B$
27	3 26	eqtrd	$⊢ (B \in ℕ \land K \in ℕ_{0} \land R \in [0, +∞)) \to K digit (B) R = ⌊\frac{R}{B^{K}}⌋ \mod B$

Metamath Proof Explorer

Theorem nn0digval

Proof