cjmul - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem cjmul 6789

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 6765	. . . . . . . 8
3	2	recn 5314	. . . . . . 7
4		readd.2	. . . . . . . . 9
5	4	recl 6765	. . . . . . . 8
6	5	recn 5314	. . . . . . 7
7	3, 6	mulcl 5321	. . . . . 6
8	1	imcl 6766	. . . . . . . 8
9	8	recn 5314	. . . . . . 7
10	4	imcl 6766	. . . . . . . 8
11	10	recn 5314	. . . . . . 7
12	9, 11	mulcl 5321	. . . . . 6
13	7, 12	subcl 5366	. . . . 5
14		axicn 5270	. . . . . 6
15	3, 11	mulcl 5321	. . . . . . 7
16	9, 6	mulcl 5321	. . . . . . 7
17	15, 16	addcl 5320	. . . . . 6
18	14, 17	mulcl 5321	. . . . 5
19	13, 18	negsub 5381	. . . 4
20	9, 11	mul2neg 5447	. . . . . . 7
21	20	eqcomi 1479	. . . . . 6
22	21	opreq2i 3972	. . . . 5
23	14, 17	mulneg2 5446	. . . . . 6
24	15, 16	negdi 5448	. . . . . . . 8
25	3, 11	mulneg2 5446	. . . . . . . . 9
26	9, 6	mulneg1 5445	. . . . . . . . 9
27	25, 26	opreq12i 3973	. . . . . . . 8
28	24, 27	eqtr4 1498	. . . . . . 7
29	28	opreq2i 3972	. . . . . 6
30	23, 29	eqtr3 1497	. . . . 5
31	22, 30	opreq12i 3973	. . . 4
32	19, 31	eqtr3 1497	. . 3
33	1, 4	remul 6786	. . . 4
34	1, 4	immul 6787	. . . . 5
35	34	opreq2i 3972	. . . 4
36	33, 35	opreq12i 3973	. . 3
37	9	negcl 5369	. . . 4
38	11	negcl 5369	. . . 4
39	3, 37, 6, 38	crmul 6740	. . 3
40	32, 36, 39	3eqtr4 1505	. 2
41	1, 4	mulcl 5321	. . 3
42		cjvalt 6763	. . 3
43	41, 42	ax-mp 7	. 2
44	14, 9	mulcl 5321	. . . . 5
45	3, 44	negsub 5381	. . . 4
46	14, 9	mulneg2 5446	. . . . 5
47	46	opreq2i 3972	. . . 4
48		cjvalt 6763	. . . . 5
49	1, 48	ax-mp 7	. . . 4
50	45, 47, 49	3eqtr4r 1506	. . 3
51	14, 11	mulcl 5321	. . . . 5
52	6, 51	negsub 5381	. . . 4
53	14, 11	mulneg2 5446	. . . . 5
54	53	opreq2i 3972	. . . 4