This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-add

Description: Define addition over complex numbers. (Contributed by NM, 28-May-1995) (New usage is discouraged.)

Ref Expression
Assertion df-add ⊢ + = x y z | x ∈ ℂ ∧ y ∈ ℂ ∧ ∃ w ∃ v ∃ u ∃ f x = w v ∧ y = u f ∧ z = w + 𝑹 u v + 𝑹 f

Detailed syntax breakdown

Step Hyp Ref Expression
0 caddc class +
1 vx setvar x
2 vy setvar y
3 vz setvar z
4 1 cv setvar x
5 cc class ℂ
6 4 5 wcel wff x ∈ ℂ
7 2 cv setvar y
8 7 5 wcel wff y ∈ ℂ
9 6 8 wa wff x ∈ ℂ ∧ y ∈ ℂ
10 vw setvar w
11 vv setvar v
12 vu setvar u
13 vf setvar f
14 10 cv setvar w
15 11 cv setvar v
16 14 15 cop class w v
17 4 16 wceq wff x = w v
18 12 cv setvar u
19 13 cv setvar f
20 18 19 cop class u f
21 7 20 wceq wff y = u f
22 17 21 wa wff x = w v ∧ y = u f
23 3 cv setvar z
24 cplr class + 𝑹
25 14 18 24 co class w + 𝑹 u
26 15 19 24 co class v + 𝑹 f
27 25 26 cop class w + 𝑹 u v + 𝑹 f
28 23 27 wceq wff z = w + 𝑹 u v + 𝑹 f
29 22 28 wa wff x = w v ∧ y = u f ∧ z = w + 𝑹 u v + 𝑹 f
30 29 13 wex wff ∃ f x = w v ∧ y = u f ∧ z = w + 𝑹 u v + 𝑹 f
31 30 12 wex wff ∃ u ∃ f x = w v ∧ y = u f ∧ z = w + 𝑹 u v + 𝑹 f
32 31 11 wex wff ∃ v ∃ u ∃ f x = w v ∧ y = u f ∧ z = w + 𝑹 u v + 𝑹 f
33 32 10 wex wff ∃ w ∃ v ∃ u ∃ f x = w v ∧ y = u f ∧ z = w + 𝑹 u v + 𝑹 f
34 9 33 wa wff x ∈ ℂ ∧ y ∈ ℂ ∧ ∃ w ∃ v ∃ u ∃ f x = w v ∧ y = u f ∧ z = w + 𝑹 u v + 𝑹 f
35 34 1 2 3 coprab class x y z | x ∈ ℂ ∧ y ∈ ℂ ∧ ∃ w ∃ v ∃ u ∃ f x = w v ∧ y = u f ∧ z = w + 𝑹 u v + 𝑹 f
36 0 35 wceq wff + = x y z | x ∈ ℂ ∧ y ∈ ℂ ∧ ∃ w ∃ v ∃ u ∃ f x = w v ∧ y = u f ∧ z = w + 𝑹 u v + 𝑹 f