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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	efiargd.2	⊢ ( 𝜑 → 𝐴 ≠ 0 )
	arginv.1	⊢ ( 𝜑 → ¬ - 𝐴 ∈ ℝ+ )
Assertion	arginv	⊢ ( 𝜑 → ( ℑ ‘ ( log ‘ ( 1 / 𝐴 ) ) ) = - ( ℑ ‘ ( log ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		efiargd.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		efiargd.2	⊢ ( 𝜑 → 𝐴 ≠ 0 )
3		arginv.1	⊢ ( 𝜑 → ¬ - 𝐴 ∈ ℝ+ )
4	1 2	logcld	⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℂ )
5	1 2	reccld	⊢ ( 𝜑 → ( 1 / 𝐴 ) ∈ ℂ )
6	1 2	recne0d	⊢ ( 𝜑 → ( 1 / 𝐴 ) ≠ 0 )
7	5 6	logcld	⊢ ( 𝜑 → ( log ‘ ( 1 / 𝐴 ) ) ∈ ℂ )
8		lognegb	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - 𝐴 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝐴 ) ) = π ) )
9	8	necon3bbid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ¬ - 𝐴 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π ) )
10	9	biimpa	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ¬ - 𝐴 ∈ ℝ+ ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π )
11	1 2 3 10	syl21anc	⊢ ( 𝜑 → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π )
12		logrec	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≠ π ) → ( log ‘ 𝐴 ) = - ( log ‘ ( 1 / 𝐴 ) ) )
13	1 2 11 12	syl3anc	⊢ ( 𝜑 → ( log ‘ 𝐴 ) = - ( log ‘ ( 1 / 𝐴 ) ) )
14		negcon2	⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( log ‘ ( 1 / 𝐴 ) ) ∈ ℂ ) → ( ( log ‘ 𝐴 ) = - ( log ‘ ( 1 / 𝐴 ) ) ↔ ( log ‘ ( 1 / 𝐴 ) ) = - ( log ‘ 𝐴 ) ) )
15	14	biimpa	⊢ ( ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( log ‘ ( 1 / 𝐴 ) ) ∈ ℂ ) ∧ ( log ‘ 𝐴 ) = - ( log ‘ ( 1 / 𝐴 ) ) ) → ( log ‘ ( 1 / 𝐴 ) ) = - ( log ‘ 𝐴 ) )
16	4 7 13 15	syl21anc	⊢ ( 𝜑 → ( log ‘ ( 1 / 𝐴 ) ) = - ( log ‘ 𝐴 ) )
17	16	fveq2d	⊢ ( 𝜑 → ( ℑ ‘ ( log ‘ ( 1 / 𝐴 ) ) ) = ( ℑ ‘ - ( log ‘ 𝐴 ) ) )
18	4	imnegd	⊢ ( 𝜑 → ( ℑ ‘ - ( log ‘ 𝐴 ) ) = - ( ℑ ‘ ( log ‘ 𝐴 ) ) )
19	17 18	eqtrd	⊢ ( 𝜑 → ( ℑ ‘ ( log ‘ ( 1 / 𝐴 ) ) ) = - ( ℑ ‘ ( log ‘ 𝐴 ) ) )