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 \in ℝ \land B \in ℝ) \to ℑ (A + i B) = B$

Proof

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

Metamath Proof Explorer

Theorem crim

Proof