Home | Metamath
Proof Explorer Theorem List (p. 253 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44899) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | reeflogd 25201 | Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (exp‘(log‘𝐴)) = 𝐴) | ||
Theorem | relogmuld 25202 | The natural logarithm of the product of two positive real numbers is the sum of natural logarithms. Property 2 of [Cohen] p. 301, restricted to natural logarithms. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (log‘(𝐴 · 𝐵)) = ((log‘𝐴) + (log‘𝐵))) | ||
Theorem | relogdivd 25203 | The natural logarithm of the quotient of two positive real numbers is the difference of natural logarithms. Exercise 72(a) and Property 3 of [Cohen] p. 301, restricted to natural logarithms. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (log‘(𝐴 / 𝐵)) = ((log‘𝐴) − (log‘𝐵))) | ||
Theorem | logled 25204 | Natural logarithm preserves ≤. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (log‘𝐴) ≤ (log‘𝐵))) | ||
Theorem | relogefd 25205 | Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (log‘(exp‘𝐴)) = 𝐴) | ||
Theorem | rplogcld 25206 | Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 < 𝐴) ⇒ ⊢ (𝜑 → (log‘𝐴) ∈ ℝ+) | ||
Theorem | logge0d 25207 | The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 ≤ 𝐴) ⇒ ⊢ (𝜑 → 0 ≤ (log‘𝐴)) | ||
Theorem | logge0b 25208 | The logarithm of a number is nonnegative iff the number is greater than or equal to 1. (Contributed by AV, 30-May-2020.) |
⊢ (𝐴 ∈ ℝ+ → (0 ≤ (log‘𝐴) ↔ 1 ≤ 𝐴)) | ||
Theorem | loggt0b 25209 | The logarithm of a number is positive iff the number is greater than 1. (Contributed by AV, 30-May-2020.) |
⊢ (𝐴 ∈ ℝ+ → (0 < (log‘𝐴) ↔ 1 < 𝐴)) | ||
Theorem | logle1b 25210 | The logarithm of a number is less than or equal to 1 iff the number is less than or equal to Euler's constant. (Contributed by AV, 30-May-2020.) |
⊢ (𝐴 ∈ ℝ+ → ((log‘𝐴) ≤ 1 ↔ 𝐴 ≤ e)) | ||
Theorem | loglt1b 25211 | The logarithm of a number is less than 1 iff the number is less than Euler's constant. (Contributed by AV, 30-May-2020.) |
⊢ (𝐴 ∈ ℝ+ → ((log‘𝐴) < 1 ↔ 𝐴 < e)) | ||
Theorem | divlogrlim 25212 | The inverse logarithm function converges to zero. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝𝑟 0 | ||
Theorem | logno1 25213 | 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 25214 | The derivative of the real logarithm function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (ℝ D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) | ||
Theorem | relogcn 25215 | The real logarithm function is continuous. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ (log ↾ ℝ+) ∈ (ℝ+–cn→ℝ) | ||
Theorem | ellogdm 25216 | Elementhood in the "continuous domain" of the complex logarithm. (Contributed by Mario Carneiro, 18-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝐴 ∈ 𝐷 ↔ (𝐴 ∈ ℂ ∧ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ+))) | ||
Theorem | logdmn0 25217 | A number in the continuous domain of log is nonzero. (Contributed by Mario Carneiro, 18-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝐴 ∈ 𝐷 → 𝐴 ≠ 0) | ||
Theorem | logdmnrp 25218 | A number in the continuous domain of log is not a strictly negative number. (Contributed by Mario Carneiro, 18-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝐴 ∈ 𝐷 → ¬ -𝐴 ∈ ℝ+) | ||
Theorem | logdmss 25219 | 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 25220 | Lemma for logcn 25224. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) & ⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) ⇒ ⊢ (𝜑 → if(𝑆 ≤ 𝑇, 𝑆, 𝑇) ∈ ℝ+) | ||
Theorem | logcnlem3 25221 | Lemma for logcn 25224. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) & ⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < if(𝑆 ≤ 𝑇, 𝑆, 𝑇)) ⇒ ⊢ (𝜑 → (-π < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ∧ ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π)) | ||
Theorem | logcnlem4 25222 | Lemma for logcn 25224. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) & ⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < if(𝑆 ≤ 𝑇, 𝑆, 𝑇)) ⇒ ⊢ (𝜑 → (abs‘((ℑ‘(log‘𝐴)) − (ℑ‘(log‘𝐵)))) < 𝑅) | ||
Theorem | logcnlem5 25223* | Lemma for logcn 25224. (Contributed by Mario Carneiro, 18-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝑥 ∈ 𝐷 ↦ (ℑ‘(log‘𝑥))) ∈ (𝐷–cn→ℝ) | ||
Theorem | logcn 25224 | 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 25225 | Lemma for dvlog 25228. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (log “ 𝐷) ∈ (TopOpen‘ℂfld) | ||
Theorem | logdmopn 25226 | The "continuous domain" of log is an open set. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ 𝐷 ∈ (TopOpen‘ℂfld) | ||
Theorem | logf1o2 25227 | 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 25228* | The derivative of the complex logarithm function. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (ℂ D (log ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) | ||
Theorem | dvlog2lem 25229 | Lemma for dvlog2 25230. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ 𝑆 = (1(ball‘(abs ∘ − ))1) ⇒ ⊢ 𝑆 ⊆ (ℂ ∖ (-∞(,]0)) | ||
Theorem | dvlog2 25230* | 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 25228. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ 𝑆 = (1(ball‘(abs ∘ − ))1) ⇒ ⊢ (ℂ D (log ↾ 𝑆)) = (𝑥 ∈ 𝑆 ↦ (1 / 𝑥)) | ||
Theorem | advlog 25231 | The antiderivative of the logarithm. (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥)) | ||
Theorem | advlogexp 25232* | 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 25233 | Lemma for efopn 25235. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by Mario Carneiro, 8-Sep-2015.) |
⊢ (((𝑅 ∈ ℝ+ ∧ 𝑅 < π) ∧ 𝐴 ∈ (0(ball‘(abs ∘ − ))𝑅)) → (abs‘(ℑ‘𝐴)) < π) | ||
Theorem | efopnlem2 25234 | Lemma for efopn 25235. (Contributed by Mario Carneiro, 2-May-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ ((𝑅 ∈ ℝ+ ∧ 𝑅 < π) → (exp “ (0(ball‘(abs ∘ − ))𝑅)) ∈ 𝐽) | ||
Theorem | efopn 25235 | The exponential map is an open map. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑆 ∈ 𝐽 → (exp “ 𝑆) ∈ 𝐽) | ||
Theorem | logtayllem 25236* | Lemma for logtayl 25237. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))) ∈ dom ⇝ ) | ||
Theorem | logtayl 25237* | The Taylor series for -log(1 − 𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴↑𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴))) | ||
Theorem | logtaylsum 25238* | The Taylor series for -log(1 − 𝐴), as an infinite sum. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → Σ𝑘 ∈ ℕ ((𝐴↑𝑘) / 𝑘) = -(log‘(1 − 𝐴))) | ||
Theorem | logtayl2 25239* | Power series expression for the logarithm. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ 𝑆 = (1(ball‘(abs ∘ − ))1) ⇒ ⊢ (𝐴 ∈ 𝑆 → seq1( + , (𝑘 ∈ ℕ ↦ (((-1↑(𝑘 − 1)) / 𝑘) · ((𝐴 − 1)↑𝑘)))) ⇝ (log‘𝐴)) | ||
Theorem | logccv 25240 | 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 25241 | Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) = if(𝐴 = 0, if(𝐵 = 0, 1, 0), (exp‘(𝐵 · (log‘𝐴))))) | ||
Theorem | cxpef 25242 | Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴)))) | ||
Theorem | 0cxp 25243 | Value of the complex power function when the first argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (0↑𝑐𝐴) = 0) | ||
Theorem | cxpexpz 25244 | Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℤ) → (𝐴↑𝑐𝐵) = (𝐴↑𝐵)) | ||
Theorem | cxpexp 25245 | Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝑐𝐵) = (𝐴↑𝐵)) | ||
Theorem | logcxp 25246 | Logarithm of a complex power. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴))) | ||
Theorem | cxp0 25247 | Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴↑𝑐0) = 1) | ||
Theorem | cxp1 25248 | Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴↑𝑐1) = 𝐴) | ||
Theorem | 1cxp 25249 | Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (𝐴 ∈ ℂ → (1↑𝑐𝐴) = 1) | ||
Theorem | ecxp 25250 | Write the exponential function as an exponent to the power e. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (𝐴 ∈ ℂ → (e↑𝑐𝐴) = (exp‘𝐴)) | ||
Theorem | cxpcl 25251 | Closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) ∈ ℂ) | ||
Theorem | recxpcl 25252 | Real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ) → (𝐴↑𝑐𝐵) ∈ ℝ) | ||
Theorem | rpcxpcl 25253 | Positive real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (𝐴↑𝑐𝐵) ∈ ℝ+) | ||
Theorem | cxpne0 25254 | Complex exponentiation is nonzero if its mantissa is nonzero. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) ≠ 0) | ||
Theorem | cxpeq0 25255 | Complex exponentiation is zero iff the mantissa is zero and the exponent is nonzero. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑐𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 ≠ 0))) | ||
Theorem | cxpadd 25256 | 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 25257 | Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐(𝐵 + 1)) = ((𝐴↑𝑐𝐵) · 𝐴)) | ||
Theorem | cxpneg 25258 | Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐-𝐵) = (1 / (𝐴↑𝑐𝐵))) | ||
Theorem | cxpsub 25259 | Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴↑𝑐(𝐵 − 𝐶)) = ((𝐴↑𝑐𝐵) / (𝐴↑𝑐𝐶))) | ||
Theorem | cxpge0 25260 | Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ) → 0 ≤ (𝐴↑𝑐𝐵)) | ||
Theorem | mulcxplem 25261 | Lemma for mulcxp 25262. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (0↑𝑐𝐶) = ((𝐴↑𝑐𝐶) · (0↑𝑐𝐶))) | ||
Theorem | mulcxp 25262 | 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 25263 | Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → ((1 / 𝐴)↑𝑐𝐵) = (1 / (𝐴↑𝑐𝐵))) | ||
Theorem | divcxp 25264 | Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) / (𝐵↑𝑐𝐶))) | ||
Theorem | cxpmul 25265 | 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 25266 | Product of exponents law for complex exponentiation. Variation on cxpmul 25265 with more general conditions on 𝐴 and 𝐵 when 𝐶 is an integer. (Contributed by Mario Carneiro, 9-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℕ0) → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
Theorem | cxproot 25267 | The complex power function allows us to write n-th roots via the idiom 𝐴↑𝑐(1 / 𝑁). (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑐(1 / 𝑁))↑𝑁) = 𝐴) | ||
Theorem | cxpmul2z 25268 | Generalize cxpmul2 25266 to negative integers. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℤ)) → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
Theorem | abscxp 25269 | Absolute value of a power, when the base is real. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴↑𝑐𝐵)) = (𝐴↑𝑐(ℜ‘𝐵))) | ||
Theorem | abscxp2 25270 | Absolute value of a power, when the exponent is real. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ) → (abs‘(𝐴↑𝑐𝐵)) = ((abs‘𝐴)↑𝑐𝐵)) | ||
Theorem | cxplt 25271 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐵) < (𝐴↑𝑐𝐶))) | ||
Theorem | cxple 25272 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶))) | ||
Theorem | cxplea 25273 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ≤ 𝐶) → (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶)) | ||
Theorem | cxple2 25274 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶))) | ||
Theorem | cxplt2 25275 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐴↑𝑐𝐶) < (𝐵↑𝑐𝐶))) | ||
Theorem | cxple2a 25276 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐶) ∧ 𝐴 ≤ 𝐵) → (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶)) | ||
Theorem | cxplt3 25277 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐴 < 1) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐶) < (𝐴↑𝑐𝐵))) | ||
Theorem | cxple3 25278 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐴 < 1) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐶) ≤ (𝐴↑𝑐𝐵))) | ||
Theorem | cxpsqrtlem 25279 | Lemma for cxpsqrt 25280. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 / 2)) = -(√‘𝐴)) → (i · (√‘𝐴)) ∈ ℝ) | ||
Theorem | cxpsqrt 25280 | 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 25281 | Logarithm of a square root. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ (𝐴 ∈ ℝ+ → (log‘(√‘𝐴)) = ((log‘𝐴) / 2)) | ||
Theorem | cxp0d 25282 | Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐0) = 1) | ||
Theorem | cxp1d 25283 | Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐1) = 𝐴) | ||
Theorem | 1cxpd 25284 | Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (1↑𝑐𝐴) = 1) | ||
Theorem | cxpcld 25285 | Closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℂ) | ||
Theorem | cxpmul2d 25286 | Product of exponents law for complex exponentiation. Variation on cxpmul 25265 with more general conditions on 𝐴 and 𝐵 when 𝐶 is an integer. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
Theorem | 0cxpd 25287 | Value of the complex power function when the first argument is zero. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (0↑𝑐𝐴) = 0) | ||
Theorem | cxpexpzd 25288 | Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) = (𝐴↑𝐵)) | ||
Theorem | cxpefd 25289 | Value of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴)))) | ||
Theorem | cxpne0d 25290 | Complex exponentiation is nonzero if its mantissa is nonzero. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ≠ 0) | ||
Theorem | cxpp1d 25291 | Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 + 1)) = ((𝐴↑𝑐𝐵) · 𝐴)) | ||
Theorem | cxpnegd 25292 | Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐-𝐵) = (1 / (𝐴↑𝑐𝐵))) | ||
Theorem | cxpmul2zd 25293 | Generalize cxpmul2 25266 to negative integers. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
Theorem | cxpaddd 25294 | 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 25295 | Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 − 𝐶)) = ((𝐴↑𝑐𝐵) / (𝐴↑𝑐𝐶))) | ||
Theorem | cxpltd 25296 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 < 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐵) < (𝐴↑𝑐𝐶))) | ||
Theorem | cxpled 25297 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 < 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶))) | ||
Theorem | cxplead 25298 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶)) | ||
Theorem | divcxpd 25299 | Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) / (𝐵↑𝑐𝐶))) | ||
Theorem | recxpcld 25300 | Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℝ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |