Metamath Proof Explorer

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