Metamath Proof Explorer


Theorem flt4lem

Description: Raising a number to the fourth power is equivalent to squaring it twice. (Contributed by SN, 21-Aug-2024)

Ref Expression
Hypothesis flt4lem.a
|- ( ph -> A e. CC )
Assertion flt4lem
|- ( ph -> ( A ^ 4 ) = ( ( A ^ 2 ) ^ 2 ) )

Proof

Step Hyp Ref Expression
1 flt4lem.a
 |-  ( ph -> A e. CC )
2 2t2e4
 |-  ( 2 x. 2 ) = 4
3 2 oveq2i
 |-  ( A ^ ( 2 x. 2 ) ) = ( A ^ 4 )
4 2nn0
 |-  2 e. NN0
5 4 a1i
 |-  ( ph -> 2 e. NN0 )
6 1 5 5 expmuld
 |-  ( ph -> ( A ^ ( 2 x. 2 ) ) = ( ( A ^ 2 ) ^ 2 ) )
7 3 6 eqtr3id
 |-  ( ph -> ( A ^ 4 ) = ( ( A ^ 2 ) ^ 2 ) )