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 ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → ( 𝐾 ( digit ‘ 𝐵 ) 𝑁 ) = 0 )

Proof

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