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