Theorem 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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) − ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		nnre	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
2		nnnn0	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℕ0 )
3		reexpcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐵 ↑ 𝐾 ) ∈ ℝ )
4	1 2 3	syl2an	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ↑ 𝐾 ) ∈ ℝ )
5		remulcl	⊢ ( ( ( 𝐵 ↑ 𝐾 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ∈ ℝ )
6	4 5	stoic3	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ∈ ℝ )
7	6	3comr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ∈ ℝ )
8		reflcl	⊢ ( ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ∈ ℝ → ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) ∈ ℝ )
9	7 8	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) ∈ ℝ )
10		nnrp	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ+ )
11	10	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → 𝐵 ∈ ℝ+ )
12		modval	⊢ ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) − ( 𝐵 · ( ⌊ ‘ ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) / 𝐵 ) ) ) ) )
13	9 11 12	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) − ( 𝐵 · ( ⌊ ‘ ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) / 𝐵 ) ) ) ) )
14		simp2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → 𝐵 ∈ ℕ )
15		fldiv	⊢ ( ( ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) / 𝐵 ) ) = ( ⌊ ‘ ( ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) / 𝐵 ) ) )
16	7 14 15	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) / 𝐵 ) ) = ( ⌊ ‘ ( ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) / 𝐵 ) ) )
17		nncn	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
18		expcl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐵 ↑ 𝐾 ) ∈ ℂ )
19	17 2 18	syl2an	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ↑ 𝐾 ) ∈ ℂ )
20	19	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ↑ 𝐾 ) ∈ ℂ )
21		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
22	21	3ad2ant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → 𝐴 ∈ ℂ )
23		nnne0	⊢ ( 𝐵 ∈ ℕ → 𝐵 ≠ 0 )
24	17 23	jca	⊢ ( 𝐵 ∈ ℕ → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
25	24	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
26		div23	⊢ ( ( ( 𝐵 ↑ 𝐾 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) / 𝐵 ) = ( ( ( 𝐵 ↑ 𝐾 ) / 𝐵 ) · 𝐴 ) )
27	20 22 25 26	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) / 𝐵 ) = ( ( ( 𝐵 ↑ 𝐾 ) / 𝐵 ) · 𝐴 ) )
28		nnz	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℤ )
29		expm1	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐾 ∈ ℤ ) → ( 𝐵 ↑ ( 𝐾 − 1 ) ) = ( ( 𝐵 ↑ 𝐾 ) / 𝐵 ) )
30	17 23 28 29	syl2an3an	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ↑ ( 𝐾 − 1 ) ) = ( ( 𝐵 ↑ 𝐾 ) / 𝐵 ) )
31	30	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ↑ ( 𝐾 − 1 ) ) = ( ( 𝐵 ↑ 𝐾 ) / 𝐵 ) )
32	31	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) = ( ( ( 𝐵 ↑ 𝐾 ) / 𝐵 ) · 𝐴 ) )
33	27 32	eqtr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) / 𝐵 ) = ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) )
34	33	fveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ⌊ ‘ ( ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) / 𝐵 ) ) = ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) )
35	16 34	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ⌊ ‘ ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) / 𝐵 ) ) = ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) )
36	35	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 · ( ⌊ ‘ ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) / 𝐵 ) ) ) = ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) )
37	36	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) − ( 𝐵 · ( ⌊ ‘ ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) / 𝐵 ) ) ) ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) − ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) ) )
38	13 37	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) − ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) ) )