Metamath Proof Explorer


Theorem sqval

Description: Value of the square of a complex number. (Contributed by Raph Levien, 10-Apr-2004)

Ref Expression
Assertion sqval AA2=AA

Proof

Step Hyp Ref Expression
1 df-2 2=1+1
2 1 oveq2i A2=A1+1
3 1nn0 10
4 expp1 A10A1+1=A1A
5 3 4 mpan2 AA1+1=A1A
6 2 5 eqtrid AA2=A1A
7 exp1 AA1=A
8 7 oveq1d AA1A=AA
9 6 8 eqtrd AA2=AA