Metamath Proof Explorer


Theorem gzcjcl

Description: The gaussian integers are closed under conjugation. (Contributed by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion gzcjcl AiAi

Proof

Step Hyp Ref Expression
1 gzcn AiA
2 1 cjcld AiA
3 1 recjd AiA=A
4 elgz AiAAA
5 4 simp2bi AiA
6 3 5 eqeltrd AiA
7 1 imcjd AiA=A
8 4 simp3bi AiA
9 8 znegcld AiA
10 7 9 eqeltrd AiA
11 elgz AiAAA
12 2 6 10 11 syl3anbrc AiAi