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 
|- ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> ( K ( digit ` B ) N ) = 0 )

Proof

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