Home | Metamath
Proof Explorer Theorem List (p. 243 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | advlogexp 24201* | 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 24202 | Lemma for efopn 24204. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by Mario Carneiro, 8-Sep-2015.) |
⊢ (((𝑅 ∈ ℝ+ ∧ 𝑅 < π) ∧ 𝐴 ∈ (0(ball‘(abs ∘ − ))𝑅)) → (abs‘(ℑ‘𝐴)) < π) | ||
Theorem | efopnlem2 24203 | Lemma for efopn 24204. (Contributed by Mario Carneiro, 2-May-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ ((𝑅 ∈ ℝ+ ∧ 𝑅 < π) → (exp “ (0(ball‘(abs ∘ − ))𝑅)) ∈ 𝐽) | ||
Theorem | efopn 24204 | The exponential map is an open map. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑆 ∈ 𝐽 → (exp “ 𝑆) ∈ 𝐽) | ||
Theorem | logtayllem 24205* | Lemma for logtayl 24206. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))) ∈ dom ⇝ ) | ||
Theorem | logtayl 24206* | The Taylor series for -log(1 − 𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴↑𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴))) | ||
Theorem | logtaylsum 24207* | The Taylor series for -log(1 − 𝐴), as an infinite sum. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → Σ𝑘 ∈ ℕ ((𝐴↑𝑘) / 𝑘) = -(log‘(1 − 𝐴))) | ||
Theorem | logtayl2 24208* | Power series expression for the logarithm. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ 𝑆 = (1(ball‘(abs ∘ − ))1) ⇒ ⊢ (𝐴 ∈ 𝑆 → seq1( + , (𝑘 ∈ ℕ ↦ (((-1↑(𝑘 − 1)) / 𝑘) · ((𝐴 − 1)↑𝑘)))) ⇝ (log‘𝐴)) | ||
Theorem | logccv 24209 | 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 24210 | Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) = if(𝐴 = 0, if(𝐵 = 0, 1, 0), (exp‘(𝐵 · (log‘𝐴))))) | ||
Theorem | cxpef 24211 | Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴)))) | ||
Theorem | 0cxp 24212 | Value of the complex power function when the first argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (0↑𝑐𝐴) = 0) | ||
Theorem | cxpexpz 24213 | Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℤ) → (𝐴↑𝑐𝐵) = (𝐴↑𝐵)) | ||
Theorem | cxpexp 24214 | Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝑐𝐵) = (𝐴↑𝐵)) | ||
Theorem | logcxp 24215 | Logarithm of a complex power. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴))) | ||
Theorem | cxp0 24216 | Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴↑𝑐0) = 1) | ||
Theorem | cxp1 24217 | Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴↑𝑐1) = 𝐴) | ||
Theorem | 1cxp 24218 | Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (𝐴 ∈ ℂ → (1↑𝑐𝐴) = 1) | ||
Theorem | ecxp 24219 | Write the exponential function as an exponent to the power e. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (𝐴 ∈ ℂ → (e↑𝑐𝐴) = (exp‘𝐴)) | ||
Theorem | cxpcl 24220 | Closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) ∈ ℂ) | ||
Theorem | recxpcl 24221 | Real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ) → (𝐴↑𝑐𝐵) ∈ ℝ) | ||
Theorem | rpcxpcl 24222 | Positive real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (𝐴↑𝑐𝐵) ∈ ℝ+) | ||
Theorem | cxpne0 24223 | Complex exponentiation is nonzero if its mantissa is nonzero. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) ≠ 0) | ||
Theorem | cxpeq0 24224 | 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 24225 | 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 24226 | Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐(𝐵 + 1)) = ((𝐴↑𝑐𝐵) · 𝐴)) | ||
Theorem | cxpneg 24227 | Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐-𝐵) = (1 / (𝐴↑𝑐𝐵))) | ||
Theorem | cxpsub 24228 | Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴↑𝑐(𝐵 − 𝐶)) = ((𝐴↑𝑐𝐵) / (𝐴↑𝑐𝐶))) | ||
Theorem | cxpge0 24229 | Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ) → 0 ≤ (𝐴↑𝑐𝐵)) | ||
Theorem | mulcxplem 24230 | Lemma for mulcxp 24231. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (0↑𝑐𝐶) = ((𝐴↑𝑐𝐶) · (0↑𝑐𝐶))) | ||
Theorem | mulcxp 24231 | 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 24232 | Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → ((1 / 𝐴)↑𝑐𝐵) = (1 / (𝐴↑𝑐𝐵))) | ||
Theorem | divcxp 24233 | Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) / (𝐵↑𝑐𝐶))) | ||
Theorem | cxpmul 24234 | 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 24235 | Product of exponents law for complex exponentiation. Variation on cxpmul 24234 with more general conditions on 𝐴 and 𝐵 when 𝐶 is an integer. (Contributed by Mario Carneiro, 9-Aug-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℕ0) → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
Theorem | cxproot 24236 | 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 24237 | Generalize cxpmul2 24235 to negative integers. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℤ)) → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
Theorem | abscxp 24238 | Absolute value of a power, when the base is real. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴↑𝑐𝐵)) = (𝐴↑𝑐(ℜ‘𝐵))) | ||
Theorem | abscxp2 24239 | Absolute value of a power, when the exponent is real. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ) → (abs‘(𝐴↑𝑐𝐵)) = ((abs‘𝐴)↑𝑐𝐵)) | ||
Theorem | cxplt 24240 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐵) < (𝐴↑𝑐𝐶))) | ||
Theorem | cxple 24241 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶))) | ||
Theorem | cxplea 24242 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ≤ 𝐶) → (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶)) | ||
Theorem | cxple2 24243 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶))) | ||
Theorem | cxplt2 24244 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐴↑𝑐𝐶) < (𝐵↑𝑐𝐶))) | ||
Theorem | cxple2a 24245 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐶) ∧ 𝐴 ≤ 𝐵) → (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶)) | ||
Theorem | cxplt3 24246 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐴 < 1) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐶) < (𝐴↑𝑐𝐵))) | ||
Theorem | cxple3 24247 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐴 < 1) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐶) ≤ (𝐴↑𝑐𝐵))) | ||
Theorem | cxpsqrtlem 24248 | Lemma for cxpsqrt 24249. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 / 2)) = -(√‘𝐴)) → (i · (√‘𝐴)) ∈ ℝ) | ||
Theorem | cxpsqrt 24249 | 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 24250 | Logarithm of a square root. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ (𝐴 ∈ ℝ+ → (log‘(√‘𝐴)) = ((log‘𝐴) / 2)) | ||
Theorem | cxp0d 24251 | Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐0) = 1) | ||
Theorem | cxp1d 24252 | Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐1) = 𝐴) | ||
Theorem | 1cxpd 24253 | Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (1↑𝑐𝐴) = 1) | ||
Theorem | cxpcld 24254 | Closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℂ) | ||
Theorem | cxpmul2d 24255 | Product of exponents law for complex exponentiation. Variation on cxpmul 24234 with more general conditions on 𝐴 and 𝐵 when 𝐶 is an integer. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
Theorem | 0cxpd 24256 | Value of the complex power function when the first argument is zero. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (0↑𝑐𝐴) = 0) | ||
Theorem | cxpexpzd 24257 | Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) = (𝐴↑𝐵)) | ||
Theorem | cxpefd 24258 | Value of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴)))) | ||
Theorem | cxpne0d 24259 | Complex exponentiation is nonzero if its mantissa is nonzero. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ≠ 0) | ||
Theorem | cxpp1d 24260 | Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 + 1)) = ((𝐴↑𝑐𝐵) · 𝐴)) | ||
Theorem | cxpnegd 24261 | Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐-𝐵) = (1 / (𝐴↑𝑐𝐵))) | ||
Theorem | cxpmul2zd 24262 | Generalize cxpmul2 24235 to negative integers. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
Theorem | cxpaddd 24263 | 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 24264 | Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 − 𝐶)) = ((𝐴↑𝑐𝐵) / (𝐴↑𝑐𝐶))) | ||
Theorem | cxpltd 24265 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 < 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐵) < (𝐴↑𝑐𝐶))) | ||
Theorem | cxpled 24266 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 < 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶))) | ||
Theorem | cxplead 24267 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶)) | ||
Theorem | divcxpd 24268 | Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) / (𝐵↑𝑐𝐶))) | ||
Theorem | recxpcld 24269 | Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℝ) | ||
Theorem | cxpge0d 24270 | Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴↑𝑐𝐵)) | ||
Theorem | cxple2ad 24271 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶)) | ||
Theorem | cxplt2d 24272 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴↑𝑐𝐶) < (𝐵↑𝑐𝐶))) | ||
Theorem | cxple2d 24273 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶))) | ||
Theorem | mulcxpd 24274 | Complex exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) · (𝐵↑𝑐𝐶))) | ||
Theorem | cxprecd 24275 | Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((1 / 𝐴)↑𝑐𝐵) = (1 / (𝐴↑𝑐𝐵))) | ||
Theorem | rpcxpcld 24276 | Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℝ+) | ||
Theorem | logcxpd 24277 | Logarithm of a complex power. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴))) | ||
Theorem | cxplt3d 24278 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐶) < (𝐴↑𝑐𝐵))) | ||
Theorem | cxple3d 24279 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐶) ≤ (𝐴↑𝑐𝐵))) | ||
Theorem | cxpmuld 24280 | Product of exponents law for complex exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝑐𝐶)) | ||
Theorem | dvcxp1 24281* | The derivative of a complex power with respect to the first argument. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝐴 ∈ ℂ → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥↑𝑐𝐴))) = (𝑥 ∈ ℝ+ ↦ (𝐴 · (𝑥↑𝑐(𝐴 − 1))))) | ||
Theorem | dvcxp2 24282* | The derivative of a complex power with respect to the second argument. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝐴 ∈ ℝ+ → (ℂ D (𝑥 ∈ ℂ ↦ (𝐴↑𝑐𝑥))) = (𝑥 ∈ ℂ ↦ ((log‘𝐴) · (𝐴↑𝑐𝑥)))) | ||
Theorem | dvsqrt 24283 | The derivative of the real square root function. (Contributed by Mario Carneiro, 1-May-2016.) |
⊢ (ℝ D (𝑥 ∈ ℝ+ ↦ (√‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (1 / (2 · (√‘𝑥)))) | ||
Theorem | dvcncxp1 24284* | 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 24285* | Derivative of square root function. (Contributed by Brendan Leahy, 18-Dec-2018.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (ℂ D (𝑥 ∈ 𝐷 ↦ (√‘𝑥))) = (𝑥 ∈ 𝐷 ↦ (1 / (2 · (√‘𝑥)))) | ||
Theorem | cxpcn 24286* | Domain of continuity of the complex power function. (Contributed by Mario Carneiro, 1-May-2016.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝐷) ⇒ ⊢ (𝑥 ∈ 𝐷, 𝑦 ∈ ℂ ↦ (𝑥↑𝑐𝑦)) ∈ ((𝐾 ×t 𝐽) Cn 𝐽) | ||
Theorem | cxpcn2 24287* | 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 24288* | Lemma for cxpcn3 24289. (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 24289* | 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 24290 | Continuity of the real square root function. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ (√ ↾ (0[,)+∞)) ∈ ((0[,)+∞)–cn→ℝ) | ||
Theorem | sqrtcn 24291 | Continuity of the square root function. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (√ ↾ 𝐷) ∈ (𝐷–cn→ℂ) | ||
Theorem | cxpaddlelem 24292 | Lemma for cxpaddle 24293. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 1) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ≤ 1) ⇒ ⊢ (𝜑 → 𝐴 ≤ (𝐴↑𝑐𝐵)) | ||
Theorem | cxpaddle 24293 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ≤ 1) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵)↑𝑐𝐶) ≤ ((𝐴↑𝑐𝐶) + (𝐵↑𝑐𝐶))) | ||
Theorem | abscxpbnd 24294 | Bound on the absolute value of a complex power. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 0 ≤ (ℜ‘𝐵)) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐴) ≤ 𝑀) ⇒ ⊢ (𝜑 → (abs‘(𝐴↑𝑐𝐵)) ≤ ((𝑀↑𝑐(ℜ‘𝐵)) · (exp‘((abs‘𝐵) · π)))) | ||
Theorem | root1id 24295 | Property of an 𝑁-th root of unity. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ (𝑁 ∈ ℕ → ((-1↑𝑐(2 / 𝑁))↑𝑁) = 1) | ||
Theorem | root1eq1 24296 | 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 24297 | 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 24298* | 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 / 𝑁))↑𝑛)))) | ||
Theorem | loglesqrt 24299 | An upper bound on the logarithm. (Contributed by Mario Carneiro, 2-May-2016.) (Proof shortened by AV, 2-Aug-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (log‘(𝐴 + 1)) ≤ (√‘𝐴)) | ||
Theorem | logreclem 24300 | Symmetry of the natural logarithm range by negation. Lemma for logrec 24301. (Contributed by Saveliy Skresanov, 27-Dec-2016.) |
⊢ ((𝐴 ∈ ran log ∧ ¬ (ℑ‘𝐴) = π) → -𝐴 ∈ ran log) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |