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 φ A
Assertion flt4lem φ A 4 = A 2 2

Proof

Step Hyp Ref Expression
1 flt4lem.a φ A
2 2t2e4 2 2 = 4
3 2 oveq2i A 2 2 = A 4
4 2nn0 2 0
5 4 a1i φ 2 0
6 1 5 5 expmuld φ A 2 2 = A 2 2
7 3 6 eqtr3id φ A 4 = A 2 2