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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
Assertion	exp4sqsq	⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) = ( ( 𝐴 ↑ 2 ) ↑ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		exp4sqsq.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		2t2e4	⊢ ( 2 · 2 ) = 4
3	2	oveq2i	⊢ ( 𝐴 ↑ ( 2 · 2 ) ) = ( 𝐴 ↑ 4 )
4		2nn0	⊢ 2 ∈ ℕ0
5	4	a1i	⊢ ( 𝜑 → 2 ∈ ℕ0 )
6	1 5 5	expmuld	⊢ ( 𝜑 → ( 𝐴 ↑ ( 2 · 2 ) ) = ( ( 𝐴 ↑ 2 ) ↑ 2 ) )
7	3 6	eqtr3id	⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) = ( ( 𝐴 ↑ 2 ) ↑ 2 ) )