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/CAFXXJSsdjOPDC-BXUbRrEiH%2BA5A4sZbDYMgHjRHhoDSdV3Th6Q%40mail.gmail.com.
