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

Proof

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