This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Step	Hyp	Ref	Expression
1		flt4lem.a	$⊢ φ \to A \in ℂ$
2		2t2e4	$⊢ 2 \cdot 2 = 4$
3	2	oveq2i	$⊢ A^{2 \cdot 2} = A^{4}$
4		2nn0	$⊢ 2 \in ℕ_{0}$
5	4	a1i	$⊢ φ \to 2 \in ℕ_{0}$
6	1 5 5	expmuld	$⊢ φ \to A^{2 \cdot 2} = {(A^{2})}^{2}$
7	3 6	eqtr3id	$⊢ φ \to A^{4} = {(A^{2})}^{2}$