Metamath Proof Explorer


Theorem denexp

Description: densq extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023)

Ref Expression
Assertion denexp AN0denomAN=denomAN

Proof

Step Hyp Ref Expression
1 numdenexp AN0numerAN=numerANdenomAN=denomAN
2 1 simprd AN0denomAN=denomAN