dignn0ldlem

		Ref	Expression
	Assertion	dignn0ldlem	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to N < B^{K}$

Proof

Step	Hyp	Ref	Expression
1		nnre	$⊢ N \in ℕ \to N \in ℝ$
2	1	3ad2ant2	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to N \in ℝ$
3		eluzelre	$⊢ B \in ℤ_{\geq 2} \to B \in ℝ$
4	3	3ad2ant1	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to B \in ℝ$
5		eluz2nn	$⊢ B \in ℤ_{\geq 2} \to B \in ℕ$
6		nnnn0	$⊢ B \in ℕ \to B \in ℕ_{0}$
7	6	nn0ge0d	$⊢ B \in ℕ \to 0 \leq B$
8	5 7	syl	$⊢ B \in ℤ_{\geq 2} \to 0 \leq B$
9	8	3ad2ant1	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to 0 \leq B$
10		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
11		relogbzcl	$⊢ (B \in ℤ_{\geq 2} \land N \in ℝ^{+}) \to \log_{B} N \in ℝ$
12	10 11	sylan2	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ) \to \log_{B} N \in ℝ$
13	12	3adant3	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to \log_{B} N \in ℝ$
14	4 9 13	recxpcld	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to B^{\log_{B} N} \in ℝ$
15		eluzelre	$⊢ K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)} \to K \in ℝ$
16	15	3ad2ant3	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to K \in ℝ$
17	4 9 16	recxpcld	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to B^{K} \in ℝ$
18	1	leidd	$⊢ N \in ℕ \to N \leq N$
19	18	adantl	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ) \to N \leq N$
20		eluz2cnn0n1	$⊢ B \in ℤ_{\geq 2} \to B \in (ℂ ∖ \{0, 1\})$
21		nncn	$⊢ N \in ℕ \to N \in ℂ$
22		nnne0	$⊢ N \in ℕ \to N \neq 0$
23		eldifsn	$⊢ N \in (ℂ ∖ \{0\}) \leftrightarrow (N \in ℂ \land N \neq 0)$
24	21 22 23	sylanbrc	$⊢ N \in ℕ \to N \in (ℂ ∖ \{0\})$
25		cxplogb	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land N \in (ℂ ∖ \{0\})) \to B^{\log_{B} N} = N$
26	20 24 25	syl2an	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ) \to B^{\log_{B} N} = N$
27	19 26	breqtrrd	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ) \to N \leq B^{\log_{B} N}$
28	27	3adant3	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to N \leq B^{\log_{B} N}$
29		eluz2	$⊢ K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)} \leftrightarrow (⌊\log_{B} N⌋ + 1 \in ℤ \land K \in ℤ \land ⌊\log_{B} N⌋ + 1 \leq K)$
30	12	adantl	$⊢ ((⌊\log_{B} N⌋ + 1 \in ℤ \land K \in ℤ) \land (B \in ℤ_{\geq 2} \land N \in ℕ)) \to \log_{B} N \in ℝ$
31		flltp1	$⊢ \log_{B} N \in ℝ \to \log_{B} N < ⌊\log_{B} N⌋ + 1$
32	30 31	syl	$⊢ ((⌊\log_{B} N⌋ + 1 \in ℤ \land K \in ℤ) \land (B \in ℤ_{\geq 2} \land N \in ℕ)) \to \log_{B} N < ⌊\log_{B} N⌋ + 1$
33		zre	$⊢ ⌊\log_{B} N⌋ + 1 \in ℤ \to ⌊\log_{B} N⌋ + 1 \in ℝ$
34	33	adantr	$⊢ (⌊\log_{B} N⌋ + 1 \in ℤ \land K \in ℤ) \to ⌊\log_{B} N⌋ + 1 \in ℝ$
35	34	adantr	$⊢ ((⌊\log_{B} N⌋ + 1 \in ℤ \land K \in ℤ) \land (B \in ℤ_{\geq 2} \land N \in ℕ)) \to ⌊\log_{B} N⌋ + 1 \in ℝ$
36		zre	$⊢ K \in ℤ \to K \in ℝ$
37	36	adantl	$⊢ (⌊\log_{B} N⌋ + 1 \in ℤ \land K \in ℤ) \to K \in ℝ$
38	37	adantr	$⊢ ((⌊\log_{B} N⌋ + 1 \in ℤ \land K \in ℤ) \land (B \in ℤ_{\geq 2} \land N \in ℕ)) \to K \in ℝ$
39		ltletr	$⊢ (\log_{B} N \in ℝ \land ⌊\log_{B} N⌋ + 1 \in ℝ \land K \in ℝ) \to ((\log_{B} N < ⌊\log_{B} N⌋ + 1 \land ⌊\log_{B} N⌋ + 1 \leq K) \to \log_{B} N < K)$
40	30 35 38 39	syl3anc	$⊢ ((⌊\log_{B} N⌋ + 1 \in ℤ \land K \in ℤ) \land (B \in ℤ_{\geq 2} \land N \in ℕ)) \to ((\log_{B} N < ⌊\log_{B} N⌋ + 1 \land ⌊\log_{B} N⌋ + 1 \leq K) \to \log_{B} N < K)$
41	32 40	mpand	$⊢ ((⌊\log_{B} N⌋ + 1 \in ℤ \land K \in ℤ) \land (B \in ℤ_{\geq 2} \land N \in ℕ)) \to (⌊\log_{B} N⌋ + 1 \leq K \to \log_{B} N < K)$
42	41	ex	$⊢ (⌊\log_{B} N⌋ + 1 \in ℤ \land K \in ℤ) \to ((B \in ℤ_{\geq 2} \land N \in ℕ) \to (⌊\log_{B} N⌋ + 1 \leq K \to \log_{B} N < K))$
43	42	com23	$⊢ (⌊\log_{B} N⌋ + 1 \in ℤ \land K \in ℤ) \to (⌊\log_{B} N⌋ + 1 \leq K \to ((B \in ℤ_{\geq 2} \land N \in ℕ) \to \log_{B} N < K))$
44	43	3impia	$⊢ (⌊\log_{B} N⌋ + 1 \in ℤ \land K \in ℤ \land ⌊\log_{B} N⌋ + 1 \leq K) \to ((B \in ℤ_{\geq 2} \land N \in ℕ) \to \log_{B} N < K)$
45	44	com12	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ) \to ((⌊\log_{B} N⌋ + 1 \in ℤ \land K \in ℤ \land ⌊\log_{B} N⌋ + 1 \leq K) \to \log_{B} N < K)$
46	29 45	biimtrid	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ) \to (K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)} \to \log_{B} N < K)$
47	46	3impia	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to \log_{B} N < K$
48		eluz2gt1	$⊢ B \in ℤ_{\geq 2} \to 1 < B$
49	3 48	jca	$⊢ B \in ℤ_{\geq 2} \to (B \in ℝ \land 1 < B)$
50	49	3ad2ant1	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to (B \in ℝ \land 1 < B)$
51		cxplt	$⊢ ((B \in ℝ \land 1 < B) \land (\log_{B} N \in ℝ \land K \in ℝ)) \to (\log_{B} N < K \leftrightarrow B^{\log_{B} N} < B^{K})$
52	50 13 16 51	syl12anc	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to (\log_{B} N < K \leftrightarrow B^{\log_{B} N} < B^{K})$
53	47 52	mpbid	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to B^{\log_{B} N} < B^{K}$
54	2 14 17 28 53	lelttrd	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to N < B^{K}$
55		eluzelcn	$⊢ B \in ℤ_{\geq 2} \to B \in ℂ$
56	55	3ad2ant1	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to B \in ℂ$
57		eluz2n0	$⊢ B \in ℤ_{\geq 2} \to B \neq 0$
58	57	3ad2ant1	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to B \neq 0$
59		eluzelz	$⊢ K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)} \to K \in ℤ$
60	59	3ad2ant3	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to K \in ℤ$
61		cxpexpz	$⊢ (B \in ℂ \land B \neq 0 \land K \in ℤ) \to B^{K} = B^{K}$
62	61	breq2d	$⊢ (B \in ℂ \land B \neq 0 \land K \in ℤ) \to (N < B^{K} \leftrightarrow N < B^{K})$
63	56 58 60 62	syl3anc	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to (N < B^{K} \leftrightarrow N < B^{K})$
64	54 63	mpbid	$⊢ (B \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{B} N⌋ + 1)}) \to N < B^{K}$

Metamath Proof Explorer

Theorem dignn0ldlem

Proof