Metamath Proof Explorer

Theorem crim

Description: The real part of a complex number representation. Definition 10-3.1 of Gleason p. 132. (Contributed by NM, 12-May-2005) (Revised by Mario Carneiro, 7-Nov-2013)

Ref Expression
Assertion crim ⊢A∈ℝ∧B∈ℝ→ℑ⁡A+i⁢B=B

Proof

Step Hyp Ref Expression
1 recn ⊢A∈ℝ→A∈ℂ
2 ax-icn ⊢i∈ℂ
3 recn ⊢B∈ℝ→B∈ℂ
4 mulcl ⊢i∈ℂ∧B∈ℂ→i⁢B∈ℂ
5 2 3 4 sylancr ⊢B∈ℝ→i⁢B∈ℂ
6 addcl ⊢A∈ℂ∧i⁢B∈ℂ→A+i⁢B∈ℂ
7 1 5 6 syl2an ⊢A∈ℝ∧B∈ℝ→A+i⁢B∈ℂ
8 imval ⊢A+i⁢B∈ℂ→ℑ⁡A+i⁢B=ℜ⁡A+i⁢Bi
9 7 8 syl ⊢A∈ℝ∧B∈ℝ→ℑ⁡A+i⁢B=ℜ⁡A+i⁢Bi
10 2 4 mpan ⊢B∈ℂ→i⁢B∈ℂ
11 ine0 ⊢i≠0
12 divdir ⊢A∈ℂ∧i⁢B∈ℂ∧i∈ℂ∧i≠0→A+i⁢Bi=Ai+i⁢Bi
13 12 3expa ⊢A∈ℂ∧i⁢B∈ℂ∧i∈ℂ∧i≠0→A+i⁢Bi=Ai+i⁢Bi
14 2 11 13 mpanr12 ⊢A∈ℂ∧i⁢B∈ℂ→A+i⁢Bi=Ai+i⁢Bi
15 10 14 sylan2 ⊢A∈ℂ∧B∈ℂ→A+i⁢Bi=Ai+i⁢Bi
16 divrec2 ⊢A∈ℂ∧i∈ℂ∧i≠0→Ai=1i⁢A
17 2 11 16 mp3an23 ⊢A∈ℂ→Ai=1i⁢A
18 irec ⊢1i=−i
19 18 oveq1i ⊢1i⁢A=−i⁢A
20 19 a1i ⊢A∈ℂ→1i⁢A=−i⁢A
21 mulneg12 ⊢i∈ℂ∧A∈ℂ→−i⁢A=i⁢−A
22 2 21 mpan ⊢A∈ℂ→−i⁢A=i⁢−A
23 17 20 22 3eqtrd ⊢A∈ℂ→Ai=i⁢−A
24 divcan3 ⊢B∈ℂ∧i∈ℂ∧i≠0→i⁢Bi=B
25 2 11 24 mp3an23 ⊢B∈ℂ→i⁢Bi=B
26 23 25 oveqan12d ⊢A∈ℂ∧B∈ℂ→Ai+i⁢Bi=i⁢−A+B
27 negcl ⊢A∈ℂ→−A∈ℂ
28 mulcl ⊢i∈ℂ∧−A∈ℂ→i⁢−A∈ℂ
29 2 27 28 sylancr ⊢A∈ℂ→i⁢−A∈ℂ
30 addcom ⊢i⁢−A∈ℂ∧B∈ℂ→i⁢−A+B=B+i⁢−A
31 29 30 sylan ⊢A∈ℂ∧B∈ℂ→i⁢−A+B=B+i⁢−A
32 15 26 31 3eqtrrd ⊢A∈ℂ∧B∈ℂ→B+i⁢−A=A+i⁢Bi
33 1 3 32 syl2an ⊢A∈ℝ∧B∈ℝ→B+i⁢−A=A+i⁢Bi
34 33 fveq2d ⊢A∈ℝ∧B∈ℝ→ℜ⁡B+i⁢−A=ℜ⁡A+i⁢Bi
35 id ⊢B∈ℝ→B∈ℝ
36 renegcl ⊢A∈ℝ→−A∈ℝ
37 crre ⊢B∈ℝ∧−A∈ℝ→ℜ⁡B+i⁢−A=B
38 35 36 37 syl2anr ⊢A∈ℝ∧B∈ℝ→ℜ⁡B+i⁢−A=B
39 9 34 38 3eqtr2d ⊢A∈ℝ∧B∈ℝ→ℑ⁡A+i⁢B=B