This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐴 ) ) )