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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 efiargd.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 efiargd.2 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
3 arginv.1 ⊢ ( 𝜑 → ¬ - 𝐴 ∈ ℝ+ )
4 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
5 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐴 ≠ 0 )
6 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ¬ - 𝐴 ∈ ℝ+ )
7 rpneg ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 ∈ ℝ+ ↔ ¬ - 𝐴 ∈ ℝ+ ) )
8 7 biimpar ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ ¬ - 𝐴 ∈ ℝ+ ) → 𝐴 ∈ ℝ+ )
9 4 5 6 8 syl21anc ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ+ )
10 9 relogcld ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ( log ‘ 𝐴 ) ∈ ℝ )
11 10 reim0d ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) = 0 )
12 4 cjred ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ( ∗ ‘ 𝐴 ) = 𝐴 )
13 12 fveq2d ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ( log ‘ ( ∗ ‘ 𝐴 ) ) = ( log ‘ 𝐴 ) )
14 13 fveq2d ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ( ℑ ‘ ( log ‘ ( ∗ ‘ 𝐴 ) ) ) = ( ℑ ‘ ( log ‘ 𝐴 ) ) )
15 11 negeqd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → - ( ℑ ‘ ( log ‘ 𝐴 ) ) = - 0 )
16 neg0 ⊢ - 0 = 0
17 15 16 eqtrdi ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → - ( ℑ ‘ ( log ‘ 𝐴 ) ) = 0 )
18 11 14 17 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ( ℑ ‘ ( log ‘ ( ∗ ‘ 𝐴 ) ) ) = - ( ℑ ‘ ( log ‘ 𝐴 ) ) )
19 1 adantr ⊢ ( ( 𝜑 ∧ ( ℑ ‘ 𝐴 ) = 0 ) → 𝐴 ∈ ℂ )
20 simpr ⊢ ( ( 𝜑 ∧ ( ℑ ‘ 𝐴 ) = 0 ) → ( ℑ ‘ 𝐴 ) = 0 )
21 19 20 reim0bd ⊢ ( ( 𝜑 ∧ ( ℑ ‘ 𝐴 ) = 0 ) → 𝐴 ∈ ℝ )
22 21 ex ⊢ ( 𝜑 → ( ( ℑ ‘ 𝐴 ) = 0 → 𝐴 ∈ ℝ ) )
23 22 necon3bd ⊢ ( 𝜑 → ( ¬ 𝐴 ∈ ℝ → ( ℑ ‘ 𝐴 ) ≠ 0 ) )
24 23 imp ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) → ( ℑ ‘ 𝐴 ) ≠ 0 )
25 logcj ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( ∗ ‘ 𝐴 ) ) = ( ∗ ‘ ( log ‘ 𝐴 ) ) )
26 1 24 25 syl2an2r ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) → ( log ‘ ( ∗ ‘ 𝐴 ) ) = ( ∗ ‘ ( log ‘ 𝐴 ) ) )
27 26 fveq2d ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) → ( ℑ ‘ ( log ‘ ( ∗ ‘ 𝐴 ) ) ) = ( ℑ ‘ ( ∗ ‘ ( log ‘ 𝐴 ) ) ) )
28 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℂ )
29 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) → 𝐴 ≠ 0 )
30 28 29 logcld ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) → ( log ‘ 𝐴 ) ∈ ℂ )
31 30 imcjd ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) → ( ℑ ‘ ( ∗ ‘ ( log ‘ 𝐴 ) ) ) = - ( ℑ ‘ ( log ‘ 𝐴 ) ) )
32 27 31 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) → ( ℑ ‘ ( log ‘ ( ∗ ‘ 𝐴 ) ) ) = - ( ℑ ‘ ( log ‘ 𝐴 ) ) )
33 18 32 pm2.61dan ⊢ ( 𝜑 → ( ℑ ‘ ( log ‘ ( ∗ ‘ 𝐴 ) ) ) = - ( ℑ ‘ ( log ‘ 𝐴 ) ) )