Metamath Proof Explorer


Theorem cnegex

Description: Existence of the negative of a complex number. (Contributed by Eric Schmidt, 21-May-2007) (Revised by Scott Fenton, 3-Jan-2013) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion cnegex A x A + x = 0

Proof

Step Hyp Ref Expression
1 cnre A a b A = a + i b
2 ax-rnegex a c a + c = 0
3 ax-rnegex b d b + d = 0
4 2 3 anim12i a b c a + c = 0 d b + d = 0
5 reeanv c d a + c = 0 b + d = 0 c a + c = 0 d b + d = 0
6 4 5 sylibr a b c d a + c = 0 b + d = 0
7 ax-icn i
8 7 a1i a b c d a + c = 0 b + d = 0 i
9 simplrr a b c d a + c = 0 b + d = 0 d
10 9 recnd a b c d a + c = 0 b + d = 0 d
11 8 10 mulcld a b c d a + c = 0 b + d = 0 i d
12 simplrl a b c d a + c = 0 b + d = 0 c
13 12 recnd a b c d a + c = 0 b + d = 0 c
14 11 13 addcld a b c d a + c = 0 b + d = 0 i d + c
15 simplll a b c d a + c = 0 b + d = 0 a
16 15 recnd a b c d a + c = 0 b + d = 0 a
17 simpllr a b c d a + c = 0 b + d = 0 b
18 17 recnd a b c d a + c = 0 b + d = 0 b
19 8 18 mulcld a b c d a + c = 0 b + d = 0 i b
20 16 19 11 addassd a b c d a + c = 0 b + d = 0 a + i b + i d = a + i b + i d
21 8 18 10 adddid a b c d a + c = 0 b + d = 0 i b + d = i b + i d
22 simprr a b c d a + c = 0 b + d = 0 b + d = 0
23 22 oveq2d a b c d a + c = 0 b + d = 0 i b + d = i 0
24 mul01 i i 0 = 0
25 7 24 ax-mp i 0 = 0
26 23 25 eqtrdi a b c d a + c = 0 b + d = 0 i b + d = 0
27 21 26 eqtr3d a b c d a + c = 0 b + d = 0 i b + i d = 0
28 27 oveq2d a b c d a + c = 0 b + d = 0 a + i b + i d = a + 0
29 addid1 a a + 0 = a
30 16 29 syl a b c d a + c = 0 b + d = 0 a + 0 = a
31 20 28 30 3eqtrd a b c d a + c = 0 b + d = 0 a + i b + i d = a
32 31 oveq1d a b c d a + c = 0 b + d = 0 a + i b + i d + c = a + c
33 16 19 addcld a b c d a + c = 0 b + d = 0 a + i b
34 33 11 13 addassd a b c d a + c = 0 b + d = 0 a + i b + i d + c = a + i b + i d + c
35 32 34 eqtr3d a b c d a + c = 0 b + d = 0 a + c = a + i b + i d + c
36 simprl a b c d a + c = 0 b + d = 0 a + c = 0
37 35 36 eqtr3d a b c d a + c = 0 b + d = 0 a + i b + i d + c = 0
38 oveq2 x = i d + c a + i b + x = a + i b + i d + c
39 38 eqeq1d x = i d + c a + i b + x = 0 a + i b + i d + c = 0
40 39 rspcev i d + c a + i b + i d + c = 0 x a + i b + x = 0
41 14 37 40 syl2anc a b c d a + c = 0 b + d = 0 x a + i b + x = 0
42 41 ex a b c d a + c = 0 b + d = 0 x a + i b + x = 0
43 42 rexlimdvva a b c d a + c = 0 b + d = 0 x a + i b + x = 0
44 6 43 mpd a b x a + i b + x = 0
45 oveq1 A = a + i b A + x = a + i b + x
46 45 eqeq1d A = a + i b A + x = 0 a + i b + x = 0
47 46 rexbidv A = a + i b x A + x = 0 x a + i b + x = 0
48 44 47 syl5ibrcom a b A = a + i b x A + x = 0
49 48 rexlimivv a b A = a + i b x A + x = 0
50 1 49 syl A x A + x = 0