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	$$⊢\phi \to A\in ℂ$$
Assertion	exp4sqsq	$$⊢\phi \to A^4={\left(A^2\right)}^2$$

Proof

Step	Hyp	Ref	Expression
1		exp4sqsq.a	$$⊢\phi \to A\in ℂ$$
2		2t2e4	$$⊢2\cdot 2=4$$
3	2	oveq2i	$$⊢A^{2\cdot 2}=A^4$$
4		2nn0	$$⊢2\in {\mathbb{N}}_0$$
5	4	a1i	$$⊢\phi \to 2\in {\mathbb{N}}_0$$
6	1 5 5	expmuld	$$⊢\phi \to A^{2\cdot 2}={\left(A^2\right)}^2$$
7	3 6	eqtr3id	$$⊢\phi \to A^4={\left(A^2\right)}^2$$