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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cxpmul2z 25201 | Generalize cxpmul2 25199 to negative integers. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℤ)) → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
Theorem | abscxp 25202 | Absolute value of a power, when the base is real. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴↑𝑐𝐵)) = (𝐴↑𝑐(ℜ‘𝐵))) | ||
Theorem | abscxp2 25203 | Absolute value of a power, when the exponent is real. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ) → (abs‘(𝐴↑𝑐𝐵)) = ((abs‘𝐴)↑𝑐𝐵)) | ||
Theorem | cxplt 25204 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐵) < (𝐴↑𝑐𝐶))) | ||
Theorem | cxple 25205 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶))) | ||
Theorem | cxplea 25206 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 10-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐵 ≤ 𝐶) → (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶)) | ||
Theorem | cxple2 25207 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶))) | ||
Theorem | cxplt2 25208 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐴↑𝑐𝐶) < (𝐵↑𝑐𝐶))) | ||
Theorem | cxple2a 25209 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐶) ∧ 𝐴 ≤ 𝐵) → (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶)) | ||
Theorem | cxplt3 25210 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐴 < 1) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐶) < (𝐴↑𝑐𝐵))) | ||
Theorem | cxple3 25211 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐴 < 1) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐶) ≤ (𝐴↑𝑐𝐵))) | ||
Theorem | cxpsqrtlem 25212 | Lemma for cxpsqrt 25213. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐴↑𝑐(1 / 2)) = -(√‘𝐴)) → (i · (√‘𝐴)) ∈ ℝ) | ||
Theorem | cxpsqrt 25213 | 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 25214 | Logarithm of a square root. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ (𝐴 ∈ ℝ+ → (log‘(√‘𝐴)) = ((log‘𝐴) / 2)) | ||
Theorem | cxp0d 25215 | Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐0) = 1) | ||
Theorem | cxp1d 25216 | Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐1) = 𝐴) | ||
Theorem | 1cxpd 25217 | Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (1↑𝑐𝐴) = 1) | ||
Theorem | cxpcld 25218 | Closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℂ) | ||
Theorem | cxpmul2d 25219 | Product of exponents law for complex exponentiation. Variation on cxpmul 25198 with more general conditions on 𝐴 and 𝐵 when 𝐶 is an integer. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
Theorem | 0cxpd 25220 | Value of the complex power function when the first argument is zero. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (0↑𝑐𝐴) = 0) | ||
Theorem | cxpexpzd 25221 | Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) = (𝐴↑𝐵)) | ||
Theorem | cxpefd 25222 | Value of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴)))) | ||
Theorem | cxpne0d 25223 | Complex exponentiation is nonzero if its mantissa is nonzero. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ≠ 0) | ||
Theorem | cxpp1d 25224 | Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 + 1)) = ((𝐴↑𝑐𝐵) · 𝐴)) | ||
Theorem | cxpnegd 25225 | Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐-𝐵) = (1 / (𝐴↑𝑐𝐵))) | ||
Theorem | cxpmul2zd 25226 | Generalize cxpmul2 25199 to negative integers. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶)) | ||
Theorem | cxpaddd 25227 | 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 25228 | Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 − 𝐶)) = ((𝐴↑𝑐𝐵) / (𝐴↑𝑐𝐶))) | ||
Theorem | cxpltd 25229 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 < 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐵) < (𝐴↑𝑐𝐶))) | ||
Theorem | cxpled 25230 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 < 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶))) | ||
Theorem | cxplead 25231 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶)) | ||
Theorem | divcxpd 25232 | Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) / (𝐵↑𝑐𝐶))) | ||
Theorem | recxpcld 25233 | Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℝ) | ||
Theorem | cxpge0d 25234 | Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴↑𝑐𝐵)) | ||
Theorem | cxple2ad 25235 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶)) | ||
Theorem | cxplt2d 25236 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴↑𝑐𝐶) < (𝐵↑𝑐𝐶))) | ||
Theorem | cxple2d 25237 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶))) | ||
Theorem | mulcxpd 25238 | Complex exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) · (𝐵↑𝑐𝐶))) | ||
Theorem | cxpsqrtth 25239 | Square root theorem over the complex numbers for the complex power function. Theorem I.35 of [Apostol] p. 29. Compare with sqrtth 14714. (Contributed by AV, 23-Dec-2022.) |
⊢ (𝐴 ∈ ℂ → ((√‘𝐴)↑𝑐2) = 𝐴) | ||
Theorem | 2irrexpq 25240* | 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 15592), 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 25305. (Contributed by AV, 23-Dec-2022.) |
⊢ ∃𝑎 ∈ (ℝ ∖ ℚ)∃𝑏 ∈ (ℝ ∖ ℚ)(𝑎↑𝑐𝑏) ∈ ℚ | ||
Theorem | cxprecd 25241 | Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((1 / 𝐴)↑𝑐𝐵) = (1 / (𝐴↑𝑐𝐵))) | ||
Theorem | rpcxpcld 25242 | Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℝ+) | ||
Theorem | logcxpd 25243 | Logarithm of a complex power. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴))) | ||
Theorem | cxplt3d 25244 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐶) < (𝐴↑𝑐𝐵))) | ||
Theorem | cxple3d 25245 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐶) ≤ (𝐴↑𝑐𝐵))) | ||
Theorem | cxpmuld 25246 | Product of exponents law for complex exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝑐𝐶)) | ||
Theorem | cxpcom 25247 | Commutative law for real exponentiation. (Contributed by AV, 29-Dec-2022.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴↑𝑐𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶)↑𝑐𝐵)) | ||
Theorem | dvcxp1 25248* | The derivative of a complex power with respect to the first argument. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝐴 ∈ ℂ → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥↑𝑐𝐴))) = (𝑥 ∈ ℝ+ ↦ (𝐴 · (𝑥↑𝑐(𝐴 − 1))))) | ||
Theorem | dvcxp2 25249* | The derivative of a complex power with respect to the second argument. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝐴 ∈ ℝ+ → (ℂ D (𝑥 ∈ ℂ ↦ (𝐴↑𝑐𝑥))) = (𝑥 ∈ ℂ ↦ ((log‘𝐴) · (𝐴↑𝑐𝑥)))) | ||
Theorem | dvsqrt 25250 | The derivative of the real square root function. (Contributed by Mario Carneiro, 1-May-2016.) |
⊢ (ℝ D (𝑥 ∈ ℝ+ ↦ (√‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (1 / (2 · (√‘𝑥)))) | ||
Theorem | dvcncxp1 25251* | 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 25252* | Derivative of square root function. (Contributed by Brendan Leahy, 18-Dec-2018.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (ℂ D (𝑥 ∈ 𝐷 ↦ (√‘𝑥))) = (𝑥 ∈ 𝐷 ↦ (1 / (2 · (√‘𝑥)))) | ||
Theorem | cxpcn 25253* | Domain of continuity of the complex power function. (Contributed by Mario Carneiro, 1-May-2016.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝐷) ⇒ ⊢ (𝑥 ∈ 𝐷, 𝑦 ∈ ℂ ↦ (𝑥↑𝑐𝑦)) ∈ ((𝐾 ×t 𝐽) Cn 𝐽) | ||
Theorem | cxpcn2 25254* | 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 25255* | Lemma for cxpcn3 25256. (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 25256* | 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 25257 | Continuity of the real square root function. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ (√ ↾ (0[,)+∞)) ∈ ((0[,)+∞)–cn→ℝ) | ||
Theorem | sqrtcn 25258 | Continuity of the square root function. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) ⇒ ⊢ (√ ↾ 𝐷) ∈ (𝐷–cn→ℂ) | ||
Theorem | cxpaddlelem 25259 | Lemma for cxpaddle 25260. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 1) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ≤ 1) ⇒ ⊢ (𝜑 → 𝐴 ≤ (𝐴↑𝑐𝐵)) | ||
Theorem | cxpaddle 25260 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 8-Sep-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ≤ 1) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵)↑𝑐𝐶) ≤ ((𝐴↑𝑐𝐶) + (𝐵↑𝑐𝐶))) | ||
Theorem | abscxpbnd 25261 | Bound on the absolute value of a complex power. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 0 ≤ (ℜ‘𝐵)) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐴) ≤ 𝑀) ⇒ ⊢ (𝜑 → (abs‘(𝐴↑𝑐𝐵)) ≤ ((𝑀↑𝑐(ℜ‘𝐵)) · (exp‘((abs‘𝐵) · π)))) | ||
Theorem | root1id 25262 | Property of an 𝑁-th root of unity. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ (𝑁 ∈ ℕ → ((-1↑𝑐(2 / 𝑁))↑𝑁) = 1) | ||
Theorem | root1eq1 25263 | 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 25264 | 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 25265* | 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 25266 | 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 25267 | Symmetry of the natural logarithm range by negation. Lemma for logrec 25268. (Contributed by Saveliy Skresanov, 27-Dec-2016.) |
⊢ ((𝐴 ∈ ran log ∧ ¬ (ℑ‘𝐴) = π) → -𝐴 ∈ ran log) | ||
Theorem | logrec 25268 | Logarithm of a reciprocal changes sign. (Contributed by Saveliy Skresanov, 28-Dec-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ (ℑ‘(log‘𝐴)) ≠ π) → (log‘𝐴) = -(log‘(1 / 𝐴))) | ||
Define "log using an arbitrary base" function and then prove some of its properties. Note that logb is generalized to an arbitrary base and arbitrary parameter in ℂ, but it doesn't accept infinities as arguments, unlike log. Metamath doesn't care what letters are used to represent classes. Usually classes begin with the letter "A", but here we use "B" and "X" to more clearly distinguish between "base" and "other parameter of log". There are different ways this could be defined in Metamath. The approach used here is intentionally similar to existing 2-parameter Metamath functions (operations): (𝐵 logb 𝑋) where 𝐵 is the base and 𝑋 is the argument of the logarithm function. An alternative would be to support the notational form (( logb ‘𝐵)‘𝑋); that looks a little more like traditional notation. Such a function ( logb ‘𝐵) for a fixed base can be obtained in Metamath (without the need for a new definition) by the curry function: (curry logb ‘𝐵), see logbmpt 25293, logbf 25294 and logbfval 25295. | ||
Syntax | clogb 25269 | Extend class notation to include the logarithm generalized to an arbitrary base. |
class logb | ||
Definition | df-logb 25270* | Define the logb operator. This is the logarithm generalized to an arbitrary base. It can be used as (𝐵 logb 𝑋) for "log base B of X". In the most common traditional notation, base B is a subscript of "log". The definition is according to Wikipedia "Complex logarithm": https://en.wikipedia.org/wiki/Complex_logarithm#Logarithms_to_other_bases (10-Jun-2020). (Contributed by David A. Wheeler, 21-Jan-2017.) |
⊢ logb = (𝑥 ∈ (ℂ ∖ {0, 1}), 𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝑥))) | ||
Theorem | logbval 25271 | Define the value of the logb function, the logarithm generalized to an arbitrary base, when used as infix. Most Metamath statements select variables in order of their use, but to make the order clearer we use "B" for base and "X" for the argument of the logarithm function here. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by David A. Wheeler, 16-Jul-2017.) |
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵 logb 𝑋) = ((log‘𝑋) / (log‘𝐵))) | ||
Theorem | logbcl 25272 | General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017.) |
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵 logb 𝑋) ∈ ℂ) | ||
Theorem | logbid1 25273 | General logarithm is 1 when base and arg match. Property 1(a) of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by David A. Wheeler, 22-Jul-2017.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝐴 logb 𝐴) = 1) | ||
Theorem | logb1 25274 | The logarithm of 1 to an arbitrary base 𝐵 is 0. Property 1(b) of [Cohen4] p. 361. See log1 25096. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.) |
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (𝐵 logb 1) = 0) | ||
Theorem | elogb 25275 | The general logarithm of a number to the base being Euler's constant is the natural logarithm of the number. Put another way, using e as the base in logb is the same as log. Definition in [Cohen4] p. 352. (Contributed by David A. Wheeler, 17-Oct-2017.) (Revised by David A. Wheeler and AV, 16-Jun-2020.) |
⊢ (𝐴 ∈ (ℂ ∖ {0}) → (e logb 𝐴) = (log‘𝐴)) | ||
Theorem | logbchbase 25276 | Change of base for logarithms. Property in [Cohen4] p. 367. (Contributed by AV, 11-Jun-2020.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐴 logb 𝑋) = ((𝐵 logb 𝑋) / (𝐵 logb 𝐴))) | ||
Theorem | relogbval 25277 | Value of the general logarithm with integer base. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+) → (𝐵 logb 𝑋) = ((log‘𝑋) / (log‘𝐵))) | ||
Theorem | relogbcl 25278 | Closure of the general logarithm with a positive real base on positive reals. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.) |
⊢ ((𝐵 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+ ∧ 𝐵 ≠ 1) → (𝐵 logb 𝑋) ∈ ℝ) | ||
Theorem | relogbzcl 25279 | Closure of the general logarithm with integer base on positive reals. (Contributed by Thierry Arnoux, 27-Sep-2017.) (Proof shortened by AV, 9-Jun-2020.) |
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+) → (𝐵 logb 𝑋) ∈ ℝ) | ||
Theorem | relogbreexp 25280 | Power law for the general logarithm for real powers: The logarithm of a positive real number to the power of a real number is equal to the product of the exponent and the logarithm of the base of the power. Property 4 of [Cohen4] p. 361. (Contributed by AV, 9-Jun-2020.) |
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ) → (𝐵 logb (𝐶↑𝑐𝐸)) = (𝐸 · (𝐵 logb 𝐶))) | ||
Theorem | relogbzexp 25281 | Power law for the general logarithm for integer powers: The logarithm of a positive real number to the power of an integer is equal to the product of the exponent and the logarithm of the base of the power. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 9-Jun-2020.) |
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐵 logb (𝐶↑𝑁)) = (𝑁 · (𝐵 logb 𝐶))) | ||
Theorem | relogbmul 25282 | The logarithm of the product of two positive real numbers is the sum of logarithms. Property 2 of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 29-May-2020.) |
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ (𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+)) → (𝐵 logb (𝐴 · 𝐶)) = ((𝐵 logb 𝐴) + (𝐵 logb 𝐶))) | ||
Theorem | relogbmulexp 25283 | The logarithm of the product of a positive real and a positive real number to the power of a real number is the sum of the logarithm of the first real number and the scaled logarithm of the second real number. (Contributed by AV, 29-May-2020.) |
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ (𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ)) → (𝐵 logb (𝐴 · (𝐶↑𝑐𝐸))) = ((𝐵 logb 𝐴) + (𝐸 · (𝐵 logb 𝐶)))) | ||
Theorem | relogbdiv 25284 | The logarithm of the quotient of two positive real numbers is the difference of logarithms. Property 3 of [Cohen4] p. 361. (Contributed by AV, 29-May-2020.) |
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ (𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+)) → (𝐵 logb (𝐴 / 𝐶)) = ((𝐵 logb 𝐴) − (𝐵 logb 𝐶))) | ||
Theorem | relogbexp 25285 | Identity law for general logarithm: the logarithm of a power to the base is the exponent. Property 6 of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 9-Jun-2020.) |
⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ∧ 𝑀 ∈ ℤ) → (𝐵 logb (𝐵↑𝑀)) = 𝑀) | ||
Theorem | nnlogbexp 25286 | Identity law for general logarithm with integer base. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.) |
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → (𝐵 logb (𝐵↑𝑀)) = 𝑀) | ||
Theorem | logbrec 25287 | Logarithm of a reciprocal changes sign. See logrec 25268. Particular case of Property 3 of [Cohen4] p. 361. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℝ+) → (𝐵 logb (1 / 𝐴)) = -(𝐵 logb 𝐴)) | ||
Theorem | logbleb 25288 | The general logarithm function is monotone/increasing. See logleb 25113. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by AV, 31-May-2020.) |
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+) → (𝑋 ≤ 𝑌 ↔ (𝐵 logb 𝑋) ≤ (𝐵 logb 𝑌))) | ||
Theorem | logblt 25289 | The general logarithm function is strictly monotone/increasing. Property 2 of [Cohen4] p. 377. See logltb 25110. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.) |
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+) → (𝑋 < 𝑌 ↔ (𝐵 logb 𝑋) < (𝐵 logb 𝑌))) | ||
Theorem | relogbcxp 25290 | Identity law for the general logarithm for real numbers. (Contributed by AV, 22-May-2020.) |
⊢ ((𝐵 ∈ (ℝ+ ∖ {1}) ∧ 𝑋 ∈ ℝ) → (𝐵 logb (𝐵↑𝑐𝑋)) = 𝑋) | ||
Theorem | cxplogb 25291 | Identity law for the general logarithm. (Contributed by AV, 22-May-2020.) |
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵↑𝑐(𝐵 logb 𝑋)) = 𝑋) | ||
Theorem | relogbcxpb 25292 | The logarithm is the inverse of the exponentiation. Observation in [Cohen4] p. 348. (Contributed by AV, 11-Jun-2020.) |
⊢ (((𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → ((𝐵 logb 𝑋) = 𝑌 ↔ (𝐵↑𝑐𝑌) = 𝑋)) | ||
Theorem | logbmpt 25293* | The general logarithm to a fixed base regarded as mapping. (Contributed by AV, 11-Jun-2020.) |
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (curry logb ‘𝐵) = (𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝐵)))) | ||
Theorem | logbf 25294 | The general logarithm to a fixed base regarded as function. (Contributed by AV, 11-Jun-2020.) |
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (curry logb ‘𝐵):(ℂ ∖ {0})⟶ℂ) | ||
Theorem | logbfval 25295 | The general logarithm of a complex number to a fixed base. (Contributed by AV, 11-Jun-2020.) |
⊢ (((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) ∧ 𝑋 ∈ (ℂ ∖ {0})) → ((curry logb ‘𝐵)‘𝑋) = (𝐵 logb 𝑋)) | ||
Theorem | relogbf 25296 | The general logarithm to a real base greater than 1 regarded as function restricted to the positive integers. Property in [Cohen4] p. 349. (Contributed by AV, 12-Jun-2020.) |
⊢ ((𝐵 ∈ ℝ+ ∧ 1 < 𝐵) → ((curry logb ‘𝐵) ↾ ℝ+):ℝ+⟶ℝ) | ||
Theorem | logblog 25297 | The general logarithm to the base being Euler's constant regarded as function is the natural logarithm. (Contributed by AV, 12-Jun-2020.) |
⊢ (curry logb ‘e) = log | ||
Theorem | logbgt0b 25298 | The logarithm of a positive real number to a real base greater than 1 is positive iff the number is greater than 1. (Contributed by AV, 29-Dec-2022.) |
⊢ ((𝐴 ∈ ℝ+ ∧ (𝐵 ∈ ℝ+ ∧ 1 < 𝐵)) → (0 < (𝐵 logb 𝐴) ↔ 1 < 𝐴)) | ||
Theorem | logbgcd1irr 25299 | The logarithm of an integer greater than 1 to an integer base greater than 1 is an irrational number if the argument and the base are relatively prime. For example, (2 logb 9) ∈ (ℝ ∖ ℚ) (see 2logb9irr 25300). (Contributed by AV, 29-Dec-2022.) |
⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2) ∧ (𝑋 gcd 𝐵) = 1) → (𝐵 logb 𝑋) ∈ (ℝ ∖ ℚ)) | ||
Theorem | 2logb9irr 25300 | Example for logbgcd1irr 25299. The logarithm of nine to base two is irrational. (Contributed by AV, 29-Dec-2022.) |
⊢ (2 logb 9) ∈ (ℝ ∖ ℚ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |