efexple

Description: Convert a bound on a power to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014)

		Ref	Expression
	Assertion	efexple	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to (A^{N} \leq B \leftrightarrow N \leq ⌊\frac{\log B}{\log A}⌋)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ℝ \land 1 < A) \to A \in ℝ$
2		0lt1	$⊢ 0 < 1$
3		0re	$⊢ 0 \in ℝ$
4		1re	$⊢ 1 \in ℝ$
5		lttr	$⊢ (0 \in ℝ \land 1 \in ℝ \land A \in ℝ) \to ((0 < 1 \land 1 < A) \to 0 < A)$
6	3 4 5	mp3an12	$⊢ A \in ℝ \to ((0 < 1 \land 1 < A) \to 0 < A)$
7	2 6	mpani	$⊢ A \in ℝ \to (1 < A \to 0 < A)$
8	7	imp	$⊢ (A \in ℝ \land 1 < A) \to 0 < A$
9	1 8	elrpd	$⊢ (A \in ℝ \land 1 < A) \to A \in ℝ^{+}$
10	9	3ad2ant1	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to A \in ℝ^{+}$
11		simp2	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to N \in ℤ$
12		reexplog	$⊢ (A \in ℝ^{+} \land N \in ℤ) \to A^{N} = e^{N \log A}$
13	10 11 12	syl2anc	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to A^{N} = e^{N \log A}$
14		reeflog	$⊢ B \in ℝ^{+} \to e^{\log B} = B$
15	14	3ad2ant3	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to e^{\log B} = B$
16	15	eqcomd	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to B = e^{\log B}$
17	13 16	breq12d	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to (A^{N} \leq B \leftrightarrow e^{N \log A} \leq e^{\log B})$
18		zre	$⊢ N \in ℤ \to N \in ℝ$
19	18	3ad2ant2	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to N \in ℝ$
20		rplogcl	$⊢ (A \in ℝ \land 1 < A) \to \log A \in ℝ^{+}$
21	20	3ad2ant1	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to \log A \in ℝ^{+}$
22	21	rpred	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to \log A \in ℝ$
23	19 22	remulcld	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to N \log A \in ℝ$
24		relogcl	$⊢ B \in ℝ^{+} \to \log B \in ℝ$
25	24	3ad2ant3	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to \log B \in ℝ$
26		efle	$⊢ (N \log A \in ℝ \land \log B \in ℝ) \to (N \log A \leq \log B \leftrightarrow e^{N \log A} \leq e^{\log B})$
27	23 25 26	syl2anc	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to (N \log A \leq \log B \leftrightarrow e^{N \log A} \leq e^{\log B})$
28	19 25 21	lemuldivd	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to (N \log A \leq \log B \leftrightarrow N \leq \frac{\log B}{\log A})$
29	25 21	rerpdivcld	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to \frac{\log B}{\log A} \in ℝ$
30		flge	$⊢ (\frac{\log B}{\log A} \in ℝ \land N \in ℤ) \to (N \leq \frac{\log B}{\log A} \leftrightarrow N \leq ⌊\frac{\log B}{\log A}⌋)$
31	29 11 30	syl2anc	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to (N \leq \frac{\log B}{\log A} \leftrightarrow N \leq ⌊\frac{\log B}{\log A}⌋)$
32	28 31	bitrd	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to (N \log A \leq \log B \leftrightarrow N \leq ⌊\frac{\log B}{\log A}⌋)$
33	17 27 32	3bitr2d	$⊢ ((A \in ℝ \land 1 < A) \land N \in ℤ \land B \in ℝ^{+}) \to (A^{N} \leq B \leftrightarrow N \leq ⌊\frac{\log B}{\log A}⌋)$

Metamath Proof Explorer

Theorem efexple

Proof