dignnld

Description: The leading digits of a positive integer are 0. (Contributed by AV, 25-May-2020)

		Ref	Expression
	Assertion	dignnld	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to K digit (B) N = 0$

Proof

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

Metamath Proof Explorer

Theorem dignnld

Proof