Metamath Proof Explorer


Theorem sqdivid

Description: The square of a nonzero complex number divided by itself equals that number. (Contributed by AV, 19-Jul-2021)

Ref Expression
Assertion sqdivid AA0A2A=A

Proof

Step Hyp Ref Expression
1 sqval AA2=AA
2 1 adantr AA0A2=AA
3 2 oveq1d AA0A2A=AAA
4 divcan3 AAA0AAA=A
5 4 3anidm12 AA0AAA=A
6 3 5 eqtrd AA0A2A=A