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) (Proof shortened by SN, 4-Jul-2025)

	Ref	Expression
Assertion	sn-negex12	$$⊢A\in ℂ\to \exists b\in ℂ\left(A+b=0\wedge b+A=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnre	$$⊢A\in ℂ\to \exists x\in ℝ\exists y\in ℝA=x+\mathrm{i}y$$
2		oveq2	$$⊢b=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\to x+\mathrm{i}y+b=x+\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)$$
3	2	eqeq1d	$$⊢b=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\to \left(x+\mathrm{i}y+b=0\leftrightarrow x+\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)=0\right)$$
4		oveq1	$$⊢b=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\to b+x+\mathrm{i}y=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+x+\mathrm{i}y$$
5	4	eqeq1d	$$⊢b=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\to \left(b+x+\mathrm{i}y=0\leftrightarrow \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+x+\mathrm{i}y=0\right)$$
6	3 5	anbi12d	$$⊢b=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\to \left(\left(x+\mathrm{i}y+b=0\wedge b+x+\mathrm{i}y=0\right)\leftrightarrow \left(x+\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)=0\wedge \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+x+\mathrm{i}y=0\right)\right)$$
7		ax-icn	$$⊢\mathrm{i}\in ℂ$$
8	7	a1i	$$⊢y\in ℝ\to \mathrm{i}\in ℂ$$
9		rernegcl	$$⊢y\in ℝ\to 0{-}_{ℝ}y\in ℝ$$
10	9	recnd	$$⊢y\in ℝ\to 0{-}_{ℝ}y\in ℂ$$
11	8 10	mulcld	$$⊢y\in ℝ\to \mathrm{i}\left(0{-}_{ℝ}y\right)\in ℂ$$
12	11	adantl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\left(0{-}_{ℝ}y\right)\in ℂ$$
13		rernegcl	$$⊢x\in ℝ\to 0{-}_{ℝ}x\in ℝ$$
14	13	recnd	$$⊢x\in ℝ\to 0{-}_{ℝ}x\in ℂ$$
15	14	adantr	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 0{-}_{ℝ}x\in ℂ$$
16	12 15	addcld	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\in ℂ$$
17		recn	$$⊢x\in ℝ\to x\in ℂ$$
18	17	adantr	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x\in ℂ$$
19		recn	$$⊢y\in ℝ\to y\in ℂ$$
20	8 19	mulcld	$$⊢y\in ℝ\to \mathrm{i}y\in ℂ$$
21	20	adantl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}y\in ℂ$$
22	18 21 12	addassd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x+\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)=x+\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)$$
23	8 19 10	adddid	$$⊢y\in ℝ\to \mathrm{i}\left(y+\left(0{-}_{ℝ}y\right)\right)=\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)$$
24		renegid	$$⊢y\in ℝ\to y+\left(0{-}_{ℝ}y\right)=0$$
25	24	oveq2d	$$⊢y\in ℝ\to \mathrm{i}\left(y+\left(0{-}_{ℝ}y\right)\right)=\mathrm{i}\cdot 0$$
26		sn-it0e0	$$⊢\mathrm{i}\cdot 0=0$$
27	25 26	eqtrdi	$$⊢y\in ℝ\to \mathrm{i}\left(y+\left(0{-}_{ℝ}y\right)\right)=0$$
28	23 27	eqtr3d	$$⊢y\in ℝ\to \mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)=0$$
29	28	adantl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)=0$$
30	29	oveq2d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x+\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)=x+0$$
31		readdrid	$$⊢x\in ℝ\to x+0=x$$
32	31	adantr	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x+0=x$$
33	22 30 32	3eqtrd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x+\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)=x$$
34	33	oveq1d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(x+\mathrm{i}y\right)+\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)=x+\left(0{-}_{ℝ}x\right)$$
35	18 21	addcld	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x+\mathrm{i}y\in ℂ$$
36	35 12 15	addassd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(x+\mathrm{i}y\right)+\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)=x+\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)$$
37		renegid	$$⊢x\in ℝ\to x+\left(0{-}_{ℝ}x\right)=0$$
38	37	adantr	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x+\left(0{-}_{ℝ}x\right)=0$$
39	34 36 38	3eqtr3d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x+\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)=0$$
40	12 15 35	addassd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+x+\mathrm{i}y=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+\left(x+\mathrm{i}y\right)$$
41		renegid2	$$⊢x\in ℝ\to \left(0{-}_{ℝ}x\right)+x=0$$
42	41	adantr	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(0{-}_{ℝ}x\right)+x=0$$
43	42	oveq1d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(0{-}_{ℝ}x\right)+x+\mathrm{i}y=0+\mathrm{i}y$$
44	15 18 21	addassd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(0{-}_{ℝ}x\right)+x+\mathrm{i}y=\left(0{-}_{ℝ}x\right)+x+\mathrm{i}y$$
45		sn-addlid	$$⊢\mathrm{i}y\in ℂ\to 0+\mathrm{i}y=\mathrm{i}y$$
46	21 45	syl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 0+\mathrm{i}y=\mathrm{i}y$$
47	43 44 46	3eqtr3rd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}y=\left(0{-}_{ℝ}x\right)+x+\mathrm{i}y$$
48	47	oveq2d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\left(0{-}_{ℝ}y\right)+\mathrm{i}y=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+\left(x+\mathrm{i}y\right)$$
49	8 10 19	adddid	$$⊢y\in ℝ\to \mathrm{i}\left(\left(0{-}_{ℝ}y\right)+y\right)=\mathrm{i}\left(0{-}_{ℝ}y\right)+\mathrm{i}y$$
50		renegid2	$$⊢y\in ℝ\to \left(0{-}_{ℝ}y\right)+y=0$$
51	50	oveq2d	$$⊢y\in ℝ\to \mathrm{i}\left(\left(0{-}_{ℝ}y\right)+y\right)=\mathrm{i}\cdot 0$$
52	51 26	eqtrdi	$$⊢y\in ℝ\to \mathrm{i}\left(\left(0{-}_{ℝ}y\right)+y\right)=0$$
53	49 52	eqtr3d	$$⊢y\in ℝ\to \mathrm{i}\left(0{-}_{ℝ}y\right)+\mathrm{i}y=0$$
54	53	adantl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\left(0{-}_{ℝ}y\right)+\mathrm{i}y=0$$
55	40 48 54	3eqtr2d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+x+\mathrm{i}y=0$$
56	39 55	jca	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(x+\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)=0\wedge \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+x+\mathrm{i}y=0\right)$$
57	6 16 56	rspcedvdw	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \exists b\in ℂ\left(x+\mathrm{i}y+b=0\wedge b+x+\mathrm{i}y=0\right)$$
58	57	adantl	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to \exists b\in ℂ\left(x+\mathrm{i}y+b=0\wedge b+x+\mathrm{i}y=0\right)$$
59		oveq1	$$⊢A=x+\mathrm{i}y\to A+b=x+\mathrm{i}y+b$$
60	59	eqeq1d	$$⊢A=x+\mathrm{i}y\to \left(A+b=0\leftrightarrow x+\mathrm{i}y+b=0\right)$$
61		oveq2	$$⊢A=x+\mathrm{i}y\to b+A=b+x+\mathrm{i}y$$
62	61	eqeq1d	$$⊢A=x+\mathrm{i}y\to \left(b+A=0\leftrightarrow b+x+\mathrm{i}y=0\right)$$
63	60 62	anbi12d	$$⊢A=x+\mathrm{i}y\to \left(\left(A+b=0\wedge b+A=0\right)\leftrightarrow \left(x+\mathrm{i}y+b=0\wedge b+x+\mathrm{i}y=0\right)\right)$$
64	63	rexbidv	$$⊢A=x+\mathrm{i}y\to \left(\exists b\in ℂ\left(A+b=0\wedge b+A=0\right)\leftrightarrow \exists b\in ℂ\left(x+\mathrm{i}y+b=0\wedge b+x+\mathrm{i}y=0\right)\right)$$
65	58 64	syl5ibrcom	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to \left(A=x+\mathrm{i}y\to \exists b\in ℂ\left(A+b=0\wedge b+A=0\right)\right)$$
66	65	rexlimdvva	$$⊢A\in ℂ\to \left(\exists x\in ℝ\exists y\in ℝA=x+\mathrm{i}y\to \exists b\in ℂ\left(A+b=0\wedge b+A=0\right)\right)$$
67	1 66	mpd	$$⊢A\in ℂ\to \exists b\in ℂ\left(A+b=0\wedge b+A=0\right)$$