relogbf

Description: The general logarithm to a real base greater than 1 regarded as function restricted to the positive integers. Property in Cohen4 p. 349. (Contributed by AV, 12-Jun-2020)

		Ref	Expression
	Assertion	relogbf	$⊢ (B \in ℝ^{+} \land 1 < B) \to ({curry logb (B) ↾}_{ℝ^{+}}) : ℝ^{+} ⟶ ℝ$

Proof

Step	Hyp	Ref	Expression
1		rpcndif0	$⊢ x \in ℝ^{+} \to x \in (ℂ ∖ \{0\})$
2	1	adantl	$⊢ ((B \in ℝ^{+} \land 1 < B) \land x \in ℝ^{+}) \to x \in (ℂ ∖ \{0\})$
3		rpcn	$⊢ B \in ℝ^{+} \to B \in ℂ$
4	3	adantr	$⊢ (B \in ℝ^{+} \land 1 < B) \to B \in ℂ$
5		rpne0	$⊢ B \in ℝ^{+} \to B \neq 0$
6	5	adantr	$⊢ (B \in ℝ^{+} \land 1 < B) \to B \neq 0$
7		animorr	$⊢ (B \in ℝ^{+} \land 1 < B) \to (B < 1 \lor 1 < B)$
8		rpre	$⊢ B \in ℝ^{+} \to B \in ℝ$
9		1red	$⊢ 1 < B \to 1 \in ℝ$
10		lttri2	$⊢ (B \in ℝ \land 1 \in ℝ) \to (B \neq 1 \leftrightarrow (B < 1 \lor 1 < B))$
11	8 9 10	syl2an	$⊢ (B \in ℝ^{+} \land 1 < B) \to (B \neq 1 \leftrightarrow (B < 1 \lor 1 < B))$
12	7 11	mpbird	$⊢ (B \in ℝ^{+} \land 1 < B) \to B \neq 1$
13	4 6 12	3jca	$⊢ (B \in ℝ^{+} \land 1 < B) \to (B \in ℂ \land B \neq 0 \land B \neq 1)$
14		logbmpt	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to curry logb (B) = (x \in (ℂ ∖ \{0\}) ⟼ \frac{\log x}{\log B})$
15	13 14	syl	$⊢ (B \in ℝ^{+} \land 1 < B) \to curry logb (B) = (x \in (ℂ ∖ \{0\}) ⟼ \frac{\log x}{\log B})$
16	15	dmeqd	$⊢ (B \in ℝ^{+} \land 1 < B) \to dom curry logb (B) = dom (x \in (ℂ ∖ \{0\}) ⟼ \frac{\log x}{\log B})$
17		ovexd	$⊢ ((B \in ℝ^{+} \land 1 < B) \land x \in (ℂ ∖ \{0\})) \to \frac{\log x}{\log B} \in V$
18	17	ralrimiva	$⊢ (B \in ℝ^{+} \land 1 < B) \to \forall x \in (ℂ ∖ \{0\}) \frac{\log x}{\log B} \in V$
19		dmmptg	$⊢ \forall x \in (ℂ ∖ \{0\}) \frac{\log x}{\log B} \in V \to dom (x \in (ℂ ∖ \{0\}) ⟼ \frac{\log x}{\log B}) = ℂ ∖ \{0\}$
20	18 19	syl	$⊢ (B \in ℝ^{+} \land 1 < B) \to dom (x \in (ℂ ∖ \{0\}) ⟼ \frac{\log x}{\log B}) = ℂ ∖ \{0\}$
21	16 20	eqtrd	$⊢ (B \in ℝ^{+} \land 1 < B) \to dom curry logb (B) = ℂ ∖ \{0\}$
22	21	adantr	$⊢ ((B \in ℝ^{+} \land 1 < B) \land x \in ℝ^{+}) \to dom curry logb (B) = ℂ ∖ \{0\}$
23	2 22	eleqtrrd	$⊢ ((B \in ℝ^{+} \land 1 < B) \land x \in ℝ^{+}) \to x \in dom curry logb (B)$
24		logbfval	$⊢ ((B \in ℂ \land B \neq 0 \land B \neq 1) \land x \in (ℂ ∖ \{0\})) \to curry logb (B) (x) = \log_{B} x$
25	13 1 24	syl2an	$⊢ ((B \in ℝ^{+} \land 1 < B) \land x \in ℝ^{+}) \to curry logb (B) (x) = \log_{B} x$
26		simpll	$⊢ ((B \in ℝ^{+} \land 1 < B) \land x \in ℝ^{+}) \to B \in ℝ^{+}$
27		simpr	$⊢ ((B \in ℝ^{+} \land 1 < B) \land x \in ℝ^{+}) \to x \in ℝ^{+}$
28	12	adantr	$⊢ ((B \in ℝ^{+} \land 1 < B) \land x \in ℝ^{+}) \to B \neq 1$
29	26 27 28	3jca	$⊢ ((B \in ℝ^{+} \land 1 < B) \land x \in ℝ^{+}) \to (B \in ℝ^{+} \land x \in ℝ^{+} \land B \neq 1)$
30		relogbcl	$⊢ (B \in ℝ^{+} \land x \in ℝ^{+} \land B \neq 1) \to \log_{B} x \in ℝ$
31	29 30	syl	$⊢ ((B \in ℝ^{+} \land 1 < B) \land x \in ℝ^{+}) \to \log_{B} x \in ℝ$
32	25 31	eqeltrd	$⊢ ((B \in ℝ^{+} \land 1 < B) \land x \in ℝ^{+}) \to curry logb (B) (x) \in ℝ$
33	23 32	jca	$⊢ ((B \in ℝ^{+} \land 1 < B) \land x \in ℝ^{+}) \to (x \in dom curry logb (B) \land curry logb (B) (x) \in ℝ)$
34	33	ralrimiva	$⊢ (B \in ℝ^{+} \land 1 < B) \to \forall x \in ℝ^{+} (x \in dom curry logb (B) \land curry logb (B) (x) \in ℝ)$
35		logbf	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to curry logb (B) : ℂ ∖ \{0\} ⟶ ℂ$
36		ffun	$⊢ curry logb (B) : ℂ ∖ \{0\} ⟶ ℂ \to Fun curry logb (B)$
37		ffvresb	$⊢ Fun curry logb (B) \to (({curry logb (B) ↾}_{ℝ^{+}}) : ℝ^{+} ⟶ ℝ \leftrightarrow \forall x \in ℝ^{+} (x \in dom curry logb (B) \land curry logb (B) (x) \in ℝ))$
38	13 35 36 37	4syl	$⊢ (B \in ℝ^{+} \land 1 < B) \to (({curry logb (B) ↾}_{ℝ^{+}}) : ℝ^{+} ⟶ ℝ \leftrightarrow \forall x \in ℝ^{+} (x \in dom curry logb (B) \land curry logb (B) (x) \in ℝ))$
39	34 38	mpbird	$⊢ (B \in ℝ^{+} \land 1 < B) \to ({curry logb (B) ↾}_{ℝ^{+}}) : ℝ^{+} ⟶ ℝ$

Metamath Proof Explorer

Theorem relogbf

Proof