Description: Square can be moved in and out of absolute value. (Contributed by Scott Fenton, 18-Apr-2014) (Proof shortened by Mario Carneiro, 29-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | abssq | |- ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( abs ` ( A ^ 2 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2nn0 | |- 2 e. NN0 |
|
| 2 | absexp | |- ( ( A e. CC /\ 2 e. NN0 ) -> ( abs ` ( A ^ 2 ) ) = ( ( abs ` A ) ^ 2 ) ) |
|
| 3 | 1 2 | mpan2 | |- ( A e. CC -> ( abs ` ( A ^ 2 ) ) = ( ( abs ` A ) ^ 2 ) ) |
| 4 | 3 | eqcomd | |- ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( abs ` ( A ^ 2 ) ) ) |