Metamath Proof Explorer

Theorem reneg

Description: Real part of negative. (Contributed by NM, 17-Mar-2005) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion reneg ⊢ A ∈ ℂ → ℜ ⁡ − A = − ℜ ⁡ A

Proof

Step Hyp Ref Expression
1 recl ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℝ
2 1 recnd ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℂ
3 ax-icn ⊢ i ∈ ℂ
4 imcl ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℝ
5 4 recnd ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℂ
6 mulcl ⊢ i ∈ ℂ ∧ ℑ ⁡ A ∈ ℂ → i ⁢ ℑ ⁡ A ∈ ℂ
7 3 5 6 sylancr ⊢ A ∈ ℂ → i ⁢ ℑ ⁡ A ∈ ℂ
8 2 7 negdid ⊢ A ∈ ℂ → − ℜ ⁡ A + i ⁢ ℑ ⁡ A = - ℜ ⁡ A + − i ⁢ ℑ ⁡ A
9 replim ⊢ A ∈ ℂ → A = ℜ ⁡ A + i ⁢ ℑ ⁡ A
10 9 negeqd ⊢ A ∈ ℂ → − A = − ℜ ⁡ A + i ⁢ ℑ ⁡ A
11 mulneg2 ⊢ i ∈ ℂ ∧ ℑ ⁡ A ∈ ℂ → i ⁢ − ℑ ⁡ A = − i ⁢ ℑ ⁡ A
12 3 5 11 sylancr ⊢ A ∈ ℂ → i ⁢ − ℑ ⁡ A = − i ⁢ ℑ ⁡ A
13 12 oveq2d ⊢ A ∈ ℂ → - ℜ ⁡ A + i ⁢ − ℑ ⁡ A = - ℜ ⁡ A + − i ⁢ ℑ ⁡ A
14 8 10 13 3eqtr4d ⊢ A ∈ ℂ → − A = - ℜ ⁡ A + i ⁢ − ℑ ⁡ A
15 14 fveq2d ⊢ A ∈ ℂ → ℜ ⁡ − A = ℜ ⁡ - ℜ ⁡ A + i ⁢ − ℑ ⁡ A
16 1 renegcld ⊢ A ∈ ℂ → − ℜ ⁡ A ∈ ℝ
17 4 renegcld ⊢ A ∈ ℂ → − ℑ ⁡ A ∈ ℝ
18 crre ⊢ − ℜ ⁡ A ∈ ℝ ∧ − ℑ ⁡ A ∈ ℝ → ℜ ⁡ - ℜ ⁡ A + i ⁢ − ℑ ⁡ A = − ℜ ⁡ A
19 16 17 18 syl2anc ⊢ A ∈ ℂ → ℜ ⁡ - ℜ ⁡ A + i ⁢ − ℑ ⁡ A = − ℜ ⁡ A
20 15 19 eqtrd ⊢ A ∈ ℂ → ℜ ⁡ − A = − ℜ ⁡ A