Metamath Proof Explorer

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∈ℂ→¬∃!p∈ℂ×ℂ1st⁡p+2nd⁡p2=C

Proof

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