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	$$⊢A\in ℂ\to \exists b\in ℂ\left(A+b=0\wedge b+A=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2	1	a1i	$$⊢y\in ℝ\to \mathrm{i}\in ℂ$$
3		rernegcl	$$⊢y\in ℝ\to 0{-}_{ℝ}y\in ℝ$$
4	3	recnd	$$⊢y\in ℝ\to 0{-}_{ℝ}y\in ℂ$$
5	2 4	mulcld	$$⊢y\in ℝ\to \mathrm{i}\left(0{-}_{ℝ}y\right)\in ℂ$$
6	5	adantl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\left(0{-}_{ℝ}y\right)\in ℂ$$
7		rernegcl	$$⊢x\in ℝ\to 0{-}_{ℝ}x\in ℝ$$
8	7	recnd	$$⊢x\in ℝ\to 0{-}_{ℝ}x\in ℂ$$
9	8	adantr	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 0{-}_{ℝ}x\in ℂ$$
10	6 9	addcld	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\in ℂ$$
11	10	adantl	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\in ℂ$$
12		eqeq1	$$⊢b=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\to \left(b=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\leftrightarrow \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\right)$$
13	12	adantl	$$⊢\left(\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\wedge b=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\right)\to \left(b=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\leftrightarrow \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\right)$$
14		eqidd	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)$$
15	11 13 14	rspcedvd	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to \exists b\in ℂb=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)$$
16	15	ralrimivva	$$⊢A\in ℂ\to \forall x\in ℝ\forall y\in ℝ\exists b\in ℂb=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)$$
17		cnre	$$⊢A\in ℂ\to \exists x\in ℝ\exists y\in ℝA=x+\mathrm{i}y$$
18	16 17	r19.29d2r	$$⊢A\in ℂ\to \exists x\in ℝ\exists y\in ℝ\left(\exists b\in ℂb=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\wedge A=x+\mathrm{i}y\right)$$
19		oveq1	$$⊢A=x+\mathrm{i}y\to A+\mathrm{i}\left(0{-}_{ℝ}y\right)=x+\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)$$
20	19	adantl	$$⊢\left(\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\wedge A=x+\mathrm{i}y\right)\to A+\mathrm{i}\left(0{-}_{ℝ}y\right)=x+\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)$$
21		recn	$$⊢x\in ℝ\to x\in ℂ$$
22	21	adantr	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x\in ℂ$$
23	1	a1i	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\in ℂ$$
24		recn	$$⊢y\in ℝ\to y\in ℂ$$
25	24	adantl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to y\in ℂ$$
26	23 25	mulcld	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}y\in ℂ$$
27	22 26 6	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)$$
28		renegid	$$⊢y\in ℝ\to y+\left(0{-}_{ℝ}y\right)=0$$
29	28	oveq2d	$$⊢y\in ℝ\to \mathrm{i}\left(y+\left(0{-}_{ℝ}y\right)\right)=\mathrm{i}\cdot 0$$
30	2 24 4	adddid	$$⊢y\in ℝ\to \mathrm{i}\left(y+\left(0{-}_{ℝ}y\right)\right)=\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)$$
31		sn-it0e0	$$⊢\mathrm{i}\cdot 0=0$$
32	31	a1i	$$⊢y\in ℝ\to \mathrm{i}\cdot 0=0$$
33	29 30 32	3eqtr3d	$$⊢y\in ℝ\to \mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)=0$$
34	33	oveq2d	$$⊢y\in ℝ\to x+\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)=x+0$$
35	34	adantl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x+\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)=x+0$$
36		readdrid	$$⊢x\in ℝ\to x+0=x$$
37	36	adantr	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x+0=x$$
38	27 35 37	3eqtrd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x+\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)=x$$
39	38	ad2antlr	$$⊢\left(\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\wedge A=x+\mathrm{i}y\right)\to x+\mathrm{i}y+\mathrm{i}\left(0{-}_{ℝ}y\right)=x$$
40	20 39	eqtrd	$$⊢\left(\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\wedge A=x+\mathrm{i}y\right)\to A+\mathrm{i}\left(0{-}_{ℝ}y\right)=x$$
41	40	oveq1d	$$⊢\left(\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\wedge A=x+\mathrm{i}y\right)\to A+\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)=x+\left(0{-}_{ℝ}x\right)$$
42		simpll	$$⊢\left(\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\wedge A=x+\mathrm{i}y\right)\to A\in ℂ$$
43	6	ad2antlr	$$⊢\left(\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\wedge A=x+\mathrm{i}y\right)\to \mathrm{i}\left(0{-}_{ℝ}y\right)\in ℂ$$
44	9	ad2antlr	$$⊢\left(\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\wedge A=x+\mathrm{i}y\right)\to 0{-}_{ℝ}x\in ℂ$$
45	42 43 44	addassd	$$⊢\left(\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\wedge A=x+\mathrm{i}y\right)\to A+\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)=A+\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)$$
46		renegid	$$⊢x\in ℝ\to x+\left(0{-}_{ℝ}x\right)=0$$
47	46	adantr	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x+\left(0{-}_{ℝ}x\right)=0$$
48	47	ad2antlr	$$⊢\left(\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\wedge A=x+\mathrm{i}y\right)\to x+\left(0{-}_{ℝ}x\right)=0$$
49	41 45 48	3eqtr3d	$$⊢\left(\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\wedge A=x+\mathrm{i}y\right)\to A+\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)=0$$
50		oveq2	$$⊢A=x+\mathrm{i}y\to \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+A=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+x+\mathrm{i}y$$
51	22 26	addcld	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x+\mathrm{i}y\in ℂ$$
52	6 9 51	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)$$
53	9 22 26	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$$
54	53	oveq2d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(\left(0{-}_{ℝ}x\right)+x\right)+\mathrm{i}y=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+\left(x+\mathrm{i}y\right)$$
55		renegid2	$$⊢x\in ℝ\to \left(0{-}_{ℝ}x\right)+x=0$$
56	55	adantr	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(0{-}_{ℝ}x\right)+x=0$$
57	56	oveq1d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(0{-}_{ℝ}x\right)+x+\mathrm{i}y=0+\mathrm{i}y$$
58		sn-addlid	$$⊢\mathrm{i}y\in ℂ\to 0+\mathrm{i}y=\mathrm{i}y$$
59	26 58	syl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 0+\mathrm{i}y=\mathrm{i}y$$
60	57 59	eqtrd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(0{-}_{ℝ}x\right)+x+\mathrm{i}y=\mathrm{i}y$$
61	60	oveq2d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(\left(0{-}_{ℝ}x\right)+x\right)+\mathrm{i}y=\mathrm{i}\left(0{-}_{ℝ}y\right)+\mathrm{i}y$$
62	4	adantl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 0{-}_{ℝ}y\in ℂ$$
63	23 62 25	adddid	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\left(\left(0{-}_{ℝ}y\right)+y\right)=\mathrm{i}\left(0{-}_{ℝ}y\right)+\mathrm{i}y$$
64		renegid2	$$⊢y\in ℝ\to \left(0{-}_{ℝ}y\right)+y=0$$
65	64	adantl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(0{-}_{ℝ}y\right)+y=0$$
66	65	oveq2d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\left(\left(0{-}_{ℝ}y\right)+y\right)=\mathrm{i}\cdot 0$$
67	66 31	eqtrdi	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\left(\left(0{-}_{ℝ}y\right)+y\right)=0$$
68	61 63 67	3eqtr2d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(\left(0{-}_{ℝ}x\right)+x\right)+\mathrm{i}y=0$$
69	52 54 68	3eqtr2d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+x+\mathrm{i}y=0$$
70	69	adantl	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+x+\mathrm{i}y=0$$
71	50 70	sylan9eqr	$$⊢\left(\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\wedge A=x+\mathrm{i}y\right)\to \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+A=0$$
72	49 71	jca	$$⊢\left(\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\wedge A=x+\mathrm{i}y\right)\to \left(A+\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)=0\wedge \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+A=0\right)$$
73		oveq2	$$⊢b=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\to A+b=A+\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)$$
74	73	eqeq1d	$$⊢b=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\to \left(A+b=0\leftrightarrow A+\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)=0\right)$$
75		oveq1	$$⊢b=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\to b+A=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+A$$
76	75	eqeq1d	$$⊢b=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\to \left(b+A=0\leftrightarrow \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+A=0\right)$$
77	74 76	anbi12d	$$⊢b=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\to \left(\left(A+b=0\wedge b+A=0\right)\leftrightarrow \left(A+\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)=0\wedge \mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)+A=0\right)\right)$$
78	72 77	syl5ibrcom	$$⊢\left(\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\wedge A=x+\mathrm{i}y\right)\to \left(b=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\to \left(A+b=0\wedge b+A=0\right)\right)$$
79	78	reximdv	$$⊢\left(\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\wedge A=x+\mathrm{i}y\right)\to \left(\exists b\in ℂb=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\to \exists b\in ℂ\left(A+b=0\wedge b+A=0\right)\right)$$
80	79	expimpd	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to \left(\left(A=x+\mathrm{i}y\wedge \exists b\in ℂb=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\right)\to \exists b\in ℂ\left(A+b=0\wedge b+A=0\right)\right)$$
81	80	ancomsd	$$⊢\left(A\in ℂ\wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to \left(\left(\exists b\in ℂb=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\wedge A=x+\mathrm{i}y\right)\to \exists b\in ℂ\left(A+b=0\wedge b+A=0\right)\right)$$
82	81	rexlimdvva	$$⊢A\in ℂ\to \left(\exists x\in ℝ\exists y\in ℝ\left(\exists b\in ℂb=\mathrm{i}\left(0{-}_{ℝ}y\right)+\left(0{-}_{ℝ}x\right)\wedge A=x+\mathrm{i}y\right)\to \exists b\in ℂ\left(A+b=0\wedge b+A=0\right)\right)$$
83	18 82	mpd	$$⊢A\in ℂ\to \exists b\in ℂ\left(A+b=0\wedge b+A=0\right)$$