recextlem1

		Ref	Expression
	Assertion	recextlem1	$⊢ (A \in ℂ \land B \in ℂ) \to (A + i B) (A - i B) = A A + B B$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ℂ \land B \in ℂ) \to A \in ℂ$
2		ax-icn	$⊢ i \in ℂ$
3		mulcl	$⊢ (i \in ℂ \land B \in ℂ) \to i B \in ℂ$
4	2 3	mpan	$⊢ B \in ℂ \to i B \in ℂ$
5	4	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to i B \in ℂ$
6		subcl	$⊢ (A \in ℂ \land i B \in ℂ) \to A - i B \in ℂ$
7	4 6	sylan2	$⊢ (A \in ℂ \land B \in ℂ) \to A - i B \in ℂ$
8	1 5 7	adddird	$⊢ (A \in ℂ \land B \in ℂ) \to (A + i B) (A - i B) = A (A - i B) + i B (A - i B)$
9	1 1 5	subdid	$⊢ (A \in ℂ \land B \in ℂ) \to A (A - i B) = A A - A i B$
10	5 1 5	subdid	$⊢ (A \in ℂ \land B \in ℂ) \to i B (A - i B) = i B A - i B i B$
11		mulcom	$⊢ (A \in ℂ \land i B \in ℂ) \to A i B = i B A$
12	4 11	sylan2	$⊢ (A \in ℂ \land B \in ℂ) \to A i B = i B A$
13		ixi	$⊢ i i = - 1$
14	13	oveq1i	$⊢ i i B B = -1 B B$
15		mulcl	$⊢ (B \in ℂ \land B \in ℂ) \to B B \in ℂ$
16	15	mulm1d	$⊢ (B \in ℂ \land B \in ℂ) \to -1 B B = - B B$
17	14 16	syl5req	$⊢ (B \in ℂ \land B \in ℂ) \to - B B = i i B B$
18		mul4	$⊢ ((i \in ℂ \land i \in ℂ) \land (B \in ℂ \land B \in ℂ)) \to i i B B = i B i B$
19	2 2 18	mpanl12	$⊢ (B \in ℂ \land B \in ℂ) \to i i B B = i B i B$
20	17 19	eqtrd	$⊢ (B \in ℂ \land B \in ℂ) \to - B B = i B i B$
21	20	anidms	$⊢ B \in ℂ \to - B B = i B i B$
22	21	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to - B B = i B i B$
23	12 22	oveq12d	$⊢ (A \in ℂ \land B \in ℂ) \to A i B - (- B B) = i B A - i B i B$
24	10 23	eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to i B (A - i B) = A i B - (- B B)$
25	9 24	oveq12d	$⊢ (A \in ℂ \land B \in ℂ) \to A (A - i B) + i B (A - i B) = (A A - A i B) + A i B - (- B B)$
26		mulcl	$⊢ (A \in ℂ \land A \in ℂ) \to A A \in ℂ$
27	26	anidms	$⊢ A \in ℂ \to A A \in ℂ$
28	27	adantr	$⊢ (A \in ℂ \land B \in ℂ) \to A A \in ℂ$
29		mulcl	$⊢ (A \in ℂ \land i B \in ℂ) \to A i B \in ℂ$
30	4 29	sylan2	$⊢ (A \in ℂ \land B \in ℂ) \to A i B \in ℂ$
31	15	negcld	$⊢ (B \in ℂ \land B \in ℂ) \to - B B \in ℂ$
32	31	anidms	$⊢ B \in ℂ \to - B B \in ℂ$
33	32	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to - B B \in ℂ$
34	28 30 33	npncand	$⊢ (A \in ℂ \land B \in ℂ) \to (A A - A i B) + A i B - (- B B) = A A - (- B B)$
35	15	anidms	$⊢ B \in ℂ \to B B \in ℂ$
36		subneg	$⊢ (A A \in ℂ \land B B \in ℂ) \to A A - (- B B) = A A + B B$
37	27 35 36	syl2an	$⊢ (A \in ℂ \land B \in ℂ) \to A A - (- B B) = A A + B B$
38	34 37	eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to (A A - A i B) + A i B - (- B B) = A A + B B$
39	8 25 38	3eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to (A + i B) (A - i B) = A A + B B$

Metamath Proof Explorer

Theorem recextlem1

Proof