Theorem arginv

Description: The argument of the inverse 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	arginv	$$⊢\phi \to \Im \left(\log \left(\frac{1}{A}\right)\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	1 2	logcld	$$⊢\phi \to \log A\in ℂ$$
5	1 2	reccld	$$⊢\phi \to \frac{1}{A}\in ℂ$$
6	1 2	recne0d	$$⊢\phi \to \frac{1}{A}\ne 0$$
7	5 6	logcld	$$⊢\phi \to \log \left(\frac{1}{A}\right)\in ℂ$$
8		lognegb	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(-A\in {ℝ}^{+}\leftrightarrow \Im \left(\log A\right)=\mathrm{\pi }\right)$$
9	8	necon3bbid	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(\neg -A\in {ℝ}^{+}\leftrightarrow \Im \left(\log A\right)\ne \mathrm{\pi }\right)$$
10	9	biimpa	$$⊢\left(\left(A\in ℂ\wedge A\ne 0\right)\wedge \neg -A\in {ℝ}^{+}\right)\to \Im \left(\log A\right)\ne \mathrm{\pi }$$
11	1 2 3 10	syl21anc	$$⊢\phi \to \Im \left(\log A\right)\ne \mathrm{\pi }$$
12		logrec	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge \Im \left(\log A\right)\ne \mathrm{\pi }\right)\to \log A=-\log \left(\frac{1}{A}\right)$$
13	1 2 11 12	syl3anc	$$⊢\phi \to \log A=-\log \left(\frac{1}{A}\right)$$
14		negcon2	$$⊢\left(\log A\in ℂ\wedge \log \left(\frac{1}{A}\right)\in ℂ\right)\to \left(\log A=-\log \left(\frac{1}{A}\right)\leftrightarrow \log \left(\frac{1}{A}\right)=-\log A\right)$$
15	14	biimpa	$$⊢\left(\left(\log A\in ℂ\wedge \log \left(\frac{1}{A}\right)\in ℂ\right)\wedge \log A=-\log \left(\frac{1}{A}\right)\right)\to \log \left(\frac{1}{A}\right)=-\log A$$
16	4 7 13 15	syl21anc	$$⊢\phi \to \log \left(\frac{1}{A}\right)=-\log A$$
17	16	fveq2d	$$⊢\phi \to \Im \left(\log \left(\frac{1}{A}\right)\right)=\Im \left(-\log A\right)$$
18	4	imnegd	$$⊢\phi \to \Im \left(-\log A\right)=-\Im \left(\log A\right)$$
19	17 18	eqtrd	$$⊢\phi \to \Im \left(\log \left(\frac{1}{A}\right)\right)=-\Im \left(\log A\right)$$