Description: The gaussian integers are closed under conjugation. (Contributed by Mario Carneiro, 14-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | gzcjcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gzcn | |
|
2 | 1 | cjcld | |
3 | 1 | recjd | |
4 | elgz | |
|
5 | 4 | simp2bi | |
6 | 3 5 | eqeltrd | |
7 | 1 | imcjd | |
8 | 4 | simp3bi | |
9 | 8 | znegcld | |
10 | 7 9 | eqeltrd | |
11 | elgz | |
|
12 | 2 6 10 11 | syl3anbrc | |