![]() |
Metamath
Proof Explorer Theorem List (p. 263 of 479) | < 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-30158) |
![]() (30159-31681) |
![]() (31682-47805) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cxpsqrtlem 26201 | Lemma for cxpsqrt 26202. (Contributed by Mario Carneiro, 2-Aug-2014.) |
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ดโ๐(1 / 2)) = -(โโ๐ด)) โ (i ยท (โโ๐ด)) โ โ) | ||
Theorem | cxpsqrt 26202 | 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 26203 | Logarithm of a square root. (Contributed by Mario Carneiro, 5-May-2016.) |
โข (๐ด โ โ+ โ (logโ(โโ๐ด)) = ((logโ๐ด) / 2)) | ||
Theorem | cxp0d 26204 | Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ดโ๐0) = 1) | ||
Theorem | cxp1d 26205 | Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ดโ๐1) = ๐ด) | ||
Theorem | 1cxpd 26206 | Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (1โ๐๐ด) = 1) | ||
Theorem | cxpcld 26207 | Closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ดโ๐๐ต) โ โ) | ||
Theorem | cxpmul2d 26208 | Product of exponents law for complex exponentiation. Variation on cxpmul 26187 with more general conditions on ๐ด and ๐ต when ๐ถ is an integer. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ0) โ โข (๐ โ (๐ดโ๐(๐ต ยท ๐ถ)) = ((๐ดโ๐๐ต)โ๐ถ)) | ||
Theorem | 0cxpd 26209 | Value of the complex power function when the first argument is zero. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (0โ๐๐ด) = 0) | ||
Theorem | cxpexpzd 26210 | Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ ๐ต โ โค) โ โข (๐ โ (๐ดโ๐๐ต) = (๐ดโ๐ต)) | ||
Theorem | cxpefd 26211 | Value of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ดโ๐๐ต) = (expโ(๐ต ยท (logโ๐ด)))) | ||
Theorem | cxpne0d 26212 | Complex exponentiation is nonzero if its base is nonzero. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ดโ๐๐ต) โ 0) | ||
Theorem | cxpp1d 26213 | Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ดโ๐(๐ต + 1)) = ((๐ดโ๐๐ต) ยท ๐ด)) | ||
Theorem | cxpnegd 26214 | Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ดโ๐-๐ต) = (1 / (๐ดโ๐๐ต))) | ||
Theorem | cxpmul2zd 26215 | Generalize cxpmul2 26188 to negative integers. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โค) โ โข (๐ โ (๐ดโ๐(๐ต ยท ๐ถ)) = ((๐ดโ๐๐ต)โ๐ถ)) | ||
Theorem | cxpaddd 26216 | 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 26217 | Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ (๐ดโ๐(๐ต โ ๐ถ)) = ((๐ดโ๐๐ต) / (๐ดโ๐๐ถ))) | ||
Theorem | cxpltd 26218 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 1 < ๐ด) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ (๐ต < ๐ถ โ (๐ดโ๐๐ต) < (๐ดโ๐๐ถ))) | ||
Theorem | cxpled 26219 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 1 < ๐ด) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ (๐ต โค ๐ถ โ (๐ดโ๐๐ต) โค (๐ดโ๐๐ถ))) | ||
Theorem | cxplead 26220 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 1 โค ๐ด) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ต โค ๐ถ) โ โข (๐ โ (๐ดโ๐๐ต) โค (๐ดโ๐๐ถ)) | ||
Theorem | divcxpd 26221 | Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ ((๐ด / ๐ต)โ๐๐ถ) = ((๐ดโ๐๐ถ) / (๐ตโ๐๐ถ))) | ||
Theorem | recxpcld 26222 | Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ดโ๐๐ต) โ โ) | ||
Theorem | cxpge0d 26223 | Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ 0 โค (๐ดโ๐๐ต)) | ||
Theorem | cxple2ad 26224 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ 0 โค ๐ถ) & โข (๐ โ ๐ด โค ๐ต) โ โข (๐ โ (๐ดโ๐๐ถ) โค (๐ตโ๐๐ถ)) | ||
Theorem | cxplt2d 26225 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 โค ๐ต) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ (๐ด < ๐ต โ (๐ดโ๐๐ถ) < (๐ตโ๐๐ถ))) | ||
Theorem | cxple2d 26226 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 โค ๐ต) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ (๐ด โค ๐ต โ (๐ดโ๐๐ถ) โค (๐ตโ๐๐ถ))) | ||
Theorem | mulcxpd 26227 | 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 26228 | Square root theorem over the complex numbers for the complex power function. Theorem I.35 of [Apostol] p. 29. Compare with sqrtth 15307. (Contributed by AV, 23-Dec-2022.) |
โข (๐ด โ โ โ ((โโ๐ด)โ๐2) = ๐ด) | ||
Theorem | 2irrexpq 26229* | 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 16188), 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 26294. (Contributed by AV, 23-Dec-2022.) |
โข โ๐ โ (โ โ โ)โ๐ โ (โ โ โ)(๐โ๐๐) โ โ | ||
Theorem | cxprecd 26230 | Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ ((1 / ๐ด)โ๐๐ต) = (1 / (๐ดโ๐๐ต))) | ||
Theorem | rpcxpcld 26231 | Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ดโ๐๐ต) โ โ+) | ||
Theorem | logcxpd 26232 | Logarithm of a complex power. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (logโ(๐ดโ๐๐ต)) = (๐ต ยท (logโ๐ด))) | ||
Theorem | cxplt3d 26233 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด < 1) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ (๐ต < ๐ถ โ (๐ดโ๐๐ถ) < (๐ดโ๐๐ต))) | ||
Theorem | cxple3d 26234 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด < 1) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ (๐ต โค ๐ถ โ (๐ดโ๐๐ถ) โค (๐ดโ๐๐ต))) | ||
Theorem | cxpmuld 26235 | 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 26236 | Commutative law for real exponentiation. (Contributed by AV, 29-Dec-2022.) |
โข ((๐ด โ โ+ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ดโ๐๐ต)โ๐๐ถ) = ((๐ดโ๐๐ถ)โ๐๐ต)) | ||
Theorem | dvcxp1 26237* | The derivative of a complex power with respect to the first argument. (Contributed by Mario Carneiro, 24-Feb-2015.) |
โข (๐ด โ โ โ (โ D (๐ฅ โ โ+ โฆ (๐ฅโ๐๐ด))) = (๐ฅ โ โ+ โฆ (๐ด ยท (๐ฅโ๐(๐ด โ 1))))) | ||
Theorem | dvcxp2 26238* | The derivative of a complex power with respect to the second argument. (Contributed by Mario Carneiro, 24-Feb-2015.) |
โข (๐ด โ โ+ โ (โ D (๐ฅ โ โ โฆ (๐ดโ๐๐ฅ))) = (๐ฅ โ โ โฆ ((logโ๐ด) ยท (๐ดโ๐๐ฅ)))) | ||
Theorem | dvsqrt 26239 | The derivative of the real square root function. (Contributed by Mario Carneiro, 1-May-2016.) |
โข (โ D (๐ฅ โ โ+ โฆ (โโ๐ฅ))) = (๐ฅ โ โ+ โฆ (1 / (2 ยท (โโ๐ฅ)))) | ||
Theorem | dvcncxp1 26240* | 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 26241* | Derivative of square root function. (Contributed by Brendan Leahy, 18-Dec-2018.) |
โข ๐ท = (โ โ (-โ(,]0)) โ โข (โ D (๐ฅ โ ๐ท โฆ (โโ๐ฅ))) = (๐ฅ โ ๐ท โฆ (1 / (2 ยท (โโ๐ฅ)))) | ||
Theorem | cxpcn 26242* | Domain of continuity of the complex power function. (Contributed by Mario Carneiro, 1-May-2016.) |
โข ๐ท = (โ โ (-โ(,]0)) & โข ๐ฝ = (TopOpenโโfld) & โข ๐พ = (๐ฝ โพt ๐ท) โ โข (๐ฅ โ ๐ท, ๐ฆ โ โ โฆ (๐ฅโ๐๐ฆ)) โ ((๐พ รt ๐ฝ) Cn ๐ฝ) | ||
Theorem | cxpcn2 26243* | 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 26244* | Lemma for cxpcn3 26245. (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 26245* | 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 26246 | Continuity of the real square root function. (Contributed by Mario Carneiro, 2-May-2016.) |
โข (โ โพ (0[,)+โ)) โ ((0[,)+โ)โcnโโ) | ||
Theorem | sqrtcn 26247 | Continuity of the square root function. (Contributed by Mario Carneiro, 2-May-2016.) |
โข ๐ท = (โ โ (-โ(,]0)) โ โข (โ โพ ๐ท) โ (๐ทโcnโโ) | ||
Theorem | cxpaddlelem 26248 | Lemma for cxpaddle 26249. (Contributed by Mario Carneiro, 2-Aug-2014.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ ๐ด โค 1) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ต โค 1) โ โข (๐ โ ๐ด โค (๐ดโ๐๐ต)) | ||
Theorem | cxpaddle 26249 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 8-Sep-2014.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 โค ๐ต) & โข (๐ โ ๐ถ โ โ+) & โข (๐ โ ๐ถ โค 1) โ โข (๐ โ ((๐ด + ๐ต)โ๐๐ถ) โค ((๐ดโ๐๐ถ) + (๐ตโ๐๐ถ))) | ||
Theorem | abscxpbnd 26250 | Bound on the absolute value of a complex power. (Contributed by Mario Carneiro, 15-Sep-2014.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 โค (โโ๐ต)) & โข (๐ โ ๐ โ โ) & โข (๐ โ (absโ๐ด) โค ๐) โ โข (๐ โ (absโ(๐ดโ๐๐ต)) โค ((๐โ๐(โโ๐ต)) ยท (expโ((absโ๐ต) ยท ฯ)))) | ||
Theorem | root1id 26251 | Property of an ๐-th root of unity. (Contributed by Mario Carneiro, 23-Apr-2015.) |
โข (๐ โ โ โ ((-1โ๐(2 / ๐))โ๐) = 1) | ||
Theorem | root1eq1 26252 | 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 26253 | 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 26254* | 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 26255 | 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 26256 | Symmetry of the natural logarithm range by negation. Lemma for logrec 26257. (Contributed by Saveliy Skresanov, 27-Dec-2016.) |
โข ((๐ด โ ran log โง ยฌ (โโ๐ด) = ฯ) โ -๐ด โ ran log) | ||
Theorem | logrec 26257 | 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 26282, logbf 26283 and logbfval 26284. | ||
Syntax | clogb 26258 | Extend class notation to include the logarithm generalized to an arbitrary base. |
class logb | ||
Definition | df-logb 26259* | 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 26260 | 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 26261 | General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017.) |
โข ((๐ต โ (โ โ {0, 1}) โง ๐ โ (โ โ {0})) โ (๐ต logb ๐) โ โ) | ||
Theorem | logbid1 26262 | 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 26263 | The logarithm of 1 to an arbitrary base ๐ต is 0. Property 1(b) of [Cohen4] p. 361. See log1 26085. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.) |
โข ((๐ต โ โ โง ๐ต โ 0 โง ๐ต โ 1) โ (๐ต logb 1) = 0) | ||
Theorem | elogb 26264 | 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 26265 | 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 26266 | Value of the general logarithm with integer base. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
โข ((๐ต โ (โคโฅโ2) โง ๐ โ โ+) โ (๐ต logb ๐) = ((logโ๐) / (logโ๐ต))) | ||
Theorem | relogbcl 26267 | 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 26268 | 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 26269 | 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 26270 | 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 26271 | 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 26272 | 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 26273 | 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 26274 | 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 26275 | 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 26276 | Logarithm of a reciprocal changes sign. See logrec 26257. Particular case of Property 3 of [Cohen4] p. 361. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
โข ((๐ต โ (โคโฅโ2) โง ๐ด โ โ+) โ (๐ต logb (1 / ๐ด)) = -(๐ต logb ๐ด)) | ||
Theorem | logbleb 26277 | The general logarithm function is monotone/increasing. See logleb 26102. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by AV, 31-May-2020.) |
โข ((๐ต โ (โคโฅโ2) โง ๐ โ โ+ โง ๐ โ โ+) โ (๐ โค ๐ โ (๐ต logb ๐) โค (๐ต logb ๐))) | ||
Theorem | logblt 26278 | The general logarithm function is strictly monotone/increasing. Property 2 of [Cohen4] p. 377. See logltb 26099. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.) |
โข ((๐ต โ (โคโฅโ2) โง ๐ โ โ+ โง ๐ โ โ+) โ (๐ < ๐ โ (๐ต logb ๐) < (๐ต logb ๐))) | ||
Theorem | relogbcxp 26279 | Identity law for the general logarithm for real numbers. (Contributed by AV, 22-May-2020.) |
โข ((๐ต โ (โ+ โ {1}) โง ๐ โ โ) โ (๐ต logb (๐ตโ๐๐)) = ๐) | ||
Theorem | cxplogb 26280 | Identity law for the general logarithm. (Contributed by AV, 22-May-2020.) |
โข ((๐ต โ (โ โ {0, 1}) โง ๐ โ (โ โ {0})) โ (๐ตโ๐(๐ต logb ๐)) = ๐) | ||
Theorem | relogbcxpb 26281 | The logarithm is the inverse of the exponentiation. Observation in [Cohen4] p. 348. (Contributed by AV, 11-Jun-2020.) |
โข (((๐ต โ โ+ โง ๐ต โ 1) โง ๐ โ โ+ โง ๐ โ โ) โ ((๐ต logb ๐) = ๐ โ (๐ตโ๐๐) = ๐)) | ||
Theorem | logbmpt 26282* | 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 26283 | The general logarithm to a fixed base regarded as function. (Contributed by AV, 11-Jun-2020.) |
โข ((๐ต โ โ โง ๐ต โ 0 โง ๐ต โ 1) โ (curry logb โ๐ต):(โ โ {0})โถโ) | ||
Theorem | logbfval 26284 | 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 26285 | 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 26286 | 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 26287 | 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 26288 | 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 26289). (Contributed by AV, 29-Dec-2022.) |
โข ((๐ โ (โคโฅโ2) โง ๐ต โ (โคโฅโ2) โง (๐ gcd ๐ต) = 1) โ (๐ต logb ๐) โ (โ โ โ)) | ||
Theorem | 2logb9irr 26289 | Example for logbgcd1irr 26288. The logarithm of nine to base two is irrational. (Contributed by AV, 29-Dec-2022.) |
โข (2 logb 9) โ (โ โ โ) | ||
Theorem | logbprmirr 26290 | The logarithm of a prime to a different prime base is an irrational number. For example, (2 logb 3) โ (โ โ โ) (see 2logb3irr 26291). (Contributed by AV, 31-Dec-2022.) |
โข ((๐ โ โ โง ๐ต โ โ โง ๐ โ ๐ต) โ (๐ต logb ๐) โ (โ โ โ)) | ||
Theorem | 2logb3irr 26291 | Example for logbprmirr 26290. The logarithm of three to base two is irrational. (Contributed by AV, 31-Dec-2022.) |
โข (2 logb 3) โ (โ โ โ) | ||
Theorem | 2logb9irrALT 26292 | Alternate proof of 2logb9irr 26289: The logarithm of nine to base two is irrational. (Contributed by AV, 31-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข (2 logb 9) โ (โ โ โ) | ||
Theorem | sqrt2cxp2logb9e3 26293 | The square root of two to the power of the logarithm of nine to base two is three. (โโ2) and (2 logb 9) are irrational numbers (see sqrt2irr0 16190 resp. 2logb9irr 26289), satisfying the statement in 2irrexpqALT 26294. (Contributed by AV, 29-Dec-2022.) |
โข ((โโ2)โ๐(2 logb 9)) = 3 | ||
Theorem | 2irrexpqALT 26294* | Alternate proof of 2irrexpq 26229: 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 "constructive proof" for theorem 1.2 of [Bauer], p. 483. In contrast to 2irrexpq 26229, this is a constructive proof because it is based on two explicitly named irrational numbers (โโ2) and (2 logb 9), see sqrt2irr0 16190, 2logb9irr 26289 and sqrt2cxp2logb9e3 26293. Therefore, this proof is also acceptable/usable in intuitionistic logic. (Contributed by AV, 23-Dec-2022.) (New usage is discouraged.) (Proof modification is discouraged.) |
โข โ๐ โ (โ โ โ)โ๐ โ (โ โ โ)(๐โ๐๐) โ โ | ||
Theorem | angval 26295* | Define the angle function, which takes two complex numbers, treated as vectors from the origin, and returns the angle between them, in the range ( โ ฯ, ฯ]. To convert from the geometry notation, ๐๐ด๐ต๐ถ, the measure of the angle with legs ๐ด๐ต, ๐ถ๐ต where ๐ถ is more counterclockwise for positive angles, is represented by ((๐ถ โ ๐ต)๐น(๐ด โ ๐ต)). (Contributed by Mario Carneiro, 23-Sep-2014.) |
โข ๐น = (๐ฅ โ (โ โ {0}), ๐ฆ โ (โ โ {0}) โฆ (โโ(logโ(๐ฆ / ๐ฅ)))) โ โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ด๐น๐ต) = (โโ(logโ(๐ต / ๐ด)))) | ||
Theorem | angcan 26296* | Cancel a constant multiplier in the angle function. (Contributed by Mario Carneiro, 23-Sep-2014.) |
โข ๐น = (๐ฅ โ (โ โ {0}), ๐ฆ โ (โ โ {0}) โฆ (โโ(logโ(๐ฆ / ๐ฅ)))) โ โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((๐ถ ยท ๐ด)๐น(๐ถ ยท ๐ต)) = (๐ด๐น๐ต)) | ||
Theorem | angneg 26297* | Cancel a negative sign in the angle function. (Contributed by Mario Carneiro, 23-Sep-2014.) |
โข ๐น = (๐ฅ โ (โ โ {0}), ๐ฆ โ (โ โ {0}) โฆ (โโ(logโ(๐ฆ / ๐ฅ)))) โ โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (-๐ด๐น-๐ต) = (๐ด๐น๐ต)) | ||
Theorem | angvald 26298* | The (signed) angle between two vectors is the argument of their quotient. Deduction form of angval 26295. (Contributed by David Moews, 28-Feb-2017.) |
โข ๐น = (๐ฅ โ (โ โ {0}), ๐ฆ โ (โ โ {0}) โฆ (โโ(logโ(๐ฆ / ๐ฅ)))) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ 0) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ 0) โ โข (๐ โ (๐๐น๐) = (โโ(logโ(๐ / ๐)))) | ||
Theorem | angcld 26299* | The (signed) angle between two vectors is in (-ฯ(,]ฯ). Deduction form. (Contributed by David Moews, 28-Feb-2017.) |
โข ๐น = (๐ฅ โ (โ โ {0}), ๐ฆ โ (โ โ {0}) โฆ (โโ(logโ(๐ฆ / ๐ฅ)))) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ 0) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ 0) โ โข (๐ โ (๐๐น๐) โ (-ฯ(,]ฯ)) | ||
Theorem | angrteqvd 26300* | Two vectors are at a right angle iff their quotient is purely imaginary. (Contributed by David Moews, 28-Feb-2017.) |
โข ๐น = (๐ฅ โ (โ โ {0}), ๐ฆ โ (โ โ {0}) โฆ (โโ(logโ(๐ฆ / ๐ฅ)))) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ 0) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ 0) โ โข (๐ โ ((๐๐น๐) โ {(ฯ / 2), -(ฯ / 2)} โ (โโ(๐ / ๐)) = 0)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |