# Metamath Proof Explorer

## Theorem dignnld

Description: The leading digits of a positive integer are 0. (Contributed by AV, 25-May-2020)

Ref Expression
Assertion dignnld ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {K}\mathrm{digit}\left({B}\right){N}=0$

### Proof

Step Hyp Ref Expression
1 eluz2nn ${⊢}{B}\in {ℤ}_{\ge 2}\to {B}\in ℕ$
2 1 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {B}\in ℕ$
3 nnrp ${⊢}{N}\in ℕ\to {N}\in {ℝ}^{+}$
4 3 anim2i ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\to \left({B}\in {ℤ}_{\ge 2}\wedge {N}\in {ℝ}^{+}\right)$
5 relogbzcl ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in {ℝ}^{+}\right)\to {\mathrm{log}}_{{B}}{N}\in ℝ$
6 4 5 syl ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\to {\mathrm{log}}_{{B}}{N}\in ℝ$
7 nnre ${⊢}{N}\in ℕ\to {N}\in ℝ$
8 nnge1 ${⊢}{N}\in ℕ\to 1\le {N}$
9 7 8 jca ${⊢}{N}\in ℕ\to \left({N}\in ℝ\wedge 1\le {N}\right)$
10 1re ${⊢}1\in ℝ$
11 elicopnf ${⊢}1\in ℝ\to \left({N}\in \left[1,\mathrm{+\infty }\right)↔\left({N}\in ℝ\wedge 1\le {N}\right)\right)$
12 10 11 ax-mp ${⊢}{N}\in \left[1,\mathrm{+\infty }\right)↔\left({N}\in ℝ\wedge 1\le {N}\right)$
13 9 12 sylibr ${⊢}{N}\in ℕ\to {N}\in \left[1,\mathrm{+\infty }\right)$
14 13 anim2i ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\to \left({B}\in {ℤ}_{\ge 2}\wedge {N}\in \left[1,\mathrm{+\infty }\right)\right)$
15 rege1logbzge0 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in \left[1,\mathrm{+\infty }\right)\right)\to 0\le {\mathrm{log}}_{{B}}{N}$
16 14 15 syl ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\to 0\le {\mathrm{log}}_{{B}}{N}$
17 6 16 jca ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\to \left({\mathrm{log}}_{{B}}{N}\in ℝ\wedge 0\le {\mathrm{log}}_{{B}}{N}\right)$
18 flge0nn0 ${⊢}\left({\mathrm{log}}_{{B}}{N}\in ℝ\wedge 0\le {\mathrm{log}}_{{B}}{N}\right)\to ⌊{\mathrm{log}}_{{B}}{N}⌋\in {ℕ}_{0}$
19 peano2nn0 ${⊢}⌊{\mathrm{log}}_{{B}}{N}⌋\in {ℕ}_{0}\to ⌊{\mathrm{log}}_{{B}}{N}⌋+1\in {ℕ}_{0}$
20 17 18 19 3syl ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\to ⌊{\mathrm{log}}_{{B}}{N}⌋+1\in {ℕ}_{0}$
21 eluznn0 ${⊢}\left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\in {ℕ}_{0}\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {K}\in {ℕ}_{0}$
22 20 21 stoic3 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {K}\in {ℕ}_{0}$
23 nnnn0 ${⊢}{N}\in ℕ\to {N}\in {ℕ}_{0}$
24 nn0rp0 ${⊢}{N}\in {ℕ}_{0}\to {N}\in \left[0,\mathrm{+\infty }\right)$
25 23 24 syl ${⊢}{N}\in ℕ\to {N}\in \left[0,\mathrm{+\infty }\right)$
26 25 3ad2ant2 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {N}\in \left[0,\mathrm{+\infty }\right)$
27 nn0digval ${⊢}\left({B}\in ℕ\wedge {K}\in {ℕ}_{0}\wedge {N}\in \left[0,\mathrm{+\infty }\right)\right)\to {K}\mathrm{digit}\left({B}\right){N}=⌊\frac{{N}}{{{B}}^{{K}}}⌋\mathrm{mod}{B}$
28 2 22 26 27 syl3anc ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {K}\mathrm{digit}\left({B}\right){N}=⌊\frac{{N}}{{{B}}^{{K}}}⌋\mathrm{mod}{B}$
29 7 3ad2ant2 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {N}\in ℝ$
30 eluzelre ${⊢}{B}\in {ℤ}_{\ge 2}\to {B}\in ℝ$
31 30 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {B}\in ℝ$
32 eluz2n0 ${⊢}{B}\in {ℤ}_{\ge 2}\to {B}\ne 0$
33 32 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {B}\ne 0$
34 eluzelz ${⊢}{K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\to {K}\in ℤ$
35 34 3ad2ant3 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {K}\in ℤ$
36 31 33 35 reexpclzd ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {{B}}^{{K}}\in ℝ$
37 eluzelcn ${⊢}{B}\in {ℤ}_{\ge 2}\to {B}\in ℂ$
38 37 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {B}\in ℂ$
39 38 33 35 expne0d ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {{B}}^{{K}}\ne 0$
40 29 36 39 redivcld ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to \frac{{N}}{{{B}}^{{K}}}\in ℝ$
41 nn0ge0 ${⊢}{N}\in {ℕ}_{0}\to 0\le {N}$
42 23 41 syl ${⊢}{N}\in ℕ\to 0\le {N}$
43 42 3ad2ant2 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to 0\le {N}$
44 1 nngt0d ${⊢}{B}\in {ℤ}_{\ge 2}\to 0<{B}$
45 44 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to 0<{B}$
46 expgt0 ${⊢}\left({B}\in ℝ\wedge {K}\in ℤ\wedge 0<{B}\right)\to 0<{{B}}^{{K}}$
47 31 35 45 46 syl3anc ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to 0<{{B}}^{{K}}$
48 ge0div ${⊢}\left({N}\in ℝ\wedge {{B}}^{{K}}\in ℝ\wedge 0<{{B}}^{{K}}\right)\to \left(0\le {N}↔0\le \frac{{N}}{{{B}}^{{K}}}\right)$
49 29 36 47 48 syl3anc ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to \left(0\le {N}↔0\le \frac{{N}}{{{B}}^{{K}}}\right)$
50 43 49 mpbid ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to 0\le \frac{{N}}{{{B}}^{{K}}}$
51 dignn0ldlem ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {N}<{{B}}^{{K}}$
52 1 nnrpd ${⊢}{B}\in {ℤ}_{\ge 2}\to {B}\in {ℝ}^{+}$
53 rpexpcl ${⊢}\left({B}\in {ℝ}^{+}\wedge {K}\in ℤ\right)\to {{B}}^{{K}}\in {ℝ}^{+}$
54 52 34 53 syl2an ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {{B}}^{{K}}\in {ℝ}^{+}$
55 54 3adant2 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {{B}}^{{K}}\in {ℝ}^{+}$
56 divlt1lt ${⊢}\left({N}\in ℝ\wedge {{B}}^{{K}}\in {ℝ}^{+}\right)\to \left(\frac{{N}}{{{B}}^{{K}}}<1↔{N}<{{B}}^{{K}}\right)$
57 29 55 56 syl2anc ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to \left(\frac{{N}}{{{B}}^{{K}}}<1↔{N}<{{B}}^{{K}}\right)$
58 51 57 mpbird ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to \frac{{N}}{{{B}}^{{K}}}<1$
59 0re ${⊢}0\in ℝ$
60 1xr ${⊢}1\in {ℝ}^{*}$
61 59 60 pm3.2i ${⊢}\left(0\in ℝ\wedge 1\in {ℝ}^{*}\right)$
62 elico2 ${⊢}\left(0\in ℝ\wedge 1\in {ℝ}^{*}\right)\to \left(\frac{{N}}{{{B}}^{{K}}}\in \left[0,1\right)↔\left(\frac{{N}}{{{B}}^{{K}}}\in ℝ\wedge 0\le \frac{{N}}{{{B}}^{{K}}}\wedge \frac{{N}}{{{B}}^{{K}}}<1\right)\right)$
63 61 62 mp1i ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to \left(\frac{{N}}{{{B}}^{{K}}}\in \left[0,1\right)↔\left(\frac{{N}}{{{B}}^{{K}}}\in ℝ\wedge 0\le \frac{{N}}{{{B}}^{{K}}}\wedge \frac{{N}}{{{B}}^{{K}}}<1\right)\right)$
64 40 50 58 63 mpbir3and ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to \frac{{N}}{{{B}}^{{K}}}\in \left[0,1\right)$
65 ico01fl0 ${⊢}\frac{{N}}{{{B}}^{{K}}}\in \left[0,1\right)\to ⌊\frac{{N}}{{{B}}^{{K}}}⌋=0$
66 64 65 syl ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to ⌊\frac{{N}}{{{B}}^{{K}}}⌋=0$
67 66 oveq1d ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to ⌊\frac{{N}}{{{B}}^{{K}}}⌋\mathrm{mod}{B}=0\mathrm{mod}{B}$
68 52 3ad2ant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {B}\in {ℝ}^{+}$
69 0mod ${⊢}{B}\in {ℝ}^{+}\to 0\mathrm{mod}{B}=0$
70 68 69 syl ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to 0\mathrm{mod}{B}=0$
71 28 67 70 3eqtrd ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\wedge {K}\in {ℤ}_{\ge \left(⌊{\mathrm{log}}_{{B}}{N}⌋+1\right)}\right)\to {K}\mathrm{digit}\left({B}\right){N}=0$