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 ) ) |
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 ) ) |