Theorem argcj

Description: The argument of the conjugate of a complex number A . (Contributed by Thierry Arnoux, 5-Nov-2025)

	Ref	Expression
Hypotheses	efiargd.1	$$⊢\phi \to A\in ℂ$$
	efiargd.2	$$⊢\phi \to A\ne 0$$
	arginv.1	$$⊢\phi \to \neg -A\in {ℝ}^{+}$$
Assertion	argcj	$$⊢\phi \to \Im \left(\log \bar{A}\right)=-\Im \left(\log A\right)$$

Proof

Step	Hyp	Ref	Expression
1		efiargd.1	$$⊢\phi \to A\in ℂ$$
2		efiargd.2	$$⊢\phi \to A\ne 0$$
3		arginv.1	$$⊢\phi \to \neg -A\in {ℝ}^{+}$$
4		simpr	$$⊢\left(\phi \wedge A\in ℝ\right)\to A\in ℝ$$
5	2	adantr	$$⊢\left(\phi \wedge A\in ℝ\right)\to A\ne 0$$
6	3	adantr	$$⊢\left(\phi \wedge A\in ℝ\right)\to \neg -A\in {ℝ}^{+}$$
7		rpneg	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(A\in {ℝ}^{+}\leftrightarrow \neg -A\in {ℝ}^{+}\right)$$
8	7	biimpar	$$⊢\left(\left(A\in ℝ\wedge A\ne 0\right)\wedge \neg -A\in {ℝ}^{+}\right)\to A\in {ℝ}^{+}$$
9	4 5 6 8	syl21anc	$$⊢\left(\phi \wedge A\in ℝ\right)\to A\in {ℝ}^{+}$$
10	9	relogcld	$$⊢\left(\phi \wedge A\in ℝ\right)\to \log A\in ℝ$$
11	10	reim0d	$$⊢\left(\phi \wedge A\in ℝ\right)\to \Im \left(\log A\right)=0$$
12	4	cjred	$$⊢\left(\phi \wedge A\in ℝ\right)\to \bar{A}=A$$
13	12	fveq2d	$$⊢\left(\phi \wedge A\in ℝ\right)\to \log \bar{A}=\log A$$
14	13	fveq2d	$$⊢\left(\phi \wedge A\in ℝ\right)\to \Im \left(\log \bar{A}\right)=\Im \left(\log A\right)$$
15	11	negeqd	$$⊢\left(\phi \wedge A\in ℝ\right)\to -\Im \left(\log A\right)=-0$$
16		neg0	$$⊢-0=0$$
17	15 16	eqtrdi	$$⊢\left(\phi \wedge A\in ℝ\right)\to -\Im \left(\log A\right)=0$$
18	11 14 17	3eqtr4d	$$⊢\left(\phi \wedge A\in ℝ\right)\to \Im \left(\log \bar{A}\right)=-\Im \left(\log A\right)$$
19	1	adantr	$$⊢\left(\phi \wedge \Im \left(A\right)=0\right)\to A\in ℂ$$
20		simpr	$$⊢\left(\phi \wedge \Im \left(A\right)=0\right)\to \Im \left(A\right)=0$$
21	19 20	reim0bd	$$⊢\left(\phi \wedge \Im \left(A\right)=0\right)\to A\in ℝ$$
22	21	ex	$$⊢\phi \to \left(\Im \left(A\right)=0\to A\in ℝ\right)$$
23	22	necon3bd	$$⊢\phi \to \left(\neg A\in ℝ\to \Im \left(A\right)\ne 0\right)$$
24	23	imp	$$⊢\left(\phi \wedge \neg A\in ℝ\right)\to \Im \left(A\right)\ne 0$$
25		logcj	$$⊢\left(A\in ℂ\wedge \Im \left(A\right)\ne 0\right)\to \log \bar{A}=\overline{\log A}$$
26	1 24 25	syl2an2r	$$⊢\left(\phi \wedge \neg A\in ℝ\right)\to \log \bar{A}=\overline{\log A}$$
27	26	fveq2d	$$⊢\left(\phi \wedge \neg A\in ℝ\right)\to \Im \left(\log \bar{A}\right)=\Im \left(\overline{\log A}\right)$$
28	1	adantr	$$⊢\left(\phi \wedge \neg A\in ℝ\right)\to A\in ℂ$$
29	2	adantr	$$⊢\left(\phi \wedge \neg A\in ℝ\right)\to A\ne 0$$
30	28 29	logcld	$$⊢\left(\phi \wedge \neg A\in ℝ\right)\to \log A\in ℂ$$
31	30	imcjd	$$⊢\left(\phi \wedge \neg A\in ℝ\right)\to \Im \left(\overline{\log A}\right)=-\Im \left(\log A\right)$$
32	27 31	eqtrd	$$⊢\left(\phi \wedge \neg A\in ℝ\right)\to \Im \left(\log \bar{A}\right)=-\Im \left(\log A\right)$$
33	18 32	pm2.61dan	$$⊢\phi \to \Im \left(\log \bar{A}\right)=-\Im \left(\log A\right)$$