Theorem sn-negex12

Description: A combination of cnegex and cnegex2 , this proof takes cnre A = r +i x. s and shows that i x. -u s + -u r is both a left and right inverse. (Contributed by SN, 5-May-2024)

	Ref	Expression
Assertion	sn-negex12	⊢ ( 𝐴 ∈ ℂ → ∃ 𝑏 ∈ ℂ ( ( 𝐴 + 𝑏 ) = 0 ∧ ( 𝑏 + 𝐴 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-icn	⊢ i ∈ ℂ
2	1	a1i	⊢ ( 𝑦 ∈ ℝ → i ∈ ℂ )
3		rernegcl	⊢ ( 𝑦 ∈ ℝ → ( 0 −ℝ 𝑦 ) ∈ ℝ )
4	3	recnd	⊢ ( 𝑦 ∈ ℝ → ( 0 −ℝ 𝑦 ) ∈ ℂ )
5	2 4	mulcld	⊢ ( 𝑦 ∈ ℝ → ( i · ( 0 −ℝ 𝑦 ) ) ∈ ℂ )
6	5	adantl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( i · ( 0 −ℝ 𝑦 ) ) ∈ ℂ )
7		rernegcl	⊢ ( 𝑥 ∈ ℝ → ( 0 −ℝ 𝑥 ) ∈ ℝ )
8	7	recnd	⊢ ( 𝑥 ∈ ℝ → ( 0 −ℝ 𝑥 ) ∈ ℂ )
9	8	adantr	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 −ℝ 𝑥 ) ∈ ℂ )
10	6 9	addcld	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ∈ ℂ )
11	10	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ∈ ℂ )
12		eqeq1	⊢ ( 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) → ( 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ↔ ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ) )
13	12	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ) → ( 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ↔ ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ) )
14		eqidd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) )
15	11 13 14	rspcedvd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ∃ 𝑏 ∈ ℂ 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) )
16	15	ralrimivva	⊢ ( 𝐴 ∈ ℂ → ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ∃ 𝑏 ∈ ℂ 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) )
17		cnre	⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )
18	16 17	r19.29d2r	⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ( ∃ 𝑏 ∈ ℂ 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) )
19		oveq1	⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 𝐴 + ( i · ( 0 −ℝ 𝑦 ) ) ) = ( ( 𝑥 + ( i · 𝑦 ) ) + ( i · ( 0 −ℝ 𝑦 ) ) ) )
20	19	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( 𝐴 + ( i · ( 0 −ℝ 𝑦 ) ) ) = ( ( 𝑥 + ( i · 𝑦 ) ) + ( i · ( 0 −ℝ 𝑦 ) ) ) )
21		recn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
22	21	adantr	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑥 ∈ ℂ )
23	1	a1i	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → i ∈ ℂ )
24		recn	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
25	24	adantl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
26	23 25	mulcld	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( i · 𝑦 ) ∈ ℂ )
27	22 26 6	addassd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + ( i · 𝑦 ) ) + ( i · ( 0 −ℝ 𝑦 ) ) ) = ( 𝑥 + ( ( i · 𝑦 ) + ( i · ( 0 −ℝ 𝑦 ) ) ) ) )
28		renegid	⊢ ( 𝑦 ∈ ℝ → ( 𝑦 + ( 0 −ℝ 𝑦 ) ) = 0 )
29	28	oveq2d	⊢ ( 𝑦 ∈ ℝ → ( i · ( 𝑦 + ( 0 −ℝ 𝑦 ) ) ) = ( i · 0 ) )
30	2 24 4	adddid	⊢ ( 𝑦 ∈ ℝ → ( i · ( 𝑦 + ( 0 −ℝ 𝑦 ) ) ) = ( ( i · 𝑦 ) + ( i · ( 0 −ℝ 𝑦 ) ) ) )
31		sn-it0e0	⊢ ( i · 0 ) = 0
32	31	a1i	⊢ ( 𝑦 ∈ ℝ → ( i · 0 ) = 0 )
33	29 30 32	3eqtr3d	⊢ ( 𝑦 ∈ ℝ → ( ( i · 𝑦 ) + ( i · ( 0 −ℝ 𝑦 ) ) ) = 0 )
34	33	oveq2d	⊢ ( 𝑦 ∈ ℝ → ( 𝑥 + ( ( i · 𝑦 ) + ( i · ( 0 −ℝ 𝑦 ) ) ) ) = ( 𝑥 + 0 ) )
35	34	adantl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + ( ( i · 𝑦 ) + ( i · ( 0 −ℝ 𝑦 ) ) ) ) = ( 𝑥 + 0 ) )
36		readdid1	⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + 0 ) = 𝑥 )
37	36	adantr	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 0 ) = 𝑥 )
38	27 35 37	3eqtrd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + ( i · 𝑦 ) ) + ( i · ( 0 −ℝ 𝑦 ) ) ) = 𝑥 )
39	38	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( ( 𝑥 + ( i · 𝑦 ) ) + ( i · ( 0 −ℝ 𝑦 ) ) ) = 𝑥 )
40	20 39	eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( 𝐴 + ( i · ( 0 −ℝ 𝑦 ) ) ) = 𝑥 )
41	40	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( ( 𝐴 + ( i · ( 0 −ℝ 𝑦 ) ) ) + ( 0 −ℝ 𝑥 ) ) = ( 𝑥 + ( 0 −ℝ 𝑥 ) ) )
42		simpll	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → 𝐴 ∈ ℂ )
43	6	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( i · ( 0 −ℝ 𝑦 ) ) ∈ ℂ )
44	9	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( 0 −ℝ 𝑥 ) ∈ ℂ )
45	42 43 44	addassd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( ( 𝐴 + ( i · ( 0 −ℝ 𝑦 ) ) ) + ( 0 −ℝ 𝑥 ) ) = ( 𝐴 + ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ) )
46		renegid	⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + ( 0 −ℝ 𝑥 ) ) = 0 )
47	46	adantr	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + ( 0 −ℝ 𝑥 ) ) = 0 )
48	47	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( 𝑥 + ( 0 −ℝ 𝑥 ) ) = 0 )
49	41 45 48	3eqtr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( 𝐴 + ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ) = 0 )
50		oveq2	⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) + 𝐴 ) = ( ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) + ( 𝑥 + ( i · 𝑦 ) ) ) )
51	22 26	addcld	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + ( i · 𝑦 ) ) ∈ ℂ )
52	6 9 51	addassd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) + ( 𝑥 + ( i · 𝑦 ) ) ) = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( ( 0 −ℝ 𝑥 ) + ( 𝑥 + ( i · 𝑦 ) ) ) ) )
53	9 22 26	addassd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 0 −ℝ 𝑥 ) + 𝑥 ) + ( i · 𝑦 ) ) = ( ( 0 −ℝ 𝑥 ) + ( 𝑥 + ( i · 𝑦 ) ) ) )
54	53	oveq2d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( i · ( 0 −ℝ 𝑦 ) ) + ( ( ( 0 −ℝ 𝑥 ) + 𝑥 ) + ( i · 𝑦 ) ) ) = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( ( 0 −ℝ 𝑥 ) + ( 𝑥 + ( i · 𝑦 ) ) ) ) )
55		renegid2	⊢ ( 𝑥 ∈ ℝ → ( ( 0 −ℝ 𝑥 ) + 𝑥 ) = 0 )
56	55	adantr	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 0 −ℝ 𝑥 ) + 𝑥 ) = 0 )
57	56	oveq1d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 0 −ℝ 𝑥 ) + 𝑥 ) + ( i · 𝑦 ) ) = ( 0 + ( i · 𝑦 ) ) )
58		sn-addid2	⊢ ( ( i · 𝑦 ) ∈ ℂ → ( 0 + ( i · 𝑦 ) ) = ( i · 𝑦 ) )
59	26 58	syl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 + ( i · 𝑦 ) ) = ( i · 𝑦 ) )
60	57 59	eqtrd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 0 −ℝ 𝑥 ) + 𝑥 ) + ( i · 𝑦 ) ) = ( i · 𝑦 ) )
61	60	oveq2d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( i · ( 0 −ℝ 𝑦 ) ) + ( ( ( 0 −ℝ 𝑥 ) + 𝑥 ) + ( i · 𝑦 ) ) ) = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( i · 𝑦 ) ) )
62	4	adantl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 −ℝ 𝑦 ) ∈ ℂ )
63	23 62 25	adddid	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( i · ( ( 0 −ℝ 𝑦 ) + 𝑦 ) ) = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( i · 𝑦 ) ) )
64		renegid2	⊢ ( 𝑦 ∈ ℝ → ( ( 0 −ℝ 𝑦 ) + 𝑦 ) = 0 )
65	64	adantl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 0 −ℝ 𝑦 ) + 𝑦 ) = 0 )
66	65	oveq2d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( i · ( ( 0 −ℝ 𝑦 ) + 𝑦 ) ) = ( i · 0 ) )
67	66 31	eqtrdi	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( i · ( ( 0 −ℝ 𝑦 ) + 𝑦 ) ) = 0 )
68	61 63 67	3eqtr2d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( i · ( 0 −ℝ 𝑦 ) ) + ( ( ( 0 −ℝ 𝑥 ) + 𝑥 ) + ( i · 𝑦 ) ) ) = 0 )
69	52 54 68	3eqtr2d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) + ( 𝑥 + ( i · 𝑦 ) ) ) = 0 )
70	69	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) + ( 𝑥 + ( i · 𝑦 ) ) ) = 0 )
71	50 70	sylan9eqr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) + 𝐴 ) = 0 )
72	49 71	jca	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( ( 𝐴 + ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ) = 0 ∧ ( ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) + 𝐴 ) = 0 ) )
73		oveq2	⊢ ( 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) → ( 𝐴 + 𝑏 ) = ( 𝐴 + ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ) )
74	73	eqeq1d	⊢ ( 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) → ( ( 𝐴 + 𝑏 ) = 0 ↔ ( 𝐴 + ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ) = 0 ) )
75		oveq1	⊢ ( 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) → ( 𝑏 + 𝐴 ) = ( ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) + 𝐴 ) )
76	75	eqeq1d	⊢ ( 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) → ( ( 𝑏 + 𝐴 ) = 0 ↔ ( ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) + 𝐴 ) = 0 ) )
77	74 76	anbi12d	⊢ ( 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) → ( ( ( 𝐴 + 𝑏 ) = 0 ∧ ( 𝑏 + 𝐴 ) = 0 ) ↔ ( ( 𝐴 + ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ) = 0 ∧ ( ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) + 𝐴 ) = 0 ) ) )
78	72 77	syl5ibrcom	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) → ( ( 𝐴 + 𝑏 ) = 0 ∧ ( 𝑏 + 𝐴 ) = 0 ) ) )
79	78	reximdv	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( ∃ 𝑏 ∈ ℂ 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) → ∃ 𝑏 ∈ ℂ ( ( 𝐴 + 𝑏 ) = 0 ∧ ( 𝑏 + 𝐴 ) = 0 ) ) )
80	79	expimpd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ∧ ∃ 𝑏 ∈ ℂ 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ) → ∃ 𝑏 ∈ ℂ ( ( 𝐴 + 𝑏 ) = 0 ∧ ( 𝑏 + 𝐴 ) = 0 ) ) )
81	80	ancomsd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( ( ∃ 𝑏 ∈ ℂ 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ∃ 𝑏 ∈ ℂ ( ( 𝐴 + 𝑏 ) = 0 ∧ ( 𝑏 + 𝐴 ) = 0 ) ) )
82	81	rexlimdvva	⊢ ( 𝐴 ∈ ℂ → ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ( ∃ 𝑏 ∈ ℂ 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ∃ 𝑏 ∈ ℂ ( ( 𝐴 + 𝑏 ) = 0 ∧ ( 𝑏 + 𝐴 ) = 0 ) ) )
83	18 82	mpd	⊢ ( 𝐴 ∈ ℂ → ∃ 𝑏 ∈ ℂ ( ( 𝐴 + 𝑏 ) = 0 ∧ ( 𝑏 + 𝐴 ) = 0 ) )