addsqn2reu

Description: For each complex number C , there does not exist a unique complex number b , squared and added to a unique another complex number a resulting in the given complex number C . Actually, for each complex number b , a = ( C - ( b ^ 2 ) ) is unique.

Remark: This, together with addsq2reu , shows that commutation of two unique quantifications need not be equivalent, and provides an evident justification of the fact that considering the pair of variables is necessary to obtain what we intuitively understand as "double unique existence". (Proposed by GL, 23-Jun-2023.). (Contributed by AV, 23-Jun-2023)

		Ref	Expression
	Assertion	addsqn2reu	$⊢ C \in ℂ \to \neg \exists! b \in ℂ \exists! a \in ℂ a + b^{2} = C$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$⊢ 1 \in ℂ$
2		neg1cn	$⊢ - 1 \in ℂ$
3		1nn	$⊢ 1 \in ℕ$
4		nnneneg	$⊢ 1 \in ℕ \to 1 \neq - 1$
5	3 4	ax-mp	$⊢ 1 \neq - 1$
6	1 2 5	3pm3.2i	$⊢ (1 \in ℂ \land - 1 \in ℂ \land 1 \neq - 1)$
7		1cnd	$⊢ C \in ℂ \to 1 \in ℂ$
8		negeu	$⊢ (1 \in ℂ \land C \in ℂ) \to \exists! a \in ℂ 1 + a = C$
9	7 8	mpancom	$⊢ C \in ℂ \to \exists! a \in ℂ 1 + a = C$
10		sq1	$⊢ 1^{2} = 1$
11	10	a1i	$⊢ (C \in ℂ \land a \in ℂ) \to 1^{2} = 1$
12	11	oveq2d	$⊢ (C \in ℂ \land a \in ℂ) \to a + 1^{2} = a + 1$
13		id	$⊢ a \in ℂ \to a \in ℂ$
14		1cnd	$⊢ a \in ℂ \to 1 \in ℂ$
15	13 14	addcomd	$⊢ a \in ℂ \to a + 1 = 1 + a$
16	15	adantl	$⊢ (C \in ℂ \land a \in ℂ) \to a + 1 = 1 + a$
17	12 16	eqtrd	$⊢ (C \in ℂ \land a \in ℂ) \to a + 1^{2} = 1 + a$
18	17	eqeq1d	$⊢ (C \in ℂ \land a \in ℂ) \to (a + 1^{2} = C \leftrightarrow 1 + a = C)$
19	18	reubidva	$⊢ C \in ℂ \to (\exists! a \in ℂ a + 1^{2} = C \leftrightarrow \exists! a \in ℂ 1 + a = C)$
20	9 19	mpbird	$⊢ C \in ℂ \to \exists! a \in ℂ a + 1^{2} = C$
21		neg1sqe1	$⊢ {(- 1)}^{2} = 1$
22	21	a1i	$⊢ (C \in ℂ \land a \in ℂ) \to {(- 1)}^{2} = 1$
23	22	oveq2d	$⊢ (C \in ℂ \land a \in ℂ) \to a + {(- 1)}^{2} = a + 1$
24	23 16	eqtrd	$⊢ (C \in ℂ \land a \in ℂ) \to a + {(- 1)}^{2} = 1 + a$
25	24	eqeq1d	$⊢ (C \in ℂ \land a \in ℂ) \to (a + {(- 1)}^{2} = C \leftrightarrow 1 + a = C)$
26	25	reubidva	$⊢ C \in ℂ \to (\exists! a \in ℂ a + {(- 1)}^{2} = C \leftrightarrow \exists! a \in ℂ 1 + a = C)$
27	9 26	mpbird	$⊢ C \in ℂ \to \exists! a \in ℂ a + {(- 1)}^{2} = C$
28	20 27	jca	$⊢ C \in ℂ \to (\exists! a \in ℂ a + 1^{2} = C \land \exists! a \in ℂ a + {(- 1)}^{2} = C)$
29		oveq1	$⊢ b = 1 \to b^{2} = 1^{2}$
30	29	oveq2d	$⊢ b = 1 \to a + b^{2} = a + 1^{2}$
31	30	eqeq1d	$⊢ b = 1 \to (a + b^{2} = C \leftrightarrow a + 1^{2} = C)$
32	31	reubidv	$⊢ b = 1 \to (\exists! a \in ℂ a + b^{2} = C \leftrightarrow \exists! a \in ℂ a + 1^{2} = C)$
33		oveq1	$⊢ b = - 1 \to b^{2} = {(- 1)}^{2}$
34	33	oveq2d	$⊢ b = - 1 \to a + b^{2} = a + {(- 1)}^{2}$
35	34	eqeq1d	$⊢ b = - 1 \to (a + b^{2} = C \leftrightarrow a + {(- 1)}^{2} = C)$
36	35	reubidv	$⊢ b = - 1 \to (\exists! a \in ℂ a + b^{2} = C \leftrightarrow \exists! a \in ℂ a + {(- 1)}^{2} = C)$
37	32 36	2nreu	$⊢ (1 \in ℂ \land - 1 \in ℂ \land 1 \neq - 1) \to ((\exists! a \in ℂ a + 1^{2} = C \land \exists! a \in ℂ a + {(- 1)}^{2} = C) \to \neg \exists! b \in ℂ \exists! a \in ℂ a + b^{2} = C)$
38	6 28 37	mpsyl	$⊢ C \in ℂ \to \neg \exists! b \in ℂ \exists! a \in ℂ a + b^{2} = C$

Metamath Proof Explorer

Theorem addsqn2reu

Proof