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 \in ℤ_{\geq 2} \land K \in ℕ_{0} \land N \in ℕ_{0}) \to K digit (B) B^{N} = if (K = N, 1, 0)$

Proof

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

Metamath Proof Explorer

Theorem digexp

Proof