dig1

Description: All but one digits of 1 are 0. (Contributed by AV, 24-May-2020)

		Ref	Expression
	Assertion	dig1	$⊢ (B \in ℤ_{\geq 2} \land K \in ℤ) \to K digit (B) 1 = if (K = 0, 1, 0)$

Proof

Step	Hyp	Ref	Expression
1		eluzelcn	$⊢ B \in ℤ_{\geq 2} \to B \in ℂ$
2	1	exp0d	$⊢ B \in ℤ_{\geq 2} \to B^{0} = 1$
3	2	eqcomd	$⊢ B \in ℤ_{\geq 2} \to 1 = B^{0}$
4	3	ad2antrl	$⊢ (0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to 1 = B^{0}$
5	4	oveq2d	$⊢ (0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to K digit (B) 1 = K digit (B) B^{0}$
6		simprl	$⊢ (0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to B \in ℤ_{\geq 2}$
7		simpr	$⊢ (B \in ℤ_{\geq 2} \land K \in ℤ) \to K \in ℤ$
8	7	anim2i	$⊢ (0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to (0 \leq K \land K \in ℤ)$
9	8	ancomd	$⊢ (0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to (K \in ℤ \land 0 \leq K)$
10		elnn0z	$⊢ K \in ℕ_{0} \leftrightarrow (K \in ℤ \land 0 \leq K)$
11	9 10	sylibr	$⊢ (0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to K \in ℕ_{0}$
12		0nn0	$⊢ 0 \in ℕ_{0}$
13	12	a1i	$⊢ (0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to 0 \in ℕ_{0}$
14		digexp	$⊢ (B \in ℤ_{\geq 2} \land K \in ℕ_{0} \land 0 \in ℕ_{0}) \to K digit (B) B^{0} = if (K = 0, 1, 0)$
15	6 11 13 14	syl3anc	$⊢ (0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to K digit (B) B^{0} = if (K = 0, 1, 0)$
16	5 15	eqtrd	$⊢ (0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to K digit (B) 1 = if (K = 0, 1, 0)$
17		eluz2nn	$⊢ B \in ℤ_{\geq 2} \to B \in ℕ$
18	17	ad2antrl	$⊢ (\neg 0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to B \in ℕ$
19		simprr	$⊢ (\neg 0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to K \in ℤ$
20		nn0ge0	$⊢ K \in ℕ_{0} \to 0 \leq K$
21	20	a1i	$⊢ (B \in ℤ_{\geq 2} \land K \in ℤ) \to (K \in ℕ_{0} \to 0 \leq K)$
22	21	con3d	$⊢ (B \in ℤ_{\geq 2} \land K \in ℤ) \to (\neg 0 \leq K \to \neg K \in ℕ_{0})$
23	22	impcom	$⊢ (\neg 0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to \neg K \in ℕ_{0}$
24	19 23	eldifd	$⊢ (\neg 0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to K \in (ℤ ∖ ℕ_{0})$
25		1nn0	$⊢ 1 \in ℕ_{0}$
26	25	a1i	$⊢ (\neg 0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to 1 \in ℕ_{0}$
27		dignn0fr	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land 1 \in ℕ_{0}) \to K digit (B) 1 = 0$
28	18 24 26 27	syl3anc	$⊢ (\neg 0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to K digit (B) 1 = 0$
29		0le0	$⊢ 0 \leq 0$
30		breq2	$⊢ K = 0 \to (0 \leq K \leftrightarrow 0 \leq 0)$
31	29 30	mpbiri	$⊢ K = 0 \to 0 \leq K$
32	31	a1i	$⊢ (B \in ℤ_{\geq 2} \land K \in ℤ) \to (K = 0 \to 0 \leq K)$
33	32	con3d	$⊢ (B \in ℤ_{\geq 2} \land K \in ℤ) \to (\neg 0 \leq K \to \neg K = 0)$
34	33	impcom	$⊢ (\neg 0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to \neg K = 0$
35	34	iffalsed	$⊢ (\neg 0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to if (K = 0, 1, 0) = 0$
36	28 35	eqtr4d	$⊢ (\neg 0 \leq K \land (B \in ℤ_{\geq 2} \land K \in ℤ)) \to K digit (B) 1 = if (K = 0, 1, 0)$
37	16 36	pm2.61ian	$⊢ (B \in ℤ_{\geq 2} \land K \in ℤ) \to K digit (B) 1 = if (K = 0, 1, 0)$

Metamath Proof Explorer

Theorem dig1

Proof