Theorem exp4sqsq

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

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

Proof

Step	Hyp	Ref	Expression
1		exp4sqsq.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 ) )