Metamath Proof Explorer

Theorem digit1

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

Ref Expression
Assertion digit1 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) = ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod ( 𝐵 ↑ 𝐾 ) ) − ( ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 ↑ 𝐾 ) ) ) )

Proof

Step Hyp Ref Expression
1 digit2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) − ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) ) )
2 1 3coml ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ∧ 𝐴 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) − ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) ) )
3 2 3expa ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) − ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) ) )
4 3 oveq1d ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) mod ( 𝐵 ↑ 𝐾 ) ) = ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) − ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) ) mod ( 𝐵 ↑ 𝐾 ) ) )
5 nnre ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
6 nnnn0 ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℕ0 )
7 reexpcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐵 ↑ 𝐾 ) ∈ ℝ )
8 5 6 7 syl2an ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ↑ 𝐾 ) ∈ ℝ )
9 remulcl ⊢ ( ( ( 𝐵 ↑ 𝐾 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ∈ ℝ )
10 8 9 sylan ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ∈ ℝ )
11 reflcl ⊢ ( ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ∈ ℝ → ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) ∈ ℝ )
12 10 11 syl ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) ∈ ℝ )
13 nnrp ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ+ )
14 13 ad2antrr ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → 𝐵 ∈ ℝ+ )
15 12 14 modcld ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) ∈ ℝ )
16 nnexpcl ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐵 ↑ 𝐾 ) ∈ ℕ )
17 6 16 sylan2 ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ↑ 𝐾 ) ∈ ℕ )
18 17 nnrpd ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ↑ 𝐾 ) ∈ ℝ+ )
19 18 adantr ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( 𝐵 ↑ 𝐾 ) ∈ ℝ+ )
20 modge0 ⊢ ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 0 ≤ ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) )
21 12 14 20 syl2anc ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → 0 ≤ ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) )
22 5 ad2antrr ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → 𝐵 ∈ ℝ )
23 8 adantr ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( 𝐵 ↑ 𝐾 ) ∈ ℝ )
24 modlt ⊢ ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) < 𝐵 )
25 12 14 24 syl2anc ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) < 𝐵 )
26 nncn ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
27 exp1 ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ↑ 1 ) = 𝐵 )
28 26 27 syl ⊢ ( 𝐵 ∈ ℕ → ( 𝐵 ↑ 1 ) = 𝐵 )
29 28 adantr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ↑ 1 ) = 𝐵 )
30 5 adantr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → 𝐵 ∈ ℝ )
31 nnge1 ⊢ ( 𝐵 ∈ ℕ → 1 ≤ 𝐵 )
32 31 adantr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → 1 ≤ 𝐵 )
33 simpr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → 𝐾 ∈ ℕ )
34 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
35 33 34 eleqtrdi ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → 𝐾 ∈ ( ℤ≥ ‘ 1 ) )
36 leexp2a ⊢ ( ( 𝐵 ∈ ℝ ∧ 1 ≤ 𝐵 ∧ 𝐾 ∈ ( ℤ≥ ‘ 1 ) ) → ( 𝐵 ↑ 1 ) ≤ ( 𝐵 ↑ 𝐾 ) )
37 30 32 35 36 syl3anc ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ↑ 1 ) ≤ ( 𝐵 ↑ 𝐾 ) )
38 29 37 eqbrtrrd ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → 𝐵 ≤ ( 𝐵 ↑ 𝐾 ) )
39 38 adantr ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → 𝐵 ≤ ( 𝐵 ↑ 𝐾 ) )
40 15 22 23 25 39 ltletrd ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) < ( 𝐵 ↑ 𝐾 ) )
41 modid ⊢ ( ( ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) ∈ ℝ ∧ ( 𝐵 ↑ 𝐾 ) ∈ ℝ+ ) ∧ ( 0 ≤ ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) < ( 𝐵 ↑ 𝐾 ) ) ) → ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) mod ( 𝐵 ↑ 𝐾 ) ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) )
42 15 19 21 40 41 syl22anc ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) mod ( 𝐵 ↑ 𝐾 ) ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) )
43 simpll ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → 𝐵 ∈ ℕ )
44 nnm1nn0 ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 − 1 ) ∈ ℕ0 )
45 reexpcl ⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐾 − 1 ) ∈ ℕ0 ) → ( 𝐵 ↑ ( 𝐾 − 1 ) ) ∈ ℝ )
46 5 44 45 syl2an ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ↑ ( 𝐾 − 1 ) ) ∈ ℝ )
47 remulcl ⊢ ( ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ∈ ℝ )
48 46 47 sylan ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ∈ ℝ )
49 nnexpcl ⊢ ( ( 𝐵 ∈ ℕ ∧ ( 𝐾 − 1 ) ∈ ℕ0 ) → ( 𝐵 ↑ ( 𝐾 − 1 ) ) ∈ ℕ )
50 44 49 sylan2 ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ↑ ( 𝐾 − 1 ) ) ∈ ℕ )
51 50 adantr ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( 𝐵 ↑ ( 𝐾 − 1 ) ) ∈ ℕ )
52 modmulnn ⊢ ( ( 𝐵 ∈ ℕ ∧ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ∈ ℝ ∧ ( 𝐵 ↑ ( 𝐾 − 1 ) ) ∈ ℕ ) → ( ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 · ( 𝐵 ↑ ( 𝐾 − 1 ) ) ) ) ≤ ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 · ( 𝐵 ↑ ( 𝐾 − 1 ) ) ) ) )
53 43 48 51 52 syl3anc ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 · ( 𝐵 ↑ ( 𝐾 − 1 ) ) ) ) ≤ ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 · ( 𝐵 ↑ ( 𝐾 − 1 ) ) ) ) )
54 expm1t ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ↑ 𝐾 ) = ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐵 ) )
55 expcl ⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐾 − 1 ) ∈ ℕ0 ) → ( 𝐵 ↑ ( 𝐾 − 1 ) ) ∈ ℂ )
56 44 55 sylan2 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ↑ ( 𝐾 − 1 ) ) ∈ ℂ )
57 simpl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐾 ∈ ℕ ) → 𝐵 ∈ ℂ )
58 56 57 mulcomd ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐾 ∈ ℕ ) → ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐵 ) = ( 𝐵 · ( 𝐵 ↑ ( 𝐾 − 1 ) ) ) )
59 54 58 eqtrd ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ↑ 𝐾 ) = ( 𝐵 · ( 𝐵 ↑ ( 𝐾 − 1 ) ) ) )
60 26 59 sylan ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ↑ 𝐾 ) = ( 𝐵 · ( 𝐵 ↑ ( 𝐾 − 1 ) ) ) )
61 60 adantr ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( 𝐵 ↑ 𝐾 ) = ( 𝐵 · ( 𝐵 ↑ ( 𝐾 − 1 ) ) ) )
62 61 oveq2d ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 ↑ 𝐾 ) ) = ( ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 · ( 𝐵 ↑ ( 𝐾 − 1 ) ) ) ) )
63 61 oveq1d ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) = ( ( 𝐵 · ( 𝐵 ↑ ( 𝐾 − 1 ) ) ) · 𝐴 ) )
64 26 ad2antrr ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → 𝐵 ∈ ℂ )
65 26 44 55 syl2an ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝐵 ↑ ( 𝐾 − 1 ) ) ∈ ℂ )
66 65 adantr ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( 𝐵 ↑ ( 𝐾 − 1 ) ) ∈ ℂ )
67 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
68 67 adantl ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℂ )
69 64 66 68 mulassd ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 · ( 𝐵 ↑ ( 𝐾 − 1 ) ) ) · 𝐴 ) = ( 𝐵 · ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) )
70 63 69 eqtrd ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) = ( 𝐵 · ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) )
71 70 fveq2d ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) = ( ⌊ ‘ ( 𝐵 · ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) )
72 71 61 oveq12d ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod ( 𝐵 ↑ 𝐾 ) ) = ( ( ⌊ ‘ ( 𝐵 · ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 · ( 𝐵 ↑ ( 𝐾 − 1 ) ) ) ) )
73 53 62 72 3brtr4d ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 ↑ 𝐾 ) ) ≤ ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod ( 𝐵 ↑ 𝐾 ) ) )
74 reflcl ⊢ ( ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ∈ ℝ → ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ∈ ℝ )
75 48 74 syl ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ∈ ℝ )
76 remulcl ⊢ ( ( 𝐵 ∈ ℝ ∧ ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ∈ ℝ ) → ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) ∈ ℝ )
77 22 75 76 syl2anc ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) ∈ ℝ )
78 modsubdir ⊢ ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) ∈ ℝ ∧ ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) ∈ ℝ ∧ ( 𝐵 ↑ 𝐾 ) ∈ ℝ+ ) → ( ( ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 ↑ 𝐾 ) ) ≤ ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod ( 𝐵 ↑ 𝐾 ) ) ↔ ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) − ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) ) mod ( 𝐵 ↑ 𝐾 ) ) = ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod ( 𝐵 ↑ 𝐾 ) ) − ( ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 ↑ 𝐾 ) ) ) ) )
79 12 77 19 78 syl3anc ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 ↑ 𝐾 ) ) ≤ ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod ( 𝐵 ↑ 𝐾 ) ) ↔ ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) − ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) ) mod ( 𝐵 ↑ 𝐾 ) ) = ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod ( 𝐵 ↑ 𝐾 ) ) − ( ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 ↑ 𝐾 ) ) ) ) )
80 73 79 mpbid ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) − ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) ) mod ( 𝐵 ↑ 𝐾 ) ) = ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod ( 𝐵 ↑ 𝐾 ) ) − ( ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 ↑ 𝐾 ) ) ) )
81 4 42 80 3eqtr3d ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) ∧ 𝐴 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) = ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod ( 𝐵 ↑ 𝐾 ) ) − ( ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 ↑ 𝐾 ) ) ) )
82 81 3impa ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ∧ 𝐴 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) = ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod ( 𝐵 ↑ 𝐾 ) ) − ( ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 ↑ 𝐾 ) ) ) )
83 82 3comr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) = ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod ( 𝐵 ↑ 𝐾 ) ) − ( ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 ↑ 𝐾 ) ) ) )