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 
|- ( ( B e. ( ZZ>= ` 2 ) /\ K e. NN0 /\ N e. NN0 ) -> ( K ( digit ` B ) ( B ^ N ) ) = if ( K = N , 1 , 0 ) )

Proof

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