![]() |
Metamath
Proof Explorer Theorem List (p. 266 of 482) | < 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: | ![]() (1-30680) |
![]() (30681-32203) |
![]() (32204-48131) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | argimgt0 26501 | Closure of the argument of a complex number with positive imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 0 < (ℑ‘𝐴)) → (ℑ‘(log‘𝐴)) ∈ (0(,)π)) | ||
Theorem | argimlt0 26502 | Closure of the argument of a complex number with negative imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) < 0) → (ℑ‘(log‘𝐴)) ∈ (-π(,)0)) | ||
Theorem | logimul 26503 | Multiplying a number by i increases the logarithm of the number by iπ / 2. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ (ℜ‘𝐴)) → (log‘(i · 𝐴)) = ((log‘𝐴) + (i · (π / 2)))) | ||
Theorem | logneg2 26504 | The logarithm of the negative of a number with positive imaginary part is i · π less than the original. (Compare logneg 26477.) (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 0 < (ℑ‘𝐴)) → (log‘-𝐴) = ((log‘𝐴) − (i · π))) | ||
Theorem | logmul2 26505 | Generalization of relogmul 26481 to a complex left argument. (Contributed by Mario Carneiro, 9-Jul-2017.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+) → (log‘(𝐴 · 𝐵)) = ((log‘𝐴) + (log‘𝐵))) | ||
Theorem | logdiv2 26506 | Generalization of relogdiv 26482 to a complex left argument. (Contributed by Mario Carneiro, 8-Jul-2017.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+) → (log‘(𝐴 / 𝐵)) = ((log‘𝐴) − (log‘𝐵))) | ||
Theorem | abslogle 26507 | Bound on the magnitude of the complex logarithm function. (Contributed by Mario Carneiro, 3-Jul-2017.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘(log‘𝐴)) ≤ ((abs‘(log‘(abs‘𝐴))) + π)) | ||
Theorem | tanarg 26508 | The basic relation between the "arg" function ℑ ∘ log and the arctangent. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (tan‘(ℑ‘(log‘𝐴))) = ((ℑ‘𝐴) / (ℜ‘𝐴))) | ||
Theorem | logdivlti 26509 | The log𝑥 / 𝑥 function is strictly decreasing on the reals greater than e. (Contributed by Mario Carneiro, 14-Mar-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐵) / 𝐵) < ((log‘𝐴) / 𝐴)) | ||
Theorem | logdivlt 26510 | The log𝑥 / 𝑥 function is strictly decreasing on the reals greater than e. (Contributed by Mario Carneiro, 14-Mar-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ e ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ e ≤ 𝐵)) → (𝐴 < 𝐵 ↔ ((log‘𝐵) / 𝐵) < ((log‘𝐴) / 𝐴))) | ||
Theorem | logdivle 26511 | The log𝑥 / 𝑥 function is strictly decreasing on the reals greater than e. (Contributed by Mario Carneiro, 3-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ e ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ e ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ ((log‘𝐵) / 𝐵) ≤ ((log‘𝐴) / 𝐴))) | ||
Theorem | relogcld 26512 | Closure of the natural logarithm function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (log‘𝐴) ∈ ℝ) | ||
Theorem | reeflogd 26513 | Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (exp‘(log‘𝐴)) = 𝐴) | ||
Theorem | relogmuld 26514 | 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 26515 | 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 26516 | Natural logarithm preserves ≤. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (log‘𝐴) ≤ (log‘𝐵))) | ||
Theorem | relogefd 26517 | Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (log‘(exp‘𝐴)) = 𝐴) | ||
Theorem | rplogcld 26518 | Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 < 𝐴) ⇒ ⊢ (𝜑 → (log‘𝐴) ∈ ℝ+) | ||
Theorem | logge0d 26519 | The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 ≤ 𝐴) ⇒ ⊢ (𝜑 → 0 ≤ (log‘𝐴)) | ||
Theorem | logge0b 26520 | 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 26521 | 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 26522 | 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 26523 | 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 26524 | The inverse logarithm function converges to zero. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝𝑟 0 | ||
Theorem | logno1 26525 | 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 26526 | The derivative of the real logarithm function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (ℝ D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) | ||
Theorem | relogcn 26527 | The real logarithm function is continuous. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ (log ↾ ℝ+) ∈ (ℝ+–cn→ℝ) | ||
Theorem | ellogdm 26528 | Elementhood in the "continuous domain" of the complex logarithm. (Contributed by Mario Carneiro, 18-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝐴 ∈ 𝐷 ↔ (𝐴 ∈ ℂ ∧ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ+))) | ||
Theorem | logdmn0 26529 | A number in the continuous domain of log is nonzero. (Contributed by Mario Carneiro, 18-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝐴 ∈ 𝐷 → 𝐴 ≠ 0) | ||
Theorem | logdmnrp 26530 | A number in the continuous domain of log is not a strictly negative number. (Contributed by Mario Carneiro, 18-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝐴 ∈ 𝐷 → ¬ -𝐴 ∈ ℝ+) | ||
Theorem | logdmss 26531 | 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 26532 | Lemma for logcn 26536. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) & ⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) ⇒ ⊢ (𝜑 → if(𝑆 ≤ 𝑇, 𝑆, 𝑇) ∈ ℝ+) | ||
Theorem | logcnlem3 26533 | Lemma for logcn 26536. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) & ⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < if(𝑆 ≤ 𝑇, 𝑆, 𝑇)) ⇒ ⊢ (𝜑 → (-π < ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ∧ ((ℑ‘(log‘𝐵)) − (ℑ‘(log‘𝐴))) ≤ π)) | ||
Theorem | logcnlem4 26534 | Lemma for logcn 26536. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = if(𝐴 ∈ ℝ+, 𝐴, (abs‘(ℑ‘𝐴))) & ⊢ 𝑇 = ((abs‘𝐴) · (𝑅 / (1 + 𝑅))) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < if(𝑆 ≤ 𝑇, 𝑆, 𝑇)) ⇒ ⊢ (𝜑 → (abs‘((ℑ‘(log‘𝐴)) − (ℑ‘(log‘𝐵)))) < 𝑅) | ||
Theorem | logcnlem5 26535* | Lemma for logcn 26536. (Contributed by Mario Carneiro, 18-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝑥 ∈ 𝐷 ↦ (ℑ‘(log‘𝑥))) ∈ (𝐷–cn→ℝ) | ||
Theorem | logcn 26536 | 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 26537 | Lemma for dvlog 26540. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (log “ 𝐷) ∈ (TopOpen‘ℂfld) | ||
Theorem | logdmopn 26538 | The "continuous domain" of log is an open set. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ 𝐷 ∈ (TopOpen‘ℂfld) | ||
Theorem | logf1o2 26539 | 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 26540* | The derivative of the complex logarithm function. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (ℂ D (log ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) | ||
Theorem | dvlog2lem 26541 | Lemma for dvlog2 26542. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ 𝑆 = (1(ball‘(abs ∘ − ))1) ⇒ ⊢ 𝑆 ⊆ (ℂ ∖ (-∞(,]0)) | ||
Theorem | dvlog2 26542* | 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 26540. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ 𝑆 = (1(ball‘(abs ∘ − ))1) ⇒ ⊢ (ℂ D (log ↾ 𝑆)) = (𝑥 ∈ 𝑆 ↦ (1 / 𝑥)) | ||
Theorem | advlog 26543 | The antiderivative of the logarithm. (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥)) | ||
Theorem | advlogexp 26544* | 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 26545 | Lemma for efopn 26547. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by Mario Carneiro, 8-Sep-2015.) |
⊢ (((𝑅 ∈ ℝ+ ∧ 𝑅 < π) ∧ 𝐴 ∈ (0(ball‘(abs ∘ − ))𝑅)) → (abs‘(ℑ‘𝐴)) < π) | ||
Theorem | efopnlem2 26546 | Lemma for efopn 26547. (Contributed by Mario Carneiro, 2-May-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ ((𝑅 ∈ ℝ+ ∧ 𝑅 < π) → (exp “ (0(ball‘(abs ∘ − ))𝑅)) ∈ 𝐽) | ||
Theorem | efopn 26547 | The exponential map is an open map. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑆 ∈ 𝐽 → (exp “ 𝑆) ∈ 𝐽) | ||
Theorem | logtayllem 26548* | Lemma for logtayl 26549. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))) ∈ dom ⇝ ) | ||
Theorem | logtayl 26549* | The Taylor series for -log(1 − 𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴↑𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴))) | ||
Theorem | logtaylsum 26550* | The Taylor series for -log(1 − 𝐴), as an infinite sum. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → Σ𝑘 ∈ ℕ ((𝐴↑𝑘) / 𝑘) = -(log‘(1 − 𝐴))) | ||
Theorem | logtayl2 26551* | Power series expression for the logarithm. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ 𝑆 = (1(ball‘(abs ∘ − ))1) ⇒ ⊢ (𝐴 ∈ 𝑆 → seq1( + , (𝑘 ∈ ℕ ↦ (((-1↑(𝑘 − 1)) / 𝑘) · ((𝐴 − 1)↑𝑘)))) ⇝ (log‘𝐴)) | ||
Theorem | logccv 26552 | 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 26553 | Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) = if(𝐴 = 0, if(𝐵 = 0, 1, 0), (exp‘(𝐵 · (log‘𝐴))))) | ||
Theorem | cxpef 26554 | Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴)))) | ||
Theorem | 0cxp 26555 | Value of the complex power function when the first argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (0↑𝑐𝐴) = 0) | ||
Theorem | cxpexpz 26556 | Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℤ) → (𝐴↑𝑐𝐵) = (𝐴↑𝐵)) | ||
Theorem | cxpexp 26557 | Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝑐𝐵) = (𝐴↑𝐵)) | ||
Theorem | logcxp 26558 | Logarithm of a complex power. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴))) | ||
Theorem | cxp0 26559 | Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴↑𝑐0) = 1) | ||
Theorem | cxp1 26560 | Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴↑𝑐1) = 𝐴) | ||
Theorem | 1cxp 26561 | Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (𝐴 ∈ ℂ → (1↑𝑐𝐴) = 1) | ||
Theorem | ecxp 26562 | Write the exponential function as an exponent to the power e. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (𝐴 ∈ ℂ → (e↑𝑐𝐴) = (exp‘𝐴)) | ||
Theorem | cxpcl 26563 | Closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) ∈ ℂ) | ||
Theorem | recxpcl 26564 | Real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ) → (𝐴↑𝑐𝐵) ∈ ℝ) | ||
Theorem | rpcxpcl 26565 | Positive real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (𝐴↑𝑐𝐵) ∈ ℝ+) | ||
Theorem | cxpne0 26566 | Complex exponentiation is nonzero if its base is nonzero. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) ≠ 0) | ||
Theorem | cxpeq0 26567 | 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 26568 | 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 26569 | Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐(𝐵 + 1)) = ((𝐴↑𝑐𝐵) · 𝐴)) | ||
Theorem | cxpneg 26570 | Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐-𝐵) = (1 / (𝐴↑𝑐𝐵))) | ||
Theorem | cxpsub 26571 | Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴↑𝑐(𝐵 − 𝐶)) = ((𝐴↑𝑐𝐵) / (𝐴↑𝑐𝐶))) | ||
Theorem | cxpge0 26572 | Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ) → 0 ≤ (𝐴↑𝑐𝐵)) | ||
Theorem | mulcxplem 26573 | Lemma for mulcxp 26574. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (0↑𝑐𝐶) = ((𝐴↑𝑐𝐶) · (0↑𝑐𝐶))) | ||
Theorem | mulcxp 26574 | 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 26575 | Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → ((1 / 𝐴)↑𝑐𝐵) = (1 / (𝐴↑𝑐𝐵))) | ||
Theorem | divcxp 26576 | Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) / (𝐵↑𝑐𝐶))) | ||
Theorem | cxpmul 26577 | 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 26578 | Product of exponents law for complex exponentiation. Variation on cxpmul 26577 with more general conditions on 𝐴 and 𝐵 when 𝐶 is an integer. (Contributed by Mario Carneiro, 9-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℕ0) → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
Theorem | cxproot 26579 | The complex power function allows to write n-th roots via the idiom 𝐴↑𝑐(1 / 𝑁). (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑐(1 / 𝑁))↑𝑁) = 𝐴) | ||
Theorem | cxpmul2z 26580 | Generalize cxpmul2 26578 to negative integers. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℤ)) → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
Theorem | abscxp 26581 | Absolute value of a power, when the base is real. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴↑𝑐𝐵)) = (𝐴↑𝑐(ℜ‘𝐵))) | ||
Theorem | abscxp2 26582 | Absolute value of a power, when the exponent is real. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ) → (abs‘(𝐴↑𝑐𝐵)) = ((abs‘𝐴)↑𝑐𝐵)) | ||
Theorem | cxplt 26583 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐵) < (𝐴↑𝑐𝐶))) | ||
Theorem | cxple 26584 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶))) | ||
Theorem | cxplea 26585 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ≤ 𝐶) → (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶)) | ||
Theorem | cxple2 26586 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶))) | ||
Theorem | cxplt2 26587 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐴↑𝑐𝐶) < (𝐵↑𝑐𝐶))) | ||
Theorem | cxple2a 26588 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐶) ∧ 𝐴 ≤ 𝐵) → (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶)) | ||
Theorem | cxplt3 26589 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐴 < 1) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐶) < (𝐴↑𝑐𝐵))) | ||
Theorem | cxple3 26590 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐴 < 1) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐶) ≤ (𝐴↑𝑐𝐵))) | ||
Theorem | cxpsqrtlem 26591 | Lemma for cxpsqrt 26592. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 / 2)) = -(√‘𝐴)) → (i · (√‘𝐴)) ∈ ℝ) | ||
Theorem | cxpsqrt 26592 | 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 26593 | Logarithm of a square root. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ (𝐴 ∈ ℝ+ → (log‘(√‘𝐴)) = ((log‘𝐴) / 2)) | ||
Theorem | cxp0d 26594 | Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐0) = 1) | ||
Theorem | cxp1d 26595 | Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐1) = 𝐴) | ||
Theorem | 1cxpd 26596 | Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (1↑𝑐𝐴) = 1) | ||
Theorem | cxpcld 26597 | Closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℂ) | ||
Theorem | cxpmul2d 26598 | Product of exponents law for complex exponentiation. Variation on cxpmul 26577 with more general conditions on 𝐴 and 𝐵 when 𝐶 is an integer. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
Theorem | 0cxpd 26599 | Value of the complex power function when the first argument is zero. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (0↑𝑐𝐴) = 0) | ||
Theorem | cxpexpzd 26600 | Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) = (𝐴↑𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |