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

Proof

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