df-plus - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Definition df-plus 5225

Description: Define addition over complex numbers.

**Assertion**
Ref	Expression
df-plus	$/\$ $/\$ $/\$ $/\$

**Detailed syntax breakdown of Definition df-plus**
Step	Hyp	Ref	Expression
1		caddc 5217	. 2
2		vx	. . . . . . 7
3	2	cv 953	. . . . . 6
4		cc 5212	. . . . . 6
5	3, 4	wcel 956	. . . . 5
6		vy	. . . . . . 7
7	6	cv 953	. . . . . 6
8	7, 4	wcel 956	. . . . 5
9	5, 8	wa 223	. . . 4 $/\$
10		vw	. . . . . . . . . . . . 13
11	10	cv 953	. . . . . . . . . . . 12
12		vv	. . . . . . . . . . . . 13
13	12	cv 953	. . . . . . . . . . . 12
14	11, 13	cop 2407	. . . . . . . . . . 11
15	3, 14	wceq 954	. . . . . . . . . 10
16		vu	. . . . . . . . . . . . 13
17	16	cv 953	. . . . . . . . . . . 12
18		vf	. . . . . . . . . . . . 13
19	18	cv 953	. . . . . . . . . . . 12
20	17, 19	cop 2407	. . . . . . . . . . 11
21	7, 20	wceq 954	. . . . . . . . . 10
22	15, 21	wa 223	. . . . . . . . 9 $/\$
23		vz	. . . . . . . . . . 11
24	23	cv 953	. . . . . . . . . 10
25		cplr 4977	. . . . . . . . . . . 12
26	11, 17, 25	co 3954	. . . . . . . . . . 11
27	13, 19, 25	co 3954	. . . . . . . . . . 11
28	26, 27	cop 2407	. . . . . . . . . 10
29	24, 28	wceq 954	. . . . . . . . 9
30	22, 29	wa 223	. . . . . . . 8 $/\$ $/\$
31	30, 18	wex 978	. . . . . . 7 $/\$ $/\$
32	31, 16	wex 978	. . . . . 6 $/\$ $/\$
33	32, 12	wex 978	. . . . 5 $/\$ $/\$
34	33, 10	wex 978	. . . 4 $/\$ $/\$
35	9, 34	wa 223	. . 3 $/\$ $/\$ $/\$ $/\$
36	35, 2, 6, 23	copab2 3955	. 2 $/\$ $/\$ $/\$ $/\$
37	1, 36	wceq 954	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

This definition is referenced by: addcnsr 5233 axaddopr 5245