# Metamath Proof Explorer

## Theorem digexp

Description: The K th digit of a power to the base is either 1 or 0. (Contributed by AV, 24-May-2020)

Ref Expression
Assertion digexp ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {K}\mathrm{digit}\left({B}\right){{B}}^{{N}}=if\left({K}={N},1,0\right)$

### Proof

Step Hyp Ref Expression
1 eluzelcn ${⊢}{B}\in {ℤ}_{\ge 2}\to {B}\in ℂ$
2 eluz2nn ${⊢}{B}\in {ℤ}_{\ge 2}\to {B}\in ℕ$
3 2 nnne0d ${⊢}{B}\in {ℤ}_{\ge 2}\to {B}\ne 0$
4 1 3 jca ${⊢}{B}\in {ℤ}_{\ge 2}\to \left({B}\in ℂ\wedge {B}\ne 0\right)$
5 4 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({B}\in ℂ\wedge {B}\ne 0\right)$
6 nn0z ${⊢}{K}\in {ℕ}_{0}\to {K}\in ℤ$
7 nn0z ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℤ$
8 6 7 anim12i ${⊢}\left({K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({K}\in ℤ\wedge {N}\in ℤ\right)$
9 8 ancomd ${⊢}\left({K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({N}\in ℤ\wedge {K}\in ℤ\right)$
10 9 3adant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({N}\in ℤ\wedge {K}\in ℤ\right)$
11 expsub ${⊢}\left(\left({B}\in ℂ\wedge {B}\ne 0\right)\wedge \left({N}\in ℤ\wedge {K}\in ℤ\right)\right)\to {{B}}^{{N}-{K}}=\frac{{{B}}^{{N}}}{{{B}}^{{K}}}$
12 5 10 11 syl2anc ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {{B}}^{{N}-{K}}=\frac{{{B}}^{{N}}}{{{B}}^{{K}}}$
13 12 eqcomd ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \frac{{{B}}^{{N}}}{{{B}}^{{K}}}={{B}}^{{N}-{K}}$
14 13 fveq2d ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to ⌊\frac{{{B}}^{{N}}}{{{B}}^{{K}}}⌋=⌊{{B}}^{{N}-{K}}⌋$
15 14 oveq1d ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to ⌊\frac{{{B}}^{{N}}}{{{B}}^{{K}}}⌋\mathrm{mod}{B}=⌊{{B}}^{{N}-{K}}⌋\mathrm{mod}{B}$
16 2 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {B}\in ℕ$
17 simp2 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {K}\in {ℕ}_{0}$
18 eluzelre ${⊢}{B}\in {ℤ}_{\ge 2}\to {B}\in ℝ$
19 reexpcl ${⊢}\left({B}\in ℝ\wedge {N}\in {ℕ}_{0}\right)\to {{B}}^{{N}}\in ℝ$
20 18 19 sylan ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\to {{B}}^{{N}}\in ℝ$
21 18 adantr ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\to {B}\in ℝ$
22 simpr ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\to {N}\in {ℕ}_{0}$
23 eluzge2nn0 ${⊢}{B}\in {ℤ}_{\ge 2}\to {B}\in {ℕ}_{0}$
24 23 nn0ge0d ${⊢}{B}\in {ℤ}_{\ge 2}\to 0\le {B}$
25 24 adantr ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\to 0\le {B}$
26 21 22 25 expge0d ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\to 0\le {{B}}^{{N}}$
27 20 26 jca ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\to \left({{B}}^{{N}}\in ℝ\wedge 0\le {{B}}^{{N}}\right)$
28 27 3adant2 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({{B}}^{{N}}\in ℝ\wedge 0\le {{B}}^{{N}}\right)$
29 elrege0 ${⊢}{{B}}^{{N}}\in \left[0,\mathrm{+\infty }\right)↔\left({{B}}^{{N}}\in ℝ\wedge 0\le {{B}}^{{N}}\right)$
30 28 29 sylibr ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {{B}}^{{N}}\in \left[0,\mathrm{+\infty }\right)$
31 nn0digval ${⊢}\left({B}\in ℕ\wedge {K}\in {ℕ}_{0}\wedge {{B}}^{{N}}\in \left[0,\mathrm{+\infty }\right)\right)\to {K}\mathrm{digit}\left({B}\right){{B}}^{{N}}=⌊\frac{{{B}}^{{N}}}{{{B}}^{{K}}}⌋\mathrm{mod}{B}$
32 16 17 30 31 syl3anc ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {K}\mathrm{digit}\left({B}\right){{B}}^{{N}}=⌊\frac{{{B}}^{{N}}}{{{B}}^{{K}}}⌋\mathrm{mod}{B}$
33 simpr ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge {K}={N}\right)\to {K}={N}$
34 33 eqcomd ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge {K}={N}\right)\to {N}={K}$
35 nn0cn ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℂ$
36 35 3ad2ant3 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {N}\in ℂ$
37 nn0cn ${⊢}{K}\in {ℕ}_{0}\to {K}\in ℂ$
38 37 3ad2ant2 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {K}\in ℂ$
39 36 38 subeq0ad ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({N}-{K}=0↔{N}={K}\right)$
40 39 adantr ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge {K}={N}\right)\to \left({N}-{K}=0↔{N}={K}\right)$
41 34 40 mpbird ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge {K}={N}\right)\to {N}-{K}=0$
42 41 oveq2d ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge {K}={N}\right)\to {{B}}^{{N}-{K}}={{B}}^{0}$
43 1 exp0d ${⊢}{B}\in {ℤ}_{\ge 2}\to {{B}}^{0}=1$
44 43 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {{B}}^{0}=1$
45 44 adantr ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge {K}={N}\right)\to {{B}}^{0}=1$
46 42 45 eqtrd ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge {K}={N}\right)\to {{B}}^{{N}-{K}}=1$
47 46 fveq2d ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge {K}={N}\right)\to ⌊{{B}}^{{N}-{K}}⌋=⌊1⌋$
48 1zzd ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge {K}={N}\right)\to 1\in ℤ$
49 flid ${⊢}1\in ℤ\to ⌊1⌋=1$
50 48 49 syl ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge {K}={N}\right)\to ⌊1⌋=1$
51 47 50 eqtrd ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge {K}={N}\right)\to ⌊{{B}}^{{N}-{K}}⌋=1$
52 51 oveq1d ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge {K}={N}\right)\to ⌊{{B}}^{{N}-{K}}⌋\mathrm{mod}{B}=1\mathrm{mod}{B}$
53 eluz2gt1 ${⊢}{B}\in {ℤ}_{\ge 2}\to 1<{B}$
54 1mod ${⊢}\left({B}\in ℝ\wedge 1<{B}\right)\to 1\mathrm{mod}{B}=1$
55 18 53 54 syl2anc ${⊢}{B}\in {ℤ}_{\ge 2}\to 1\mathrm{mod}{B}=1$
56 55 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to 1\mathrm{mod}{B}=1$
57 56 adantr ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge {K}={N}\right)\to 1\mathrm{mod}{B}=1$
58 52 57 eqtr2d ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge {K}={N}\right)\to 1=⌊{{B}}^{{N}-{K}}⌋\mathrm{mod}{B}$
59 simprl1 ${⊢}\left({N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to {B}\in {ℤ}_{\ge 2}$
60 7 adantl ${⊢}\left({K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {N}\in ℤ$
61 6 adantr ${⊢}\left({K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {K}\in ℤ$
62 60 61 zsubcld ${⊢}\left({K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {N}-{K}\in ℤ$
63 62 3adant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {N}-{K}\in ℤ$
64 63 ad2antrl ${⊢}\left({N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to {N}-{K}\in ℤ$
65 nn0re ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℝ$
66 65 3ad2ant3 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {N}\in ℝ$
67 nn0re ${⊢}{K}\in {ℕ}_{0}\to {K}\in ℝ$
68 67 3ad2ant2 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {K}\in ℝ$
69 66 68 sublt0d ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({N}-{K}<0↔{N}<{K}\right)$
70 69 biimprd ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({N}<{K}\to {N}-{K}<0\right)$
71 70 adantr ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\to \left({N}<{K}\to {N}-{K}<0\right)$
72 71 impcom ${⊢}\left({N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to {N}-{K}<0$
73 expnegico01 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}-{K}\in ℤ\wedge {N}-{K}<0\right)\to {{B}}^{{N}-{K}}\in \left[0,1\right)$
74 59 64 72 73 syl3anc ${⊢}\left({N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to {{B}}^{{N}-{K}}\in \left[0,1\right)$
75 ico01fl0 ${⊢}{{B}}^{{N}-{K}}\in \left[0,1\right)\to ⌊{{B}}^{{N}-{K}}⌋=0$
76 74 75 syl ${⊢}\left({N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to ⌊{{B}}^{{N}-{K}}⌋=0$
77 76 oveq1d ${⊢}\left({N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to ⌊{{B}}^{{N}-{K}}⌋\mathrm{mod}{B}=0\mathrm{mod}{B}$
78 2 nnrpd ${⊢}{B}\in {ℤ}_{\ge 2}\to {B}\in {ℝ}^{+}$
79 0mod ${⊢}{B}\in {ℝ}^{+}\to 0\mathrm{mod}{B}=0$
80 78 79 syl ${⊢}{B}\in {ℤ}_{\ge 2}\to 0\mathrm{mod}{B}=0$
81 80 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to 0\mathrm{mod}{B}=0$
82 81 ad2antrl ${⊢}\left({N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to 0\mathrm{mod}{B}=0$
83 77 82 eqtrd ${⊢}\left({N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to ⌊{{B}}^{{N}-{K}}⌋\mathrm{mod}{B}=0$
84 eluzelz ${⊢}{B}\in {ℤ}_{\ge 2}\to {B}\in ℤ$
85 84 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {B}\in ℤ$
86 85 ad2antrl ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to {B}\in ℤ$
87 67 65 anim12i ${⊢}\left({K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({K}\in ℝ\wedge {N}\in ℝ\right)$
88 lenlt ${⊢}\left({K}\in ℝ\wedge {N}\in ℝ\right)\to \left({K}\le {N}↔¬{N}<{K}\right)$
89 88 bicomd ${⊢}\left({K}\in ℝ\wedge {N}\in ℝ\right)\to \left(¬{N}<{K}↔{K}\le {N}\right)$
90 87 89 syl ${⊢}\left({K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left(¬{N}<{K}↔{K}\le {N}\right)$
91 90 biimpd ${⊢}\left({K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left(¬{N}<{K}\to {K}\le {N}\right)$
92 91 3adant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left(¬{N}<{K}\to {K}\le {N}\right)$
93 92 adantr ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\to \left(¬{N}<{K}\to {K}\le {N}\right)$
94 93 impcom ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to {K}\le {N}$
95 3simpc ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)$
96 95 ad2antrl ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to \left({K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)$
97 nn0sub ${⊢}\left({K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({K}\le {N}↔{N}-{K}\in {ℕ}_{0}\right)$
98 96 97 syl ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to \left({K}\le {N}↔{N}-{K}\in {ℕ}_{0}\right)$
99 94 98 mpbid ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to {N}-{K}\in {ℕ}_{0}$
100 zexpcl ${⊢}\left({B}\in ℤ\wedge {N}-{K}\in {ℕ}_{0}\right)\to {{B}}^{{N}-{K}}\in ℤ$
101 86 99 100 syl2anc ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to {{B}}^{{N}-{K}}\in ℤ$
102 flid ${⊢}{{B}}^{{N}-{K}}\in ℤ\to ⌊{{B}}^{{N}-{K}}⌋={{B}}^{{N}-{K}}$
103 101 102 syl ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to ⌊{{B}}^{{N}-{K}}⌋={{B}}^{{N}-{K}}$
104 103 oveq1d ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to ⌊{{B}}^{{N}-{K}}⌋\mathrm{mod}{B}={{B}}^{{N}-{K}}\mathrm{mod}{B}$
105 1 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {B}\in ℂ$
106 3 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {B}\ne 0$
107 105 106 63 expm1d ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {{B}}^{{N}-{K}-1}=\frac{{{B}}^{{N}-{K}}}{{B}}$
108 107 eqcomd ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \frac{{{B}}^{{N}-{K}}}{{B}}={{B}}^{{N}-{K}-1}$
109 108 ad2antrl ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to \frac{{{B}}^{{N}-{K}}}{{B}}={{B}}^{{N}-{K}-1}$
110 pm4.56 ${⊢}\left(¬{K}={N}\wedge ¬{N}<{K}\right)↔¬\left({K}={N}\vee {N}<{K}\right)$
111 87 3adant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({K}\in ℝ\wedge {N}\in ℝ\right)$
112 axlttri ${⊢}\left({K}\in ℝ\wedge {N}\in ℝ\right)\to \left({K}<{N}↔¬\left({K}={N}\vee {N}<{K}\right)\right)$
113 111 112 syl ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({K}<{N}↔¬\left({K}={N}\vee {N}<{K}\right)\right)$
114 113 biimprd ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left(¬\left({K}={N}\vee {N}<{K}\right)\to {K}<{N}\right)$
115 110 114 syl5bi ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left(\left(¬{K}={N}\wedge ¬{N}<{K}\right)\to {K}<{N}\right)$
116 115 expdimp ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\to \left(¬{N}<{K}\to {K}<{N}\right)$
117 116 impcom ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to {K}<{N}$
118 8 3adant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({K}\in ℤ\wedge {N}\in ℤ\right)$
119 118 ad2antrl ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to \left({K}\in ℤ\wedge {N}\in ℤ\right)$
120 znnsub ${⊢}\left({K}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}<{N}↔{N}-{K}\in ℕ\right)$
121 119 120 syl ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to \left({K}<{N}↔{N}-{K}\in ℕ\right)$
122 117 121 mpbid ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to {N}-{K}\in ℕ$
123 nnm1nn0 ${⊢}{N}-{K}\in ℕ\to {N}-{K}-1\in {ℕ}_{0}$
124 122 123 syl ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to {N}-{K}-1\in {ℕ}_{0}$
125 zexpcl ${⊢}\left({B}\in ℤ\wedge {N}-{K}-1\in {ℕ}_{0}\right)\to {{B}}^{{N}-{K}-1}\in ℤ$
126 86 124 125 syl2anc ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to {{B}}^{{N}-{K}-1}\in ℤ$
127 109 126 eqeltrd ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to \frac{{{B}}^{{N}-{K}}}{{B}}\in ℤ$
128 18 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {B}\in ℝ$
129 128 106 63 reexpclzd ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {{B}}^{{N}-{K}}\in ℝ$
130 78 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {B}\in {ℝ}^{+}$
131 mod0 ${⊢}\left({{B}}^{{N}-{K}}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({{B}}^{{N}-{K}}\mathrm{mod}{B}=0↔\frac{{{B}}^{{N}-{K}}}{{B}}\in ℤ\right)$
132 129 130 131 syl2anc ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({{B}}^{{N}-{K}}\mathrm{mod}{B}=0↔\frac{{{B}}^{{N}-{K}}}{{B}}\in ℤ\right)$
133 132 ad2antrl ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to \left({{B}}^{{N}-{K}}\mathrm{mod}{B}=0↔\frac{{{B}}^{{N}-{K}}}{{B}}\in ℤ\right)$
134 127 133 mpbird ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to {{B}}^{{N}-{K}}\mathrm{mod}{B}=0$
135 104 134 eqtrd ${⊢}\left(¬{N}<{K}\wedge \left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\right)\to ⌊{{B}}^{{N}-{K}}⌋\mathrm{mod}{B}=0$
136 83 135 pm2.61ian ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\to ⌊{{B}}^{{N}-{K}}⌋\mathrm{mod}{B}=0$
137 136 eqcomd ${⊢}\left(\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\wedge ¬{K}={N}\right)\to 0=⌊{{B}}^{{N}-{K}}⌋\mathrm{mod}{B}$
138 58 137 ifeqda ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to if\left({K}={N},1,0\right)=⌊{{B}}^{{N}-{K}}⌋\mathrm{mod}{B}$
139 15 32 138 3eqtr4d ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {K}\mathrm{digit}\left({B}\right){{B}}^{{N}}=if\left({K}={N},1,0\right)$