# Metamath Proof Explorer

## Theorem cjcj

Description: The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of Gleason p. 133. (Contributed by NM, 29-Jul-1999) (Proof shortened by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion cjcj ${⊢}{A}\in ℂ\to \stackrel{‾}{\stackrel{‾}{{A}}}={A}$

### Proof

Step Hyp Ref Expression
1 cjcl ${⊢}{A}\in ℂ\to \stackrel{‾}{{A}}\in ℂ$
2 recj ${⊢}\stackrel{‾}{{A}}\in ℂ\to \Re \left(\stackrel{‾}{\stackrel{‾}{{A}}}\right)=\Re \left(\stackrel{‾}{{A}}\right)$
3 1 2 syl ${⊢}{A}\in ℂ\to \Re \left(\stackrel{‾}{\stackrel{‾}{{A}}}\right)=\Re \left(\stackrel{‾}{{A}}\right)$
4 recj ${⊢}{A}\in ℂ\to \Re \left(\stackrel{‾}{{A}}\right)=\Re \left({A}\right)$
5 3 4 eqtrd ${⊢}{A}\in ℂ\to \Re \left(\stackrel{‾}{\stackrel{‾}{{A}}}\right)=\Re \left({A}\right)$
6 imcj ${⊢}\stackrel{‾}{{A}}\in ℂ\to \Im \left(\stackrel{‾}{\stackrel{‾}{{A}}}\right)=-\Im \left(\stackrel{‾}{{A}}\right)$
7 1 6 syl ${⊢}{A}\in ℂ\to \Im \left(\stackrel{‾}{\stackrel{‾}{{A}}}\right)=-\Im \left(\stackrel{‾}{{A}}\right)$
8 imcj ${⊢}{A}\in ℂ\to \Im \left(\stackrel{‾}{{A}}\right)=-\Im \left({A}\right)$
9 8 negeqd ${⊢}{A}\in ℂ\to -\Im \left(\stackrel{‾}{{A}}\right)=-\left(-\Im \left({A}\right)\right)$
10 imcl ${⊢}{A}\in ℂ\to \Im \left({A}\right)\in ℝ$
11 10 recnd ${⊢}{A}\in ℂ\to \Im \left({A}\right)\in ℂ$
12 11 negnegd ${⊢}{A}\in ℂ\to -\left(-\Im \left({A}\right)\right)=\Im \left({A}\right)$
13 9 12 eqtrd ${⊢}{A}\in ℂ\to -\Im \left(\stackrel{‾}{{A}}\right)=\Im \left({A}\right)$
14 7 13 eqtrd ${⊢}{A}\in ℂ\to \Im \left(\stackrel{‾}{\stackrel{‾}{{A}}}\right)=\Im \left({A}\right)$
15 14 oveq2d ${⊢}{A}\in ℂ\to \mathrm{i}\Im \left(\stackrel{‾}{\stackrel{‾}{{A}}}\right)=\mathrm{i}\Im \left({A}\right)$
16 5 15 oveq12d ${⊢}{A}\in ℂ\to \Re \left(\stackrel{‾}{\stackrel{‾}{{A}}}\right)+\mathrm{i}\Im \left(\stackrel{‾}{\stackrel{‾}{{A}}}\right)=\Re \left({A}\right)+\mathrm{i}\Im \left({A}\right)$
17 cjcl ${⊢}\stackrel{‾}{{A}}\in ℂ\to \stackrel{‾}{\stackrel{‾}{{A}}}\in ℂ$
18 replim ${⊢}\stackrel{‾}{\stackrel{‾}{{A}}}\in ℂ\to \stackrel{‾}{\stackrel{‾}{{A}}}=\Re \left(\stackrel{‾}{\stackrel{‾}{{A}}}\right)+\mathrm{i}\Im \left(\stackrel{‾}{\stackrel{‾}{{A}}}\right)$
19 1 17 18 3syl ${⊢}{A}\in ℂ\to \stackrel{‾}{\stackrel{‾}{{A}}}=\Re \left(\stackrel{‾}{\stackrel{‾}{{A}}}\right)+\mathrm{i}\Im \left(\stackrel{‾}{\stackrel{‾}{{A}}}\right)$
20 replim ${⊢}{A}\in ℂ\to {A}=\Re \left({A}\right)+\mathrm{i}\Im \left({A}\right)$
21 16 19 20 3eqtr4d ${⊢}{A}\in ℂ\to \stackrel{‾}{\stackrel{‾}{{A}}}={A}$