digit2

Description: Two ways to express the K th digit in the decimal (when base B = 1 0 ) expansion of a number A . K = 1 corresponds to the first digit after the decimal point. (Contributed by NM, 25-Dec-2008)

		Ref	Expression
	Assertion	digit2	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to ⌊B^{K} A⌋ \mod B = ⌊B^{K} A⌋ - B ⌊B^{K - 1} A⌋$

Proof

Step	Hyp	Ref	Expression
1		nnre	$⊢ B \in ℕ \to B \in ℝ$
2		nnnn0	$⊢ K \in ℕ \to K \in ℕ_{0}$
3		reexpcl	$⊢ (B \in ℝ \land K \in ℕ_{0}) \to B^{K} \in ℝ$
4	1 2 3	syl2an	$⊢ (B \in ℕ \land K \in ℕ) \to B^{K} \in ℝ$
5		remulcl	$⊢ (B^{K} \in ℝ \land A \in ℝ) \to B^{K} A \in ℝ$
6	4 5	stoic3	$⊢ (B \in ℕ \land K \in ℕ \land A \in ℝ) \to B^{K} A \in ℝ$
7	6	3comr	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to B^{K} A \in ℝ$
8		reflcl	$⊢ B^{K} A \in ℝ \to ⌊B^{K} A⌋ \in ℝ$
9	7 8	syl	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to ⌊B^{K} A⌋ \in ℝ$
10		nnrp	$⊢ B \in ℕ \to B \in ℝ^{+}$
11	10	3ad2ant2	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to B \in ℝ^{+}$
12		modval	$⊢ (⌊B^{K} A⌋ \in ℝ \land B \in ℝ^{+}) \to ⌊B^{K} A⌋ \mod B = ⌊B^{K} A⌋ - B ⌊\frac{⌊B^{K} A⌋}{B}⌋$
13	9 11 12	syl2anc	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to ⌊B^{K} A⌋ \mod B = ⌊B^{K} A⌋ - B ⌊\frac{⌊B^{K} A⌋}{B}⌋$
14		simp2	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to B \in ℕ$
15		fldiv	$⊢ (B^{K} A \in ℝ \land B \in ℕ) \to ⌊\frac{⌊B^{K} A⌋}{B}⌋ = ⌊\frac{B^{K} A}{B}⌋$
16	7 14 15	syl2anc	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to ⌊\frac{⌊B^{K} A⌋}{B}⌋ = ⌊\frac{B^{K} A}{B}⌋$
17		nncn	$⊢ B \in ℕ \to B \in ℂ$
18		expcl	$⊢ (B \in ℂ \land K \in ℕ_{0}) \to B^{K} \in ℂ$
19	17 2 18	syl2an	$⊢ (B \in ℕ \land K \in ℕ) \to B^{K} \in ℂ$
20	19	3adant1	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to B^{K} \in ℂ$
21		recn	$⊢ A \in ℝ \to A \in ℂ$
22	21	3ad2ant1	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to A \in ℂ$
23		nnne0	$⊢ B \in ℕ \to B \neq 0$
24	17 23	jca	$⊢ B \in ℕ \to (B \in ℂ \land B \neq 0)$
25	24	3ad2ant2	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to (B \in ℂ \land B \neq 0)$
26		div23	$⊢ (B^{K} \in ℂ \land A \in ℂ \land (B \in ℂ \land B \neq 0)) \to \frac{B^{K} A}{B} = (\frac{B^{K}}{B}) A$
27	20 22 25 26	syl3anc	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to \frac{B^{K} A}{B} = (\frac{B^{K}}{B}) A$
28		nnz	$⊢ K \in ℕ \to K \in ℤ$
29		expm1	$⊢ (B \in ℂ \land B \neq 0 \land K \in ℤ) \to B^{K - 1} = \frac{B^{K}}{B}$
30	17 23 28 29	syl2an3an	$⊢ (B \in ℕ \land K \in ℕ) \to B^{K - 1} = \frac{B^{K}}{B}$
31	30	3adant1	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to B^{K - 1} = \frac{B^{K}}{B}$
32	31	oveq1d	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to B^{K - 1} A = (\frac{B^{K}}{B}) A$
33	27 32	eqtr4d	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to \frac{B^{K} A}{B} = B^{K - 1} A$
34	33	fveq2d	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to ⌊\frac{B^{K} A}{B}⌋ = ⌊B^{K - 1} A⌋$
35	16 34	eqtrd	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to ⌊\frac{⌊B^{K} A⌋}{B}⌋ = ⌊B^{K - 1} A⌋$
36	35	oveq2d	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to B ⌊\frac{⌊B^{K} A⌋}{B}⌋ = B ⌊B^{K - 1} A⌋$
37	36	oveq2d	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to ⌊B^{K} A⌋ - B ⌊\frac{⌊B^{K} A⌋}{B}⌋ = ⌊B^{K} A⌋ - B ⌊B^{K - 1} A⌋$
38	13 37	eqtrd	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to ⌊B^{K} A⌋ \mod B = ⌊B^{K} A⌋ - B ⌊B^{K - 1} A⌋$

Metamath Proof Explorer

Theorem digit2

Proof