I see, thank you for pointing me to the correct resource, I'm starting to get the hang of metamath better now.
On Friday, 4 July 2025 at 13:13:22 UTC+2 [email protected] wrote: > The theorem you are looking for is > https://us.metamath.org/mpeuni/cxpmul.html . Note that the assumptions > are a bit different from what you have assumed: the complex power function > works in general for arbitrary complex numbers rather than rational > numbers, but because of various issues around branch cuts these kinds of > theorems usually don't hold over the whole domain. This particular theorem, > x^(ab) = (x^a)^b, is true as long as x is a positive real number and a,b > are real numbers. (The formal theorem allows b to be complex, but not a.) > > On Fri, Jul 4, 2025 at 1:02 PM Alessandro Griseta <[email protected]> > wrote: > >> As a future university student who has just finished High School, it's >> very easy for me to randomly have some doubt about a proof. >> >> As a consequence I believe metamath has the incredible potential to allow >> anyone learning mathematics to fill gaps in their own knowledge and making >> the proof-memorising process (= basis of mathematics!) much more precise >> and methodical. Therefore the organisation has an excellent potential to >> become a valuable OER (Open Educational Resource). >> >> Having said that, it's often quite hard to find the 'right' proof in the >> giant database metamath provides (`mmset`). >> >> Here is an example: >> >> $(x^a)^b=x^{a\cdot b} \land a,b \in\mathbb{Q}$ >> >> ^^^ it isn't very formally explained here, but basically I'm looking for >> the proof that the power of a power is equal to the multiplication of >> powers, *even when the powers are rational numbers*. >> >> Any suggestions for pin-pointing the exact proof? I'd love to use and >> contribute to this database, but sadly, a bit like in real life, if I own >> something but I've lost it, it's like not owning it at all! >> >> I'd also be happy to test out similar tools/resources. Otherwise, if you >> think I need some preliminary knowledge, please feel free to post links! >> Perhaps my problem is that I don't understand in which 'topics' metamath is >> grouped in, although I'm so new to metamath and its innovative approach >> that I'd appreciate some guidance first! >> >> Thank you very much for your patience, I'll look forward to any kind of >> reply! >> >> Alessandro >> >> -- >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion visit >> https://groups.google.com/d/msgid/metamath/1252faeb-9c6a-4932-bff9-8f9f3c679016n%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/1252faeb-9c6a-4932-bff9-8f9f3c679016n%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/e7e9b84b-cc3b-4bd5-8b09-da3ab0ed0bc9n%40googlegroups.com.
