P. 267 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26601-26700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	logno1 26601	The logarithm function is not eventually bounded. (Contributed by Mario Carneiro, 30-Apr-2016.) (Proof shortened by Mario Carneiro, 30-May-2016.)
⊢ ¬ (𝑥 ∈ ℝ+ ↦ (log‘𝑥)) ∈ 𝑂(1)
Theorem	dvrelog 26602	The derivative of the real logarithm function. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (ℝ D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))
Theorem	relogcn 26603	The real logarithm function is continuous. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ (log ↾ ℝ+) ∈ (ℝ+–cn→ℝ)
Theorem	ellogdm 26604	Elementhood in the "continuous domain" of the complex logarithm. (Contributed by Mario Carneiro, 18-Feb-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    ⇒   ⊢ (𝐴 ∈ 𝐷 ↔ (𝐴 ∈ ℂ ∧ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ+)))
Theorem	logdmn0 26605	A number in the continuous domain of log is nonzero. (Contributed by Mario Carneiro, 18-Feb-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    ⇒   ⊢ (𝐴 ∈ 𝐷 → 𝐴 ≠ 0)
Theorem	logdmnrp 26606	A number in the continuous domain of log is not a strictly negative number. (Contributed by Mario Carneiro, 18-Feb-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    ⇒   ⊢ (𝐴 ∈ 𝐷 → ¬ -𝐴 ∈ ℝ+)
Theorem	logdmss 26607	The continuity domain of log is a subset of the regular domain of log. (Contributed by Mario Carneiro, 1-Mar-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    ⇒   ⊢ 𝐷 ⊆ (ℂ ∖ {0})
Theorem	logcnlem2 26608	Lemma for logcn 26612. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴)))    &   ⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    ⇒   ⊢ (𝜑 → if(𝑆 ≤ 𝑇, 𝑆, 𝑇) ∈ ℝ+)
Theorem	logcnlem3 26609	Lemma for logcn 26612. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴)))    &   ⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < if(𝑆 ≤ 𝑇, 𝑆, 𝑇))    ⇒   ⊢ (𝜑 → (-π < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ∧ ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π))
Theorem	logcnlem4 26610	Lemma for logcn 26612. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴)))    &   ⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < if(𝑆 ≤ 𝑇, 𝑆, 𝑇))    ⇒   ⊢ (𝜑 → (abs‘((ℑ‘(log‘𝐴)) − (ℑ‘(log‘𝐵)))) < 𝑅)
Theorem	logcnlem5 26611*	Lemma for logcn 26612. (Contributed by Mario Carneiro, 18-Feb-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    ⇒   ⊢ (𝑥 ∈ 𝐷 ↦ (ℑ‘(log‘𝑥))) ∈ (𝐷–cn→ℝ)
Theorem	logcn 26612	The logarithm function is continuous away from the branch cut at negative reals. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    ⇒   ⊢ (log ↾ 𝐷) ∈ (𝐷–cn→ℂ)
Theorem	dvloglem 26613	Lemma for dvlog 26616. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    ⇒   ⊢ (log “ 𝐷) ∈ (TopOpen‘ℂfld)
Theorem	logdmopn 26614	The "continuous domain" of log is an open set. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    ⇒   ⊢ 𝐷 ∈ (TopOpen‘ℂfld)
Theorem	logf1o2 26615	The logarithm maps its continuous domain bijectively onto the set of numbers with imaginary part -π < ℑ(𝑧) < π. The negative reals are mapped to the numbers with imaginary part equal to π. (Contributed by Mario Carneiro, 2-May-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    ⇒   ⊢ (log ↾ 𝐷):𝐷–1-1-onto→(◡ℑ “ (-π(,)π))
Theorem	dvlog 26616*	The derivative of the complex logarithm function. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    ⇒   ⊢ (ℂ D (log ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥))
Theorem	dvlog2lem 26617	Lemma for dvlog2 26618. (Contributed by Mario Carneiro, 1-Mar-2015.)
⊢ 𝑆 = (1(ball‘(abs ∘ − ))1)    ⇒   ⊢ 𝑆 ⊆ (ℂ ∖ (-∞(,]0))
Theorem	dvlog2 26618*	The derivative of the complex logarithm function on the open unit ball centered at 1, a sometimes easier region to work with than the ℂ ∖ (-∞, 0] of dvlog 26616. (Contributed by Mario Carneiro, 1-Mar-2015.)
⊢ 𝑆 = (1(ball‘(abs ∘ − ))1)    ⇒   ⊢ (ℂ D (log ↾ 𝑆)) = (𝑥 ∈ 𝑆 ↦ (1 / 𝑥))
Theorem	advlog 26619	The antiderivative of the logarithm. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥))
Theorem	advlogexp 26620*	The antiderivative of a power of the logarithm. (Set 𝐴 = 1 and multiply by (-1)↑𝑁 · 𝑁! to get the antiderivative of log(𝑥)↑𝑁 itself.) (Contributed by Mario Carneiro, 22-May-2016.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) = (𝑥 ∈ ℝ+ ↦ (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁))))
Theorem	efopnlem1 26621	Lemma for efopn 26623. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)
⊢ (((𝑅 ∈ ℝ+ ∧ 𝑅 < π) ∧ 𝐴 ∈ (0(ball‘(abs ∘ − ))𝑅)) → (abs‘(ℑ‘𝐴)) < π)
Theorem	efopnlem2 26622	Lemma for efopn 26623. (Contributed by Mario Carneiro, 2-May-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ ((𝑅 ∈ ℝ+ ∧ 𝑅 < π) → (exp “ (0(ball‘(abs ∘ − ))𝑅)) ∈ 𝐽)
Theorem	efopn 26623	The exponential map is an open map. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑆 ∈ 𝐽 → (exp “ 𝑆) ∈ 𝐽)
Theorem	logtayllem 26624*	Lemma for logtayl 26625. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))) ∈ dom ⇝ )
Theorem	logtayl 26625*	The Taylor series for -log(1 − 𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴↑𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴)))
Theorem	logtaylsum 26626*	The Taylor series for -log(1 − 𝐴), as an infinite sum. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → Σ𝑘 ∈ ℕ ((𝐴↑𝑘) / 𝑘) = -(log‘(1 − 𝐴)))
Theorem	logtayl2 26627*	Power series expression for the logarithm. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ 𝑆 = (1(ball‘(abs ∘ − ))1)    ⇒   ⊢ (𝐴 ∈ 𝑆 → seq1( + , (𝑘 ∈ ℕ ↦ (((-1↑(𝑘 − 1)) / 𝑘) · ((𝐴 − 1)↑𝑘)))) ⇝ (log‘𝐴))
Theorem	logccv 26628	The natural logarithm function on the reals is a strictly concave function. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0(,)1)) → ((𝑇 · (log‘𝐴)) + ((1 − 𝑇) · (log‘𝐵))) < (log‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))))
Theorem	cxpval 26629	Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) = if(𝐴 = 0, if(𝐵 = 0, 1, 0), (exp‘(𝐵 · (log‘𝐴)))))
Theorem	cxpef 26630	Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴))))
Theorem	0cxp 26631	Value of the complex power function when the first argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (0↑𝑐𝐴) = 0)
Theorem	cxpexpz 26632	Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℤ) → (𝐴↑𝑐𝐵) = (𝐴↑𝐵))
Theorem	cxpexp 26633	Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝑐𝐵) = (𝐴↑𝐵))
Theorem	logcxp 26634	Logarithm of a complex power. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴)))
Theorem	cxp0 26635	Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ (𝐴 ∈ ℂ → (𝐴↑𝑐0) = 1)
Theorem	cxp1 26636	Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ (𝐴 ∈ ℂ → (𝐴↑𝑐1) = 𝐴)
Theorem	1cxp 26637	Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ (𝐴 ∈ ℂ → (1↑𝑐𝐴) = 1)
Theorem	ecxp 26638	Write the exponential function as an exponent to the power e. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ (𝐴 ∈ ℂ → (e↑𝑐𝐴) = (exp‘𝐴))
Theorem	cxpcl 26639	Closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) ∈ ℂ)
Theorem	recxpcl 26640	Real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ) → (𝐴↑𝑐𝐵) ∈ ℝ)
Theorem	rpcxpcl 26641	Positive real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (𝐴↑𝑐𝐵) ∈ ℝ+)
Theorem	cxpne0 26642	Complex exponentiation is nonzero if its base is nonzero. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) ≠ 0)
Theorem	cxpeq0 26643	Complex exponentiation is zero iff the base is zero and the exponent is nonzero. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑐𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 ≠ 0)))
Theorem	cxpadd 26644	Sum of exponents law for complex exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴↑𝑐(𝐵 + 𝐶)) = ((𝐴↑𝑐𝐵) · (𝐴↑𝑐𝐶)))
Theorem	cxpp1 26645	Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐(𝐵 + 1)) = ((𝐴↑𝑐𝐵) · 𝐴))
Theorem	cxpneg 26646	Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐-𝐵) = (1 / (𝐴↑𝑐𝐵)))
Theorem	cxpsub 26647	Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴↑𝑐(𝐵 − 𝐶)) = ((𝐴↑𝑐𝐵) / (𝐴↑𝑐𝐶)))
Theorem	cxpge0 26648	Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ) → 0 ≤ (𝐴↑𝑐𝐵))
Theorem	mulcxplem 26649	Lemma for mulcxp 26650. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (0↑𝑐𝐶) = ((𝐴↑𝑐𝐶) · (0↑𝑐𝐶)))
Theorem	mulcxp 26650	Complex exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) · (𝐵↑𝑐𝐶)))
Theorem	cxprec 26651	Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → ((1 / 𝐴)↑𝑐𝐵) = (1 / (𝐴↑𝑐𝐵)))
Theorem	divcxp 26652	Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) / (𝐵↑𝑐𝐶)))
Theorem	cxpmul 26653	Product of exponents law for complex exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ) → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝑐𝐶))
Theorem	cxpmul2 26654	Product of exponents law for complex exponentiation. Variation on cxpmul 26653 with more general conditions on 𝐴 and 𝐵 when 𝐶 is a nonnegative integer. (Contributed by Mario Carneiro, 9-Aug-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℕ0) → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶))
Theorem	cxproot 26655	The complex power function allows to write n-th roots via the idiom 𝐴↑𝑐(1 / 𝑁). (Contributed by Mario Carneiro, 6-May-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑐(1 / 𝑁))↑𝑁) = 𝐴)
Theorem	cxpmul2z 26656	Generalize cxpmul2 26654 to negative integers. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℤ)) → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶))
Theorem	abscxp 26657	Absolute value of a power, when the base is real. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴↑𝑐𝐵)) = (𝐴↑𝑐(ℜ‘𝐵)))
Theorem	abscxp2 26658	Absolute value of a power, when the exponent is real. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ) → (abs‘(𝐴↑𝑐𝐵)) = ((abs‘𝐴)↑𝑐𝐵))
Theorem	cxplt 26659	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐵) < (𝐴↑𝑐𝐶)))
Theorem	cxple 26660	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶)))
Theorem	cxplea 26661	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ≤ 𝐶) → (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶))
Theorem	cxple2 26662	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶)))
Theorem	cxplt2 26663	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐴↑𝑐𝐶) < (𝐵↑𝑐𝐶)))
Theorem	cxple2a 26664	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐶) ∧ 𝐴 ≤ 𝐵) → (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶))
Theorem	cxplt3 26665	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐴 < 1) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐶) < (𝐴↑𝑐𝐵)))
Theorem	cxple3 26666	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐴 < 1) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐶) ≤ (𝐴↑𝑐𝐵)))
Theorem	cxpsqrtlem 26667	Lemma for cxpsqrt 26668. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 / 2)) = -(√‘𝐴)) → (i · (√‘𝐴)) ∈ ℝ)
Theorem	cxpsqrt 26668	The complex exponential function with exponent 1 / 2 exactly matches the complex square root function (the branch cut is in the same place for both functions), and thus serves as a suitable generalization to other 𝑛-th roots and irrational roots. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ (𝐴 ∈ ℂ → (𝐴↑𝑐(1 / 2)) = (√‘𝐴))
Theorem	logsqrt 26669	Logarithm of a square root. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ (𝐴 ∈ ℝ+ → (log‘(√‘𝐴)) = ((log‘𝐴) / 2))
Theorem	cxp0d 26670	Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐0) = 1)
Theorem	cxp1d 26671	Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐1) = 𝐴)
Theorem	1cxpd 26672	Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (1↑𝑐𝐴) = 1)
Theorem	cxpcld 26673	Closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℂ)
Theorem	cxpmul2d 26674	Product of exponents law for complex exponentiation. Variation on cxpmul 26653 with more general conditions on 𝐴 and 𝐵 when 𝐶 is a nonnegative integer. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶))
Theorem	0cxpd 26675	Value of the complex power function when the first argument is zero. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (0↑𝑐𝐴) = 0)
Theorem	cxpexpzd 26676	Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐𝐵) = (𝐴↑𝐵))
Theorem	cxpefd 26677	Value of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴))))
Theorem	cxpne0d 26678	Complex exponentiation is nonzero if its base is nonzero. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐𝐵) ≠ 0)
Theorem	cxpp1d 26679	Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐(𝐵 + 1)) = ((𝐴↑𝑐𝐵) · 𝐴))
Theorem	cxpnegd 26680	Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐-𝐵) = (1 / (𝐴↑𝑐𝐵)))
Theorem	cxpmul2zd 26681	Generalize cxpmul2 26654 to negative integers. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶))
Theorem	cxpaddd 26682	Sum of exponents law for complex exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐(𝐵 + 𝐶)) = ((𝐴↑𝑐𝐵) · (𝐴↑𝑐𝐶)))
Theorem	cxpsubd 26683	Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐(𝐵 − 𝐶)) = ((𝐴↑𝑐𝐵) / (𝐴↑𝑐𝐶)))
Theorem	cxpltd 26684	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐵) < (𝐴↑𝑐𝐶)))
Theorem	cxpled 26685	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶)))
Theorem	cxplead 26686	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 1 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶))
Theorem	divcxpd 26687	Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) / (𝐵↑𝑐𝐶)))
Theorem	recxpcld 26688	Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℝ)
Theorem	cxpge0d 26689	Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴↑𝑐𝐵))
Theorem	cxple2ad 26690	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶))
Theorem	cxplt2d 26691	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴↑𝑐𝐶) < (𝐵↑𝑐𝐶)))
Theorem	cxple2d 26692	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶)))
Theorem	mulcxpd 26693	Complex exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) · (𝐵↑𝑐𝐶)))
Theorem	recxpf1lem 26694	Complex exponentiation on positive real numbers is a one-to-one function. (Contributed by Thierry Arnoux, 1-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴↑𝑐𝐶) = (𝐵↑𝑐𝐶)))
Theorem	cxpsqrtth 26695	Square root theorem over the complex numbers for the complex power function. Theorem I.35 of [Apostol] p. 29. Compare with sqrtth 15288. (Contributed by AV, 23-Dec-2022.)
⊢ (𝐴 ∈ ℂ → ((√‘𝐴)↑𝑐2) = 𝐴)
Theorem	2irrexpq 26696*	There exist irrational numbers 𝑎 and 𝑏 such that (𝑎↑𝑐𝑏) is rational. Statement in the Metamath book, section 1.1.5, footnote 27 on page 17, and the "classical proof" for theorem 1.2 of [Bauer], p. 483. This proof is not acceptable in intuitionistic logic, since it is based on the law of excluded middle: Either ((√‘2)↑𝑐(√‘2)) is rational, in which case (√‘2), being irrational (see sqrt2irr 16174), can be chosen for both 𝑎 and 𝑏, or ((√‘2)↑𝑐(√‘2)) is irrational, in which case ((√‘2)↑𝑐(√‘2)) can be chosen for 𝑎 and (√‘2) for 𝑏, since (((√‘2)↑𝑐(√‘2))↑𝑐(√‘2)) = 2 is rational. For an alternate proof, which can be used in intuitionistic logic, see 2irrexpqALT 26766. (Contributed by AV, 23-Dec-2022.)
⊢ ∃𝑎 ∈ (ℝ ∖ ℚ)∃𝑏 ∈ (ℝ ∖ ℚ)(𝑎↑𝑐𝑏) ∈ ℚ
Theorem	cxprecd 26697	Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((1 / 𝐴)↑𝑐𝐵) = (1 / (𝐴↑𝑐𝐵)))
Theorem	rpcxpcld 26698	Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℝ+)
Theorem	logcxpd 26699	Logarithm of a complex power. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴)))
Theorem	cxplt3d 26700	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐶) < (𝐴↑𝑐𝐵)))