Here's one way to find that theorem. First I tried:
search * '( ( ? ^ ? ) ^ ? )'
(using metamath-exe). But then I remembered that ^ is for an integer
exponent so I better try ^c instead. So the search
search * '( ( ? ^c ? ) ^c ? )'
finds cxpmul. That indeed has the restrictions described by Mario.
On 7/4/25 04:13, Mario Carneiro 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/CAFXXJSsdjOPDC-BXUbRrEiH%2BA5A4sZbDYMgHjRHhoDSdV3Th6Q%40mail.gmail.com
<https://groups.google.com/d/msgid/metamath/CAFXXJSsdjOPDC-BXUbRrEiH%2BA5A4sZbDYMgHjRHhoDSdV3Th6Q%40mail.gmail.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/293096f4-f9d7-4cd3-8d41-16a2f1514995%40panix.com.
