Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem cjmul 6732

Description: Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133.

Hypotheses

Ref	Expression
cjcj.1
readd.2

Assertion

Ref	Expression
cjmul

---

Proof of Theorem cjmul

Step	Hyp	Ref	Expression
1		cjcj.1	. . . . . . . . 9
2	1	recl 6705	. . . . . . . 8
3	2	recn 5294	. . . . . . 7
4		readd.2	. . . . . . . . 9
5	4	recl 6705	. . . . . . . 8
6	5	recn 5294	. . . . . . 7
7	3, 6	mulcl 5301	. . . . . 6
8	1	imcl 6706	. . . . . . . 8
9	8	recn 5294	. . . . . . 7
10	4	imcl 6706	. . . . . . . 8
11	10	recn 5294	. . . . . . 7
12	9, 11	mulcl 5301	. . . . . 6
13	7, 12	subcl 5346	. . . . 5
14		axicn 5250	. . . . . 6
15	3, 11	mulcl 5301	. . . . . . 7
16	9, 6	mulcl 5301	. . . . . . 7
17	15, 16	addcl 5300	. . . . . 6
18	14, 17	mulcl 5301	. . . . 5
19	13, 18	negsub 5361	. . . 4
20	9, 11	mul2neg 5427	. . . . . . 7
21	20	eqcomi 1476	. . . . . 6
22	21	opreq2i 3963	. . . . 5
23	14, 17	mulneg2 5426	. . . . . 6
24	15, 16	negdi 5428	. . . . . . . 8
25	3, 11	mulneg2 5426	. . . . . . . . 9
26	9, 6	mulneg1 5425	. . . . . . . . 9
27	25, 26	opreq12i 3964	. . . . . . . 8
28	24, 27	eqtr4 1495	. . . . . . 7
29	28	opreq2i 3963	. . . . . 6
30	23, 29	eqtr3 1494	. . . . 5
31	22, 30	opreq12i 3964	. . . 4
32	19, 31	eqtr3 1494	. . 3
33	1, 4	remul 6729	. . . 4
34	1, 4	immul 6730	. . . . 5
35	34	opreq2i 3963	. . . 4
36	33, 35	opreq12i 3964	. . 3
37	9	negcl 5349	. . . 4
38	11	negcl 5349	. . . 4
39	3, 37, 6, 38	crmul 6679	. . 3
40	32, 36, 39	3eqtr4 1502	. 2
41	1, 4	mulcl 5301	. . 3
42		cjvalt 6703	. . 3
43	41, 42	ax-mp 7	. 2
44	14, 9	mulcl 5301	. . . . 5
45	3, 44	negsub 5361	. . . 4
46	14, 9	mulneg2 5426	. . . . 5
47	46	opreq2i 3963	. . . 4
48		cjvalt 6703	. . . . 5
49	1, 48	ax-mp 7	. . . 4
50	45, 47, 49	3eqtr4r 1503	. . 3
51	14, 11	mulcl 5301	. . . . 5
52	6, 51	negsub 5361	. . . 4
53	14, 11	mulneg2 5426	. . . . 5
54	53	opreq2i 3963	. . . 4