Theorem addsqnreup

Description: There is no unique decomposition of a complex number as a sum of a complex number and a square of a complex number.

Remark: This theorem, together with addsq2reu , is a real life example (about a numerical property) showing that the pattern E! a e. A E! b e. B ph does not necessarily mean "There are unique sets a and b fulfilling ph "). See also comments for df-eu and 2eu4 .

In the case of decompositions of complex numbers as a sum of a complex number and a square of a complex number, the only/unique complex number to which the square of a unique complex number is added yields in the given complex number is the given number itself, and the unique complex number to be squared is 0 (see comment for addsq2reu ). There are, however, complex numbers to which the square of more than one other complex numbers can be added to yield the given complex number (see addsqrexnreu ). For example, <. 1 , ( sqrt( C - 1 ) ) >. and <. 1 , -u ( sqrt( C - 1 ) ) >. are two different decompositions of C (if C =/= 1 ). Therefore, there is no unique decomposition of any complex number as a sum of a complex number and a square of a complex number, as generally proved by this theorem.

As a consequence, a theorem must claim the existence of a unique pair of sets to express "There are unique a and b so that .." (more formally E! p e. ( A X. B ) ph with p = <. a , b >. ), or by showing ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) (see 2reu4 resp. 2eu4 ). These two representations are equivalent (see opreu2reurex ). An analogon of this theorem using the latter variant is given in addsqn2reurex2 . In some cases, however, the variant with (ordered!) pairs may be possible only for ordered sets (like RR or Prime ) and claiming that the first component is less than or equal to the second component (see, for example, 2sqreunnltb and 2sqreuopb ). Alternatively, (proper) unordered pairs can be used: E! p e ~P A ( ( #p ) = 2 /\ ph ) , or, using the definition of proper pairs: E! p e. ( PrPairsA ) ph (see, for example, inlinecirc02preu ). (Contributed by AV, 21-Jun-2023)

	Ref	Expression
Assertion	addsqnreup	|- ( C e. CC -> -. E! p e. ( CC X. CC ) ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = C )

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	|- 1 e. CC
2		0cn	|- 0 e. CC
3		opelxpi	|- ( ( 1 e. CC /\ 0 e. CC ) -> <. 1 , 0 >. e. ( CC X. CC ) )
4	1 2 3	mp2an	|- <. 1 , 0 >. e. ( CC X. CC )
5		3cn	|- 3 e. CC
6	5	negcli	|- -u 3 e. CC
7		2cn	|- 2 e. CC
8		opelxpi	|- ( ( -u 3 e. CC /\ 2 e. CC ) -> <. -u 3 , 2 >. e. ( CC X. CC ) )
9	6 7 8	mp2an	|- <. -u 3 , 2 >. e. ( CC X. CC )
10		0ne2	|- 0 =/= 2
11	10	olci	|- ( 1 =/= -u 3 \/ 0 =/= 2 )
12		1ex	|- 1 e. _V
13		c0ex	|- 0 e. _V
14	12 13	opthne	|- ( <. 1 , 0 >. =/= <. -u 3 , 2 >. <-> ( 1 =/= -u 3 \/ 0 =/= 2 ) )
15	11 14	mpbir	|- <. 1 , 0 >. =/= <. -u 3 , 2 >.
16	4 9 15	3pm3.2i	|- ( <. 1 , 0 >. e. ( CC X. CC ) /\ <. -u 3 , 2 >. e. ( CC X. CC ) /\ <. 1 , 0 >. =/= <. -u 3 , 2 >. )
17	12 13	op1st	|- ( 1st ` <. 1 , 0 >. ) = 1
18	12 13	op2nd	|- ( 2nd ` <. 1 , 0 >. ) = 0
19	18	oveq1i	|- ( ( 2nd ` <. 1 , 0 >. ) ^ 2 ) = ( 0 ^ 2 )
20		sq0	|- ( 0 ^ 2 ) = 0
21	19 20	eqtri	|- ( ( 2nd ` <. 1 , 0 >. ) ^ 2 ) = 0
22	17 21	oveq12i	|- ( ( 1st ` <. 1 , 0 >. ) + ( ( 2nd ` <. 1 , 0 >. ) ^ 2 ) ) = ( 1 + 0 )
23		1p0e1	|- ( 1 + 0 ) = 1
24	22 23	eqtri	|- ( ( 1st ` <. 1 , 0 >. ) + ( ( 2nd ` <. 1 , 0 >. ) ^ 2 ) ) = 1
25		negex	|- -u 3 e. _V
26		2ex	|- 2 e. _V
27	25 26	op1st	|- ( 1st ` <. -u 3 , 2 >. ) = -u 3
28	25 26	op2nd	|- ( 2nd ` <. -u 3 , 2 >. ) = 2
29	28	oveq1i	|- ( ( 2nd ` <. -u 3 , 2 >. ) ^ 2 ) = ( 2 ^ 2 )
30		sq2	|- ( 2 ^ 2 ) = 4
31	29 30	eqtri	|- ( ( 2nd ` <. -u 3 , 2 >. ) ^ 2 ) = 4
32	27 31	oveq12i	|- ( ( 1st ` <. -u 3 , 2 >. ) + ( ( 2nd ` <. -u 3 , 2 >. ) ^ 2 ) ) = ( -u 3 + 4 )
33		4cn	|- 4 e. CC
34	33 5	negsubi	|- ( 4 + -u 3 ) = ( 4 - 3 )
35		3p1e4	|- ( 3 + 1 ) = 4
36	33 5 1 35	subaddrii	|- ( 4 - 3 ) = 1
37	34 36	eqtri	|- ( 4 + -u 3 ) = 1
38	33 6 37	addcomli	|- ( -u 3 + 4 ) = 1
39	32 38	eqtri	|- ( ( 1st ` <. -u 3 , 2 >. ) + ( ( 2nd ` <. -u 3 , 2 >. ) ^ 2 ) ) = 1
40	24 39	pm3.2i	|- ( ( ( 1st ` <. 1 , 0 >. ) + ( ( 2nd ` <. 1 , 0 >. ) ^ 2 ) ) = 1 /\ ( ( 1st ` <. -u 3 , 2 >. ) + ( ( 2nd ` <. -u 3 , 2 >. ) ^ 2 ) ) = 1 )
41		fveq2	|- ( p = <. 1 , 0 >. -> ( 1st ` p ) = ( 1st ` <. 1 , 0 >. ) )
42		fveq2	|- ( p = <. 1 , 0 >. -> ( 2nd ` p ) = ( 2nd ` <. 1 , 0 >. ) )
43	42	oveq1d	|- ( p = <. 1 , 0 >. -> ( ( 2nd ` p ) ^ 2 ) = ( ( 2nd ` <. 1 , 0 >. ) ^ 2 ) )
44	41 43	oveq12d	|- ( p = <. 1 , 0 >. -> ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = ( ( 1st ` <. 1 , 0 >. ) + ( ( 2nd ` <. 1 , 0 >. ) ^ 2 ) ) )
45	44	eqeq1d	|- ( p = <. 1 , 0 >. -> ( ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = 1 <-> ( ( 1st ` <. 1 , 0 >. ) + ( ( 2nd ` <. 1 , 0 >. ) ^ 2 ) ) = 1 ) )
46		fveq2	|- ( p = <. -u 3 , 2 >. -> ( 1st ` p ) = ( 1st ` <. -u 3 , 2 >. ) )
47		fveq2	|- ( p = <. -u 3 , 2 >. -> ( 2nd ` p ) = ( 2nd ` <. -u 3 , 2 >. ) )
48	47	oveq1d	|- ( p = <. -u 3 , 2 >. -> ( ( 2nd ` p ) ^ 2 ) = ( ( 2nd ` <. -u 3 , 2 >. ) ^ 2 ) )
49	46 48	oveq12d	|- ( p = <. -u 3 , 2 >. -> ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = ( ( 1st ` <. -u 3 , 2 >. ) + ( ( 2nd ` <. -u 3 , 2 >. ) ^ 2 ) ) )
50	49	eqeq1d	|- ( p = <. -u 3 , 2 >. -> ( ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = 1 <-> ( ( 1st ` <. -u 3 , 2 >. ) + ( ( 2nd ` <. -u 3 , 2 >. ) ^ 2 ) ) = 1 ) )
51	45 50	2nreu	|- ( ( <. 1 , 0 >. e. ( CC X. CC ) /\ <. -u 3 , 2 >. e. ( CC X. CC ) /\ <. 1 , 0 >. =/= <. -u 3 , 2 >. ) -> ( ( ( ( 1st ` <. 1 , 0 >. ) + ( ( 2nd ` <. 1 , 0 >. ) ^ 2 ) ) = 1 /\ ( ( 1st ` <. -u 3 , 2 >. ) + ( ( 2nd ` <. -u 3 , 2 >. ) ^ 2 ) ) = 1 ) -> -. E! p e. ( CC X. CC ) ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = 1 ) )
52	16 40 51	mp2	|- -. E! p e. ( CC X. CC ) ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = 1
53		eqeq2	|- ( C = 1 -> ( ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = C <-> ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = 1 ) )
54	53	reubidv	|- ( C = 1 -> ( E! p e. ( CC X. CC ) ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = C <-> E! p e. ( CC X. CC ) ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = 1 ) )
55	52 54	mtbiri	|- ( C = 1 -> -. E! p e. ( CC X. CC ) ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = C )
56	55	a1d	|- ( C = 1 -> ( C e. CC -> -. E! p e. ( CC X. CC ) ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = C ) )
57		id	|- ( C e. CC -> C e. CC )
58		0cnd	|- ( C e. CC -> 0 e. CC )
59	57 58	opelxpd	|- ( C e. CC -> <. C , 0 >. e. ( CC X. CC ) )
60	59	adantr	|- ( ( C e. CC /\ C =/= 1 ) -> <. C , 0 >. e. ( CC X. CC ) )
61		1cnd	|- ( C e. CC -> 1 e. CC )
62		peano2cnm	|- ( C e. CC -> ( C - 1 ) e. CC )
63	62	sqrtcld	|- ( C e. CC -> ( sqrt ` ( C - 1 ) ) e. CC )
64	61 63	opelxpd	|- ( C e. CC -> <. 1 , ( sqrt ` ( C - 1 ) ) >. e. ( CC X. CC ) )
65	64	adantr	|- ( ( C e. CC /\ C =/= 1 ) -> <. 1 , ( sqrt ` ( C - 1 ) ) >. e. ( CC X. CC ) )
66		animorrl	|- ( ( C e. CC /\ C =/= 1 ) -> ( C =/= 1 \/ 0 =/= ( sqrt ` ( C - 1 ) ) ) )
67		0cnd	|- ( C =/= 1 -> 0 e. CC )
68		opthneg	|- ( ( C e. CC /\ 0 e. CC ) -> ( <. C , 0 >. =/= <. 1 , ( sqrt ` ( C - 1 ) ) >. <-> ( C =/= 1 \/ 0 =/= ( sqrt ` ( C - 1 ) ) ) ) )
69	67 68	sylan2	|- ( ( C e. CC /\ C =/= 1 ) -> ( <. C , 0 >. =/= <. 1 , ( sqrt ` ( C - 1 ) ) >. <-> ( C =/= 1 \/ 0 =/= ( sqrt ` ( C - 1 ) ) ) ) )
70	66 69	mpbird	|- ( ( C e. CC /\ C =/= 1 ) -> <. C , 0 >. =/= <. 1 , ( sqrt ` ( C - 1 ) ) >. )
71	60 65 70	3jca	|- ( ( C e. CC /\ C =/= 1 ) -> ( <. C , 0 >. e. ( CC X. CC ) /\ <. 1 , ( sqrt ` ( C - 1 ) ) >. e. ( CC X. CC ) /\ <. C , 0 >. =/= <. 1 , ( sqrt ` ( C - 1 ) ) >. ) )
72		op1stg	|- ( ( C e. CC /\ 0 e. CC ) -> ( 1st ` <. C , 0 >. ) = C )
73	58 72	mpdan	|- ( C e. CC -> ( 1st ` <. C , 0 >. ) = C )
74		op2ndg	|- ( ( C e. CC /\ 0 e. CC ) -> ( 2nd ` <. C , 0 >. ) = 0 )
75	58 74	mpdan	|- ( C e. CC -> ( 2nd ` <. C , 0 >. ) = 0 )
76	75	sq0id	|- ( C e. CC -> ( ( 2nd ` <. C , 0 >. ) ^ 2 ) = 0 )
77	73 76	oveq12d	|- ( C e. CC -> ( ( 1st ` <. C , 0 >. ) + ( ( 2nd ` <. C , 0 >. ) ^ 2 ) ) = ( C + 0 ) )
78		addid1	|- ( C e. CC -> ( C + 0 ) = C )
79	77 78	eqtrd	|- ( C e. CC -> ( ( 1st ` <. C , 0 >. ) + ( ( 2nd ` <. C , 0 >. ) ^ 2 ) ) = C )
80		op1stg	|- ( ( 1 e. CC /\ ( sqrt ` ( C - 1 ) ) e. CC ) -> ( 1st ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) = 1 )
81	61 63 80	syl2anc	|- ( C e. CC -> ( 1st ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) = 1 )
82		op2ndg	|- ( ( 1 e. CC /\ ( sqrt ` ( C - 1 ) ) e. CC ) -> ( 2nd ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) = ( sqrt ` ( C - 1 ) ) )
83	61 63 82	syl2anc	|- ( C e. CC -> ( 2nd ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) = ( sqrt ` ( C - 1 ) ) )
84	83	oveq1d	|- ( C e. CC -> ( ( 2nd ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) ^ 2 ) = ( ( sqrt ` ( C - 1 ) ) ^ 2 ) )
85	62	sqsqrtd	|- ( C e. CC -> ( ( sqrt ` ( C - 1 ) ) ^ 2 ) = ( C - 1 ) )
86	84 85	eqtrd	|- ( C e. CC -> ( ( 2nd ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) ^ 2 ) = ( C - 1 ) )
87	81 86	oveq12d	|- ( C e. CC -> ( ( 1st ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) + ( ( 2nd ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) ^ 2 ) ) = ( 1 + ( C - 1 ) ) )
88	61 57	pncan3d	|- ( C e. CC -> ( 1 + ( C - 1 ) ) = C )
89	87 88	eqtrd	|- ( C e. CC -> ( ( 1st ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) + ( ( 2nd ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) ^ 2 ) ) = C )
90	79 89	jca	|- ( C e. CC -> ( ( ( 1st ` <. C , 0 >. ) + ( ( 2nd ` <. C , 0 >. ) ^ 2 ) ) = C /\ ( ( 1st ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) + ( ( 2nd ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) ^ 2 ) ) = C ) )
91	90	adantr	|- ( ( C e. CC /\ C =/= 1 ) -> ( ( ( 1st ` <. C , 0 >. ) + ( ( 2nd ` <. C , 0 >. ) ^ 2 ) ) = C /\ ( ( 1st ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) + ( ( 2nd ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) ^ 2 ) ) = C ) )
92		fveq2	|- ( p = <. C , 0 >. -> ( 1st ` p ) = ( 1st ` <. C , 0 >. ) )
93		fveq2	|- ( p = <. C , 0 >. -> ( 2nd ` p ) = ( 2nd ` <. C , 0 >. ) )
94	93	oveq1d	|- ( p = <. C , 0 >. -> ( ( 2nd ` p ) ^ 2 ) = ( ( 2nd ` <. C , 0 >. ) ^ 2 ) )
95	92 94	oveq12d	|- ( p = <. C , 0 >. -> ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = ( ( 1st ` <. C , 0 >. ) + ( ( 2nd ` <. C , 0 >. ) ^ 2 ) ) )
96	95	eqeq1d	|- ( p = <. C , 0 >. -> ( ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = C <-> ( ( 1st ` <. C , 0 >. ) + ( ( 2nd ` <. C , 0 >. ) ^ 2 ) ) = C ) )
97		fveq2	|- ( p = <. 1 , ( sqrt ` ( C - 1 ) ) >. -> ( 1st ` p ) = ( 1st ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) )
98		fveq2	|- ( p = <. 1 , ( sqrt ` ( C - 1 ) ) >. -> ( 2nd ` p ) = ( 2nd ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) )
99	98	oveq1d	|- ( p = <. 1 , ( sqrt ` ( C - 1 ) ) >. -> ( ( 2nd ` p ) ^ 2 ) = ( ( 2nd ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) ^ 2 ) )
100	97 99	oveq12d	|- ( p = <. 1 , ( sqrt ` ( C - 1 ) ) >. -> ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = ( ( 1st ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) + ( ( 2nd ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) ^ 2 ) ) )
101	100	eqeq1d	|- ( p = <. 1 , ( sqrt ` ( C - 1 ) ) >. -> ( ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = C <-> ( ( 1st ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) + ( ( 2nd ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) ^ 2 ) ) = C ) )
102	96 101	2nreu	|- ( ( <. C , 0 >. e. ( CC X. CC ) /\ <. 1 , ( sqrt ` ( C - 1 ) ) >. e. ( CC X. CC ) /\ <. C , 0 >. =/= <. 1 , ( sqrt ` ( C - 1 ) ) >. ) -> ( ( ( ( 1st ` <. C , 0 >. ) + ( ( 2nd ` <. C , 0 >. ) ^ 2 ) ) = C /\ ( ( 1st ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) + ( ( 2nd ` <. 1 , ( sqrt ` ( C - 1 ) ) >. ) ^ 2 ) ) = C ) -> -. E! p e. ( CC X. CC ) ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = C ) )
103	71 91 102	sylc	|- ( ( C e. CC /\ C =/= 1 ) -> -. E! p e. ( CC X. CC ) ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = C )
104	103	expcom	|- ( C =/= 1 -> ( C e. CC -> -. E! p e. ( CC X. CC ) ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = C ) )
105	56 104	pm2.61ine	|- ( C e. CC -> -. E! p e. ( CC X. CC ) ( ( 1st ` p ) + ( ( 2nd ` p ) ^ 2 ) ) = C )