logbgt0b

Description: The logarithm of a positive real number to a real base greater than 1 is positive iff the number is greater than 1. (Contributed by AV, 29-Dec-2022)

		Ref	Expression
	Assertion	logbgt0b	$⊢ (A \in ℝ^{+} \land (B \in ℝ^{+} \land 1 < B)) \to (0 < \log_{B} A \leftrightarrow 1 < A)$

Proof

Step	Hyp	Ref	Expression
1		rpcn	$⊢ B \in ℝ^{+} \to B \in ℂ$
2	1	adantr	$⊢ (B \in ℝ^{+} \land 1 < B) \to B \in ℂ$
3		rpne0	$⊢ B \in ℝ^{+} \to B \neq 0$
4	3	adantr	$⊢ (B \in ℝ^{+} \land 1 < B) \to B \neq 0$
5		1red	$⊢ B \in ℝ^{+} \to 1 \in ℝ$
6		ltne	$⊢ (1 \in ℝ \land 1 < B) \to B \neq 1$
7	5 6	sylan	$⊢ (B \in ℝ^{+} \land 1 < B) \to B \neq 1$
8		eldifpr	$⊢ B \in (ℂ ∖ \{0, 1\}) \leftrightarrow (B \in ℂ \land B \neq 0 \land B \neq 1)$
9	2 4 7 8	syl3anbrc	$⊢ (B \in ℝ^{+} \land 1 < B) \to B \in (ℂ ∖ \{0, 1\})$
10		rpcndif0	$⊢ A \in ℝ^{+} \to A \in (ℂ ∖ \{0\})$
11		logbval	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land A \in (ℂ ∖ \{0\})) \to \log_{B} A = \frac{\log A}{\log B}$
12	9 10 11	syl2anr	$⊢ (A \in ℝ^{+} \land (B \in ℝ^{+} \land 1 < B)) \to \log_{B} A = \frac{\log A}{\log B}$
13	12	breq2d	$⊢ (A \in ℝ^{+} \land (B \in ℝ^{+} \land 1 < B)) \to (0 < \log_{B} A \leftrightarrow 0 < \frac{\log A}{\log B})$
14		relogcl	$⊢ A \in ℝ^{+} \to \log A \in ℝ$
15	14	adantr	$⊢ (A \in ℝ^{+} \land (B \in ℝ^{+} \land 1 < B)) \to \log A \in ℝ$
16		relogcl	$⊢ B \in ℝ^{+} \to \log B \in ℝ$
17	16	adantr	$⊢ (B \in ℝ^{+} \land 1 < B) \to \log B \in ℝ$
18	17	adantl	$⊢ (A \in ℝ^{+} \land (B \in ℝ^{+} \land 1 < B)) \to \log B \in ℝ$
19		loggt0b	$⊢ B \in ℝ^{+} \to (0 < \log B \leftrightarrow 1 < B)$
20	19	biimpar	$⊢ (B \in ℝ^{+} \land 1 < B) \to 0 < \log B$
21	20	adantl	$⊢ (A \in ℝ^{+} \land (B \in ℝ^{+} \land 1 < B)) \to 0 < \log B$
22		gt0div	$⊢ (\log A \in ℝ \land \log B \in ℝ \land 0 < \log B) \to (0 < \log A \leftrightarrow 0 < \frac{\log A}{\log B})$
23	15 18 21 22	syl3anc	$⊢ (A \in ℝ^{+} \land (B \in ℝ^{+} \land 1 < B)) \to (0 < \log A \leftrightarrow 0 < \frac{\log A}{\log B})$
24		loggt0b	$⊢ A \in ℝ^{+} \to (0 < \log A \leftrightarrow 1 < A)$
25	24	adantr	$⊢ (A \in ℝ^{+} \land (B \in ℝ^{+} \land 1 < B)) \to (0 < \log A \leftrightarrow 1 < A)$
26	13 23 25	3bitr2d	$⊢ (A \in ℝ^{+} \land (B \in ℝ^{+} \land 1 < B)) \to (0 < \log_{B} A \leftrightarrow 1 < A)$

Metamath Proof Explorer

Theorem logbgt0b

Proof