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 ℂ (A + b = 0 \land b + A = 0)$

Proof

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

Metamath Proof Explorer

Theorem sn-negex12

Proof