| Metamath
Proof Explorer Theorem List (p. 268 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | logtayllem 26701* | Lemma for logtayl 26702. (Contributed by Mario Carneiro, 1-Apr-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))) ∈ dom ⇝ ) | ||
| Theorem | logtayl 26702* | The Taylor series for -log(1 − 𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴↑𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴))) | ||
| Theorem | logtaylsum 26703* | The Taylor series for -log(1 − 𝐴), as an infinite sum. (Contributed by Mario Carneiro, 31-Mar-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → Σ𝑘 ∈ ℕ ((𝐴↑𝑘) / 𝑘) = -(log‘(1 − 𝐴))) | ||
| Theorem | logtayl2 26704* | Power series expression for the logarithm. (Contributed by Mario Carneiro, 31-Mar-2015.) |
| ⊢ 𝑆 = (1(ball‘(abs ∘ − ))1) ⇒ ⊢ (𝐴 ∈ 𝑆 → seq1( + , (𝑘 ∈ ℕ ↦ (((-1↑(𝑘 − 1)) / 𝑘) · ((𝐴 − 1)↑𝑘)))) ⇝ (log‘𝐴)) | ||
| Theorem | logccv 26705 | 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 26706 | Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) = if(𝐴 = 0, if(𝐵 = 0, 1, 0), (exp‘(𝐵 · (log‘𝐴))))) | ||
| Theorem | cxpef 26707 | Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴)))) | ||
| Theorem | 0cxp 26708 | Value of the complex power function when the first argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (0↑𝑐𝐴) = 0) | ||
| Theorem | cxpexpz 26709 | Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℤ) → (𝐴↑𝑐𝐵) = (𝐴↑𝐵)) | ||
| Theorem | cxpexp 26710 | Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝑐𝐵) = (𝐴↑𝐵)) | ||
| Theorem | logcxp 26711 | Logarithm of a complex power. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴))) | ||
| Theorem | cxp0 26712 | Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴↑𝑐0) = 1) | ||
| Theorem | cxp1 26713 | Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴↑𝑐1) = 𝐴) | ||
| Theorem | 1cxp 26714 | Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ (𝐴 ∈ ℂ → (1↑𝑐𝐴) = 1) | ||
| Theorem | ecxp 26715 | Write the exponential function as an exponent to the power e. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ (𝐴 ∈ ℂ → (e↑𝑐𝐴) = (exp‘𝐴)) | ||
| Theorem | cxpcl 26716 | Closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) ∈ ℂ) | ||
| Theorem | recxpcl 26717 | Real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ) → (𝐴↑𝑐𝐵) ∈ ℝ) | ||
| Theorem | rpcxpcl 26718 | Positive real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (𝐴↑𝑐𝐵) ∈ ℝ+) | ||
| Theorem | cxpne0 26719 | Complex exponentiation is nonzero if its base is nonzero. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) ≠ 0) | ||
| Theorem | cxpeq0 26720 | 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 26721 | 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 26722 | Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐(𝐵 + 1)) = ((𝐴↑𝑐𝐵) · 𝐴)) | ||
| Theorem | cxpneg 26723 | Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐-𝐵) = (1 / (𝐴↑𝑐𝐵))) | ||
| Theorem | cxpsub 26724 | Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 22-Sep-2014.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴↑𝑐(𝐵 − 𝐶)) = ((𝐴↑𝑐𝐵) / (𝐴↑𝑐𝐶))) | ||
| Theorem | cxpge0 26725 | Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ) → 0 ≤ (𝐴↑𝑐𝐵)) | ||
| Theorem | mulcxplem 26726 | Lemma for mulcxp 26727. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (0↑𝑐𝐶) = ((𝐴↑𝑐𝐶) · (0↑𝑐𝐶))) | ||
| Theorem | mulcxp 26727 | 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 26728 | Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → ((1 / 𝐴)↑𝑐𝐵) = (1 / (𝐴↑𝑐𝐵))) | ||
| Theorem | divcxp 26729 | Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) / (𝐵↑𝑐𝐶))) | ||
| Theorem | cxpmul 26730 | 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 26731 | Product of exponents law for complex exponentiation. Variation on cxpmul 26730 with more general conditions on 𝐴 and 𝐵 when 𝐶 is a nonnegative integer. (Contributed by Mario Carneiro, 9-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℕ0) → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
| Theorem | cxproot 26732 | The complex power function allows to write n-th roots via the idiom 𝐴↑𝑐(1 / 𝑁). (Contributed by Mario Carneiro, 6-May-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑐(1 / 𝑁))↑𝑁) = 𝐴) | ||
| Theorem | cxpmul2z 26733 | Generalize cxpmul2 26731 to negative integers. (Contributed by Mario Carneiro, 23-Apr-2015.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℤ)) → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
| Theorem | abscxp 26734 | Absolute value of a power, when the base is real. (Contributed by Mario Carneiro, 15-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴↑𝑐𝐵)) = (𝐴↑𝑐(ℜ‘𝐵))) | ||
| Theorem | abscxp2 26735 | Absolute value of a power, when the exponent is real. (Contributed by Mario Carneiro, 15-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ) → (abs‘(𝐴↑𝑐𝐵)) = ((abs‘𝐴)↑𝑐𝐵)) | ||
| Theorem | cxplt 26736 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐵) < (𝐴↑𝑐𝐶))) | ||
| Theorem | cxple 26737 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶))) | ||
| Theorem | cxplea 26738 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 10-Sep-2014.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ≤ 𝐶) → (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶)) | ||
| Theorem | cxple2 26739 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶))) | ||
| Theorem | cxplt2 26740 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 15-Sep-2014.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐴↑𝑐𝐶) < (𝐵↑𝑐𝐶))) | ||
| Theorem | cxple2a 26741 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 15-Sep-2014.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐶) ∧ 𝐴 ≤ 𝐵) → (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶)) | ||
| Theorem | cxplt3 26742 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016.) |
| ⊢ (((𝐴 ∈ ℝ+ ∧ 𝐴 < 1) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐶) < (𝐴↑𝑐𝐵))) | ||
| Theorem | cxple3 26743 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016.) |
| ⊢ (((𝐴 ∈ ℝ+ ∧ 𝐴 < 1) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐶) ≤ (𝐴↑𝑐𝐵))) | ||
| Theorem | cxpsqrtlem 26744 | Lemma for cxpsqrt 26745. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 / 2)) = -(√‘𝐴)) → (i · (√‘𝐴)) ∈ ℝ) | ||
| Theorem | cxpsqrt 26745 | 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 26746 | Logarithm of a square root. (Contributed by Mario Carneiro, 5-May-2016.) |
| ⊢ (𝐴 ∈ ℝ+ → (log‘(√‘𝐴)) = ((log‘𝐴) / 2)) | ||
| Theorem | cxp0d 26747 | Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐0) = 1) | ||
| Theorem | cxp1d 26748 | Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐1) = 𝐴) | ||
| Theorem | 1cxpd 26749 | Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (1↑𝑐𝐴) = 1) | ||
| Theorem | cxpcld 26750 | Closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℂ) | ||
| Theorem | cxpmul2d 26751 | Product of exponents law for complex exponentiation. Variation on cxpmul 26730 with more general conditions on 𝐴 and 𝐵 when 𝐶 is a nonnegative integer. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
| Theorem | 0cxpd 26752 | Value of the complex power function when the first argument is zero. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (0↑𝑐𝐴) = 0) | ||
| Theorem | cxpexpzd 26753 | Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) = (𝐴↑𝐵)) | ||
| Theorem | cxpefd 26754 | Value of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴)))) | ||
| Theorem | cxpne0d 26755 | Complex exponentiation is nonzero if its base is nonzero. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ≠ 0) | ||
| Theorem | cxpp1d 26756 | Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 + 1)) = ((𝐴↑𝑐𝐵) · 𝐴)) | ||
| Theorem | cxpnegd 26757 | Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐-𝐵) = (1 / (𝐴↑𝑐𝐵))) | ||
| Theorem | cxpmul2zd 26758 | Generalize cxpmul2 26731 to negative integers. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
| Theorem | cxpaddd 26759 | 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 26760 | Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 − 𝐶)) = ((𝐴↑𝑐𝐵) / (𝐴↑𝑐𝐶))) | ||
| Theorem | cxpltd 26761 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 < 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐵) < (𝐴↑𝑐𝐶))) | ||
| Theorem | cxpled 26762 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 < 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶))) | ||
| Theorem | cxplead 26763 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶)) | ||
| Theorem | divcxpd 26764 | Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) / (𝐵↑𝑐𝐶))) | ||
| Theorem | recxpcld 26765 | Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℝ) | ||
| Theorem | cxpge0d 26766 | Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴↑𝑐𝐵)) | ||
| Theorem | cxple2ad 26767 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶)) | ||
| Theorem | cxplt2d 26768 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴↑𝑐𝐶) < (𝐵↑𝑐𝐶))) | ||
| Theorem | cxple2d 26769 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶))) | ||
| Theorem | mulcxpd 26770 | 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 26771 | Complex exponentiation on positive real numbers is a one-to-one function. (Contributed by Thierry Arnoux, 1-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴↑𝑐𝐶) = (𝐵↑𝑐𝐶))) | ||
| Theorem | cxpsqrtth 26772 | Square root theorem over the complex numbers for the complex power function. Theorem I.35 of [Apostol] p. 29. Compare with sqrtth 15403. (Contributed by AV, 23-Dec-2022.) |
| ⊢ (𝐴 ∈ ℂ → ((√‘𝐴)↑𝑐2) = 𝐴) | ||
| Theorem | 2irrexpq 26773* | 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 16285), 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 26843. (Contributed by AV, 23-Dec-2022.) |
| ⊢ ∃𝑎 ∈ (ℝ ∖ ℚ)∃𝑏 ∈ (ℝ ∖ ℚ)(𝑎↑𝑐𝑏) ∈ ℚ | ||
| Theorem | cxprecd 26774 | Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((1 / 𝐴)↑𝑐𝐵) = (1 / (𝐴↑𝑐𝐵))) | ||
| Theorem | rpcxpcld 26775 | Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℝ+) | ||
| Theorem | logcxpd 26776 | Logarithm of a complex power. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴))) | ||
| Theorem | cxplt3d 26777 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐶) < (𝐴↑𝑐𝐵))) | ||
| Theorem | cxple3d 26778 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐶) ≤ (𝐴↑𝑐𝐵))) | ||
| Theorem | cxpmuld 26779 | Product of exponents law for complex exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝑐𝐶)) | ||
| Theorem | cxpgt0d 26780 | A positive real raised to a real power is positive. (Contributed by SN, 6-Apr-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℝ) ⇒ ⊢ (𝜑 → 0 < (𝐴↑𝑐𝑁)) | ||
| Theorem | cxpcom 26781 | Commutative law for real exponentiation. (Contributed by AV, 29-Dec-2022.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴↑𝑐𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶)↑𝑐𝐵)) | ||
| Theorem | dvcxp1 26782* | The derivative of a complex power with respect to the first argument. (Contributed by Mario Carneiro, 24-Feb-2015.) |
| ⊢ (𝐴 ∈ ℂ → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥↑𝑐𝐴))) = (𝑥 ∈ ℝ+ ↦ (𝐴 · (𝑥↑𝑐(𝐴 − 1))))) | ||
| Theorem | dvcxp2 26783* | The derivative of a complex power with respect to the second argument. (Contributed by Mario Carneiro, 24-Feb-2015.) |
| ⊢ (𝐴 ∈ ℝ+ → (ℂ D (𝑥 ∈ ℂ ↦ (𝐴↑𝑐𝑥))) = (𝑥 ∈ ℂ ↦ ((log‘𝐴) · (𝐴↑𝑐𝑥)))) | ||
| Theorem | dvsqrt 26784 | The derivative of the real square root function. (Contributed by Mario Carneiro, 1-May-2016.) |
| ⊢ (ℝ D (𝑥 ∈ ℝ+ ↦ (√‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (1 / (2 · (√‘𝑥)))) | ||
| Theorem | dvcncxp1 26785* | Derivative of complex power with respect to first argument on the complex plane. (Contributed by Brendan Leahy, 18-Dec-2018.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (𝐴 ∈ ℂ → (ℂ D (𝑥 ∈ 𝐷 ↦ (𝑥↑𝑐𝐴))) = (𝑥 ∈ 𝐷 ↦ (𝐴 · (𝑥↑𝑐(𝐴 − 1))))) | ||
| Theorem | dvcnsqrt 26786* | Derivative of square root function. (Contributed by Brendan Leahy, 18-Dec-2018.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (ℂ D (𝑥 ∈ 𝐷 ↦ (√‘𝑥))) = (𝑥 ∈ 𝐷 ↦ (1 / (2 · (√‘𝑥)))) | ||
| Theorem | cxpcn 26787* | Domain of continuity of the complex power function. (Contributed by Mario Carneiro, 1-May-2016.) Avoid ax-mulf 11235. (Revised by GG, 16-Mar-2025.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝐷) ⇒ ⊢ (𝑥 ∈ 𝐷, 𝑦 ∈ ℂ ↦ (𝑥↑𝑐𝑦)) ∈ ((𝐾 ×t 𝐽) Cn 𝐽) | ||
| Theorem | cxpcnOLD 26788* | Obsolete version of cxpcn 26787 as of 17-Apr-2025. (Contributed by Mario Carneiro, 1-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝐷) ⇒ ⊢ (𝑥 ∈ 𝐷, 𝑦 ∈ ℂ ↦ (𝑥↑𝑐𝑦)) ∈ ((𝐾 ×t 𝐽) Cn 𝐽) | ||
| Theorem | cxpcn2 26789* | Continuity of the complex power function, when the base is real. (Contributed by Mario Carneiro, 1-May-2016.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t ℝ+) ⇒ ⊢ (𝑥 ∈ ℝ+, 𝑦 ∈ ℂ ↦ (𝑥↑𝑐𝑦)) ∈ ((𝐾 ×t 𝐽) Cn 𝐽) | ||
| Theorem | cxpcn3lem 26790* | Lemma for cxpcn3 26791. (Contributed by Mario Carneiro, 2-May-2016.) |
| ⊢ 𝐷 = (◡ℜ “ ℝ+) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t (0[,)+∞)) & ⊢ 𝐿 = (𝐽 ↾t 𝐷) & ⊢ 𝑈 = (if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) / 2) & ⊢ 𝑇 = if(𝑈 ≤ (𝐸↑𝑐(1 / 𝑈)), 𝑈, (𝐸↑𝑐(1 / 𝑈))) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) → ∃𝑑 ∈ ℝ+ ∀𝑎 ∈ (0[,)+∞)∀𝑏 ∈ 𝐷 (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝐴 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸)) | ||
| Theorem | cxpcn3 26791* | Extend continuity of the complex power function to a base of zero, as long as the exponent has strictly positive real part. (Contributed by Mario Carneiro, 2-May-2016.) |
| ⊢ 𝐷 = (◡ℜ “ ℝ+) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t (0[,)+∞)) & ⊢ 𝐿 = (𝐽 ↾t 𝐷) ⇒ ⊢ (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ ((𝐾 ×t 𝐿) Cn 𝐽) | ||
| Theorem | resqrtcn 26792 | Continuity of the real square root function. (Contributed by Mario Carneiro, 2-May-2016.) |
| ⊢ (√ ↾ (0[,)+∞)) ∈ ((0[,)+∞)–cn→ℝ) | ||
| Theorem | sqrtcn 26793 | Continuity of the square root function. (Contributed by Mario Carneiro, 2-May-2016.) |
| ⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (√ ↾ 𝐷) ∈ (𝐷–cn→ℂ) | ||
| Theorem | cxpaddlelem 26794 | Lemma for cxpaddle 26795. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 1) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ≤ 1) ⇒ ⊢ (𝜑 → 𝐴 ≤ (𝐴↑𝑐𝐵)) | ||
| Theorem | cxpaddle 26795 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ≤ 1) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵)↑𝑐𝐶) ≤ ((𝐴↑𝑐𝐶) + (𝐵↑𝑐𝐶))) | ||
| Theorem | abscxpbnd 26796 | Bound on the absolute value of a complex power. (Contributed by Mario Carneiro, 15-Sep-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 0 ≤ (ℜ‘𝐵)) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐴) ≤ 𝑀) ⇒ ⊢ (𝜑 → (abs‘(𝐴↑𝑐𝐵)) ≤ ((𝑀↑𝑐(ℜ‘𝐵)) · (exp‘((abs‘𝐵) · π)))) | ||
| Theorem | root1id 26797 | Property of an 𝑁-th root of unity. (Contributed by Mario Carneiro, 23-Apr-2015.) |
| ⊢ (𝑁 ∈ ℕ → ((-1↑𝑐(2 / 𝑁))↑𝑁) = 1) | ||
| Theorem | root1eq1 26798 | The only powers of an 𝑁-th root of unity that equal 1 are the multiples of 𝑁. In other words, -1↑𝑐(2 / 𝑁) has order 𝑁 in the multiplicative group of nonzero complex numbers. (In fact, these and their powers are the only elements of finite order in the complex numbers.) (Contributed by Mario Carneiro, 28-Apr-2016.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) → (((-1↑𝑐(2 / 𝑁))↑𝐾) = 1 ↔ 𝑁 ∥ 𝐾)) | ||
| Theorem | root1cj 26799 | Within the 𝑁-th roots of unity, the conjugate of the 𝐾-th root is the 𝑁 − 𝐾-th root. (Contributed by Mario Carneiro, 23-Apr-2015.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) → (∗‘((-1↑𝑐(2 / 𝑁))↑𝐾)) = ((-1↑𝑐(2 / 𝑁))↑(𝑁 − 𝐾))) | ||
| Theorem | cxpeq 26800* | Solve an equation involving an 𝑁-th power. The expression -1↑𝑐(2 / 𝑁) = exp(2πi / 𝑁) is a way to write the primitive 𝑁-th root of unity with the smallest positive argument. (Contributed by Mario Carneiro, 23-Apr-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) = 𝐵 ↔ ∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) · ((-1↑𝑐(2 / 𝑁))↑𝑛)))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |