Theorem addsqrexnreu

Description: For each complex number, there exists a complex number to which the square of more than one (or no) other complex numbers can be added to result in the given complex number.

Remark: This theorem, together with addsq2reu , shows that there are cases in which there is a set together with a not unique other set fulfilling a wff, although there is a unique set fulfilling the wff together with another unique set (see addsq2reu ). For more details see comment for addsqnreup . (Contributed by AV, 20-Jun-2023)

	Ref	Expression
Assertion	addsqrexnreu	|- ( C e. CC -> E. a e. CC -. E! b e. CC ( a + ( b ^ 2 ) ) = C )

Proof

Step	Hyp	Ref	Expression
1		peano2cnm	|- ( C e. CC -> ( C - 1 ) e. CC )
2		oveq1	|- ( a = ( C - 1 ) -> ( a + ( b ^ 2 ) ) = ( ( C - 1 ) + ( b ^ 2 ) ) )
3	2	eqeq1d	|- ( a = ( C - 1 ) -> ( ( a + ( b ^ 2 ) ) = C <-> ( ( C - 1 ) + ( b ^ 2 ) ) = C ) )
4	3	reubidv	|- ( a = ( C - 1 ) -> ( E! b e. CC ( a + ( b ^ 2 ) ) = C <-> E! b e. CC ( ( C - 1 ) + ( b ^ 2 ) ) = C ) )
5	4	notbid	|- ( a = ( C - 1 ) -> ( -. E! b e. CC ( a + ( b ^ 2 ) ) = C <-> -. E! b e. CC ( ( C - 1 ) + ( b ^ 2 ) ) = C ) )
6	5	adantl	|- ( ( C e. CC /\ a = ( C - 1 ) ) -> ( -. E! b e. CC ( a + ( b ^ 2 ) ) = C <-> -. E! b e. CC ( ( C - 1 ) + ( b ^ 2 ) ) = C ) )
7		ax-1cn	|- 1 e. CC
8		neg1cn	|- -u 1 e. CC
9		1nn	|- 1 e. NN
10		nnneneg	|- ( 1 e. NN -> 1 =/= -u 1 )
11	9 10	ax-mp	|- 1 =/= -u 1
12	7 8 11	3pm3.2i	|- ( 1 e. CC /\ -u 1 e. CC /\ 1 =/= -u 1 )
13		sq1	|- ( 1 ^ 2 ) = 1
14	13	eqcomi	|- 1 = ( 1 ^ 2 )
15		neg1sqe1	|- ( -u 1 ^ 2 ) = 1
16	15	eqcomi	|- 1 = ( -u 1 ^ 2 )
17	14 16	pm3.2i	|- ( 1 = ( 1 ^ 2 ) /\ 1 = ( -u 1 ^ 2 ) )
18		oveq1	|- ( b = 1 -> ( b ^ 2 ) = ( 1 ^ 2 ) )
19	18	eqeq2d	|- ( b = 1 -> ( 1 = ( b ^ 2 ) <-> 1 = ( 1 ^ 2 ) ) )
20		oveq1	|- ( b = -u 1 -> ( b ^ 2 ) = ( -u 1 ^ 2 ) )
21	20	eqeq2d	|- ( b = -u 1 -> ( 1 = ( b ^ 2 ) <-> 1 = ( -u 1 ^ 2 ) ) )
22	19 21	2nreu	|- ( ( 1 e. CC /\ -u 1 e. CC /\ 1 =/= -u 1 ) -> ( ( 1 = ( 1 ^ 2 ) /\ 1 = ( -u 1 ^ 2 ) ) -> -. E! b e. CC 1 = ( b ^ 2 ) ) )
23	12 17 22	mp2	|- -. E! b e. CC 1 = ( b ^ 2 )
24		simpl	|- ( ( C e. CC /\ b e. CC ) -> C e. CC )
25	1	adantr	|- ( ( C e. CC /\ b e. CC ) -> ( C - 1 ) e. CC )
26		sqcl	|- ( b e. CC -> ( b ^ 2 ) e. CC )
27	26	adantl	|- ( ( C e. CC /\ b e. CC ) -> ( b ^ 2 ) e. CC )
28	24 25 27	subaddd	|- ( ( C e. CC /\ b e. CC ) -> ( ( C - ( C - 1 ) ) = ( b ^ 2 ) <-> ( ( C - 1 ) + ( b ^ 2 ) ) = C ) )
29		id	|- ( C e. CC -> C e. CC )
30		1cnd	|- ( C e. CC -> 1 e. CC )
31	29 30	nncand	|- ( C e. CC -> ( C - ( C - 1 ) ) = 1 )
32	31	adantr	|- ( ( C e. CC /\ b e. CC ) -> ( C - ( C - 1 ) ) = 1 )
33	32	eqeq1d	|- ( ( C e. CC /\ b e. CC ) -> ( ( C - ( C - 1 ) ) = ( b ^ 2 ) <-> 1 = ( b ^ 2 ) ) )
34	28 33	bitr3d	|- ( ( C e. CC /\ b e. CC ) -> ( ( ( C - 1 ) + ( b ^ 2 ) ) = C <-> 1 = ( b ^ 2 ) ) )
35	34	reubidva	|- ( C e. CC -> ( E! b e. CC ( ( C - 1 ) + ( b ^ 2 ) ) = C <-> E! b e. CC 1 = ( b ^ 2 ) ) )
36	23 35	mtbiri	|- ( C e. CC -> -. E! b e. CC ( ( C - 1 ) + ( b ^ 2 ) ) = C )
37	1 6 36	rspcedvd	|- ( C e. CC -> E. a e. CC -. E! b e. CC ( a + ( b ^ 2 ) ) = C )