Theorem addsqnreup 26496

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 26493, is a real life example (about a numerical property) showing that the pattern ∃!𝑎 ∈ 𝐴∃!𝑏 ∈ 𝐵𝜑 does not necessarily mean "There are unique sets 𝑎 and 𝑏 fulfilling 𝜑"). See also comments for df-eu 2569 and 2eu4 2656.

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 26493). 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 26495). For example, ⟨1, (√‘(𝐶 − 1))⟩ and ⟨1, -(√‘(𝐶 − 1))⟩ are two different decompositions of 𝐶 (if 𝐶 ≠ 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 𝑎 and 𝑏 so that .." (more formally ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑 with 𝑝 = ⟨𝑎, 𝑏⟩), or by showing (∃!𝑥 ∈ 𝐴∃𝑦 ∈ 𝐵𝜑 ∧ ∃!𝑦 ∈ 𝐵∃𝑥 ∈ 𝐴𝜑) (see 2reu4 4454 resp. 2eu4 2656). These two representations are equivalent (see opreu2reurex 6186). An analogon of this theorem using the latter variant is given in addsqn2reurex2 26498. In some cases, however, the variant with (ordered!) pairs may be possible only for ordered sets (like ℝ or ℙ) and claiming that the first component is less than or equal to the second component (see, for example, 2sqreunnltb 26514 and 2sqreuopb 26521). Alternatively, (proper) unordered pairs can be used: ∃!𝑝𝑒𝒫 𝐴((♯‘𝑝) = 2 ∧ 𝜑), or, using the definition of proper pairs: ∃!𝑝 ∈ (Pairs_proper‘𝐴)𝜑 (see, for example, inlinecirc02preu 46022). (Contributed by AV, 21-Jun-2023.)

Assertion

Ref	Expression
addsqnreup	⊢ (𝐶 ∈ ℂ → ¬ ∃!𝑝 ∈ (ℂ × ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶)

Distinct variable group:   𝐶,𝑝

Proof of Theorem addsqnreup

Step	Hyp	Ref	Expression
1		ax-1cn 10860	. . . . . . 7 ⊢ 1 ∈ ℂ
2		0cn 10898	. . . . . . 7 ⊢ 0 ∈ ℂ
3		opelxpi 5617	. . . . . . 7 ⊢ ((1 ∈ ℂ ∧ 0 ∈ ℂ) → ⟨1, 0⟩ ∈ (ℂ × ℂ))
4	1, 2, 3	mp2an 688	. . . . . 6 ⊢ ⟨1, 0⟩ ∈ (ℂ × ℂ)
5		3cn 11984	. . . . . . . 8 ⊢ 3 ∈ ℂ
6	5	negcli 11219	. . . . . . 7 ⊢ -3 ∈ ℂ
7		2cn 11978	. . . . . . 7 ⊢ 2 ∈ ℂ
8		opelxpi 5617	. . . . . . 7 ⊢ ((-3 ∈ ℂ ∧ 2 ∈ ℂ) → ⟨-3, 2⟩ ∈ (ℂ × ℂ))
9	6, 7, 8	mp2an 688	. . . . . 6 ⊢ ⟨-3, 2⟩ ∈ (ℂ × ℂ)
10		0ne2 12110	. . . . . . . 8 ⊢ 0 ≠ 2
11	10	olci 862	. . . . . . 7 ⊢ (1 ≠ -3 ∨ 0 ≠ 2)
12		1ex 10902	. . . . . . . 8 ⊢ 1 ∈ V
13		c0ex 10900	. . . . . . . 8 ⊢ 0 ∈ V
14	12, 13	opthne 5391	. . . . . . 7 ⊢ (⟨1, 0⟩ ≠ ⟨-3, 2⟩ ↔ (1 ≠ -3 ∨ 0 ≠ 2))
15	11, 14	mpbir 230	. . . . . 6 ⊢ ⟨1, 0⟩ ≠ ⟨-3, 2⟩
16	4, 9, 15	3pm3.2i 1337	. . . . 5 ⊢ (⟨1, 0⟩ ∈ (ℂ × ℂ) ∧ ⟨-3, 2⟩ ∈ (ℂ × ℂ) ∧ ⟨1, 0⟩ ≠ ⟨-3, 2⟩)
17	12, 13	op1st 7812	. . . . . . . 8 ⊢ (1st ‘⟨1, 0⟩) = 1
18	12, 13	op2nd 7813	. . . . . . . . . 10 ⊢ (2nd ‘⟨1, 0⟩) = 0
19	18	oveq1i 7265	. . . . . . . . 9 ⊢ ((2nd ‘⟨1, 0⟩)↑2) = (0↑2)
20		sq0 13837	. . . . . . . . 9 ⊢ (0↑2) = 0
21	19, 20	eqtri 2766	. . . . . . . 8 ⊢ ((2nd ‘⟨1, 0⟩)↑2) = 0
22	17, 21	oveq12i 7267	. . . . . . 7 ⊢ ((1st ‘⟨1, 0⟩) + ((2nd ‘⟨1, 0⟩)↑2)) = (1 + 0)
23		1p0e1 12027	. . . . . . 7 ⊢ (1 + 0) = 1
24	22, 23	eqtri 2766	. . . . . 6 ⊢ ((1st ‘⟨1, 0⟩) + ((2nd ‘⟨1, 0⟩)↑2)) = 1
25		negex 11149	. . . . . . . . 9 ⊢ -3 ∈ V
26		2ex 11980	. . . . . . . . 9 ⊢ 2 ∈ V
27	25, 26	op1st 7812	. . . . . . . 8 ⊢ (1st ‘⟨-3, 2⟩) = -3
28	25, 26	op2nd 7813	. . . . . . . . . 10 ⊢ (2nd ‘⟨-3, 2⟩) = 2
29	28	oveq1i 7265	. . . . . . . . 9 ⊢ ((2nd ‘⟨-3, 2⟩)↑2) = (2↑2)
30		sq2 13842	. . . . . . . . 9 ⊢ (2↑2) = 4
31	29, 30	eqtri 2766	. . . . . . . 8 ⊢ ((2nd ‘⟨-3, 2⟩)↑2) = 4
32	27, 31	oveq12i 7267	. . . . . . 7 ⊢ ((1st ‘⟨-3, 2⟩) + ((2nd ‘⟨-3, 2⟩)↑2)) = (-3 + 4)
33		4cn 11988	. . . . . . . 8 ⊢ 4 ∈ ℂ
34	33, 5	negsubi 11229	. . . . . . . . 9 ⊢ (4 + -3) = (4 − 3)
35		3p1e4 12048	. . . . . . . . . 10 ⊢ (3 + 1) = 4
36	33, 5, 1, 35	subaddrii 11240	. . . . . . . . 9 ⊢ (4 − 3) = 1
37	34, 36	eqtri 2766	. . . . . . . 8 ⊢ (4 + -3) = 1
38	33, 6, 37	addcomli 11097	. . . . . . 7 ⊢ (-3 + 4) = 1
39	32, 38	eqtri 2766	. . . . . 6 ⊢ ((1st ‘⟨-3, 2⟩) + ((2nd ‘⟨-3, 2⟩)↑2)) = 1
40	24, 39	pm3.2i 470	. . . . 5 ⊢ (((1st ‘⟨1, 0⟩) + ((2nd ‘⟨1, 0⟩)↑2)) = 1 ∧ ((1st ‘⟨-3, 2⟩) + ((2nd ‘⟨-3, 2⟩)↑2)) = 1)
41		fveq2 6756	. . . . . . . 8 ⊢ (𝑝 = ⟨1, 0⟩ → (1st ‘𝑝) = (1st ‘⟨1, 0⟩))
42		fveq2 6756	. . . . . . . . 9 ⊢ (𝑝 = ⟨1, 0⟩ → (2nd ‘𝑝) = (2nd ‘⟨1, 0⟩))
43	42	oveq1d 7270	. . . . . . . 8 ⊢ (𝑝 = ⟨1, 0⟩ → ((2nd ‘𝑝)↑2) = ((2nd ‘⟨1, 0⟩)↑2))
44	41, 43	oveq12d 7273	. . . . . . 7 ⊢ (𝑝 = ⟨1, 0⟩ → ((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = ((1st ‘⟨1, 0⟩) + ((2nd ‘⟨1, 0⟩)↑2)))
45	44	eqeq1d 2740	. . . . . 6 ⊢ (𝑝 = ⟨1, 0⟩ → (((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 1 ↔ ((1st ‘⟨1, 0⟩) + ((2nd ‘⟨1, 0⟩)↑2)) = 1))
46		fveq2 6756	. . . . . . . 8 ⊢ (𝑝 = ⟨-3, 2⟩ → (1st ‘𝑝) = (1st ‘⟨-3, 2⟩))
47		fveq2 6756	. . . . . . . . 9 ⊢ (𝑝 = ⟨-3, 2⟩ → (2nd ‘𝑝) = (2nd ‘⟨-3, 2⟩))
48	47	oveq1d 7270	. . . . . . . 8 ⊢ (𝑝 = ⟨-3, 2⟩ → ((2nd ‘𝑝)↑2) = ((2nd ‘⟨-3, 2⟩)↑2))
49	46, 48	oveq12d 7273	. . . . . . 7 ⊢ (𝑝 = ⟨-3, 2⟩ → ((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = ((1st ‘⟨-3, 2⟩) + ((2nd ‘⟨-3, 2⟩)↑2)))
50	49	eqeq1d 2740	. . . . . 6 ⊢ (𝑝 = ⟨-3, 2⟩ → (((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 1 ↔ ((1st ‘⟨-3, 2⟩) + ((2nd ‘⟨-3, 2⟩)↑2)) = 1))
51	45, 50	2nreu 4372	. . . . 5 ⊢ ((⟨1, 0⟩ ∈ (ℂ × ℂ) ∧ ⟨-3, 2⟩ ∈ (ℂ × ℂ) ∧ ⟨1, 0⟩ ≠ ⟨-3, 2⟩) → ((((1st ‘⟨1, 0⟩) + ((2nd ‘⟨1, 0⟩)↑2)) = 1 ∧ ((1st ‘⟨-3, 2⟩) + ((2nd ‘⟨-3, 2⟩)↑2)) = 1) → ¬ ∃!𝑝 ∈ (ℂ × ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 1))
52	16, 40, 51	mp2 9	. . . 4 ⊢ ¬ ∃!𝑝 ∈ (ℂ × ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 1
53		eqeq2 2750	. . . . 5 ⊢ (𝐶 = 1 → (((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶 ↔ ((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 1))
54	53	reubidv 3315	. . . 4 ⊢ (𝐶 = 1 → (∃!𝑝 ∈ (ℂ × ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶 ↔ ∃!𝑝 ∈ (ℂ × ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 1))
55	52, 54	mtbiri 326	. . 3 ⊢ (𝐶 = 1 → ¬ ∃!𝑝 ∈ (ℂ × ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶)
56	55	a1d 25	. 2 ⊢ (𝐶 = 1 → (𝐶 ∈ ℂ → ¬ ∃!𝑝 ∈ (ℂ × ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶))
57		id 22	. . . . . . 7 ⊢ (𝐶 ∈ ℂ → 𝐶 ∈ ℂ)
58		0cnd 10899	. . . . . . 7 ⊢ (𝐶 ∈ ℂ → 0 ∈ ℂ)
59	57, 58	opelxpd 5618	. . . . . 6 ⊢ (𝐶 ∈ ℂ → ⟨𝐶, 0⟩ ∈ (ℂ × ℂ))
60	59	adantr 480	. . . . 5 ⊢ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 1) → ⟨𝐶, 0⟩ ∈ (ℂ × ℂ))
61		1cnd 10901	. . . . . . 7 ⊢ (𝐶 ∈ ℂ → 1 ∈ ℂ)
62		peano2cnm 11217	. . . . . . . 8 ⊢ (𝐶 ∈ ℂ → (𝐶 − 1) ∈ ℂ)
63	62	sqrtcld 15077	. . . . . . 7 ⊢ (𝐶 ∈ ℂ → (√‘(𝐶 − 1)) ∈ ℂ)
64	61, 63	opelxpd 5618	. . . . . 6 ⊢ (𝐶 ∈ ℂ → ⟨1, (√‘(𝐶 − 1))⟩ ∈ (ℂ × ℂ))
65	64	adantr 480	. . . . 5 ⊢ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 1) → ⟨1, (√‘(𝐶 − 1))⟩ ∈ (ℂ × ℂ))
66		animorrl 977	. . . . . 6 ⊢ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 1) → (𝐶 ≠ 1 ∨ 0 ≠ (√‘(𝐶 − 1))))
67		0cnd 10899	. . . . . . 7 ⊢ (𝐶 ≠ 1 → 0 ∈ ℂ)
68		opthneg 5390	. . . . . . 7 ⊢ ((𝐶 ∈ ℂ ∧ 0 ∈ ℂ) → (⟨𝐶, 0⟩ ≠ ⟨1, (√‘(𝐶 − 1))⟩ ↔ (𝐶 ≠ 1 ∨ 0 ≠ (√‘(𝐶 − 1)))))
69	67, 68	sylan2 592	. . . . . 6 ⊢ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 1) → (⟨𝐶, 0⟩ ≠ ⟨1, (√‘(𝐶 − 1))⟩ ↔ (𝐶 ≠ 1 ∨ 0 ≠ (√‘(𝐶 − 1)))))
70	66, 69	mpbird 256	. . . . 5 ⊢ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 1) → ⟨𝐶, 0⟩ ≠ ⟨1, (√‘(𝐶 − 1))⟩)
71	60, 65, 70	3jca 1126	. . . 4 ⊢ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 1) → (⟨𝐶, 0⟩ ∈ (ℂ × ℂ) ∧ ⟨1, (√‘(𝐶 − 1))⟩ ∈ (ℂ × ℂ) ∧ ⟨𝐶, 0⟩ ≠ ⟨1, (√‘(𝐶 − 1))⟩))
72		op1stg 7816	. . . . . . . . 9 ⊢ ((𝐶 ∈ ℂ ∧ 0 ∈ ℂ) → (1st ‘⟨𝐶, 0⟩) = 𝐶)
73	58, 72	mpdan 683	. . . . . . . 8 ⊢ (𝐶 ∈ ℂ → (1st ‘⟨𝐶, 0⟩) = 𝐶)
74		op2ndg 7817	. . . . . . . . . 10 ⊢ ((𝐶 ∈ ℂ ∧ 0 ∈ ℂ) → (2nd ‘⟨𝐶, 0⟩) = 0)
75	58, 74	mpdan 683	. . . . . . . . 9 ⊢ (𝐶 ∈ ℂ → (2nd ‘⟨𝐶, 0⟩) = 0)
76	75	sq0id 13839	. . . . . . . 8 ⊢ (𝐶 ∈ ℂ → ((2nd ‘⟨𝐶, 0⟩)↑2) = 0)
77	73, 76	oveq12d 7273	. . . . . . 7 ⊢ (𝐶 ∈ ℂ → ((1st ‘⟨𝐶, 0⟩) + ((2nd ‘⟨𝐶, 0⟩)↑2)) = (𝐶 + 0))
78		addid1 11085	. . . . . . 7 ⊢ (𝐶 ∈ ℂ → (𝐶 + 0) = 𝐶)
79	77, 78	eqtrd 2778	. . . . . 6 ⊢ (𝐶 ∈ ℂ → ((1st ‘⟨𝐶, 0⟩) + ((2nd ‘⟨𝐶, 0⟩)↑2)) = 𝐶)
80		op1stg 7816	. . . . . . . . 9 ⊢ ((1 ∈ ℂ ∧ (√‘(𝐶 − 1)) ∈ ℂ) → (1st ‘⟨1, (√‘(𝐶 − 1))⟩) = 1)
81	61, 63, 80	syl2anc 583	. . . . . . . 8 ⊢ (𝐶 ∈ ℂ → (1st ‘⟨1, (√‘(𝐶 − 1))⟩) = 1)
82		op2ndg 7817	. . . . . . . . . . 11 ⊢ ((1 ∈ ℂ ∧ (√‘(𝐶 − 1)) ∈ ℂ) → (2nd ‘⟨1, (√‘(𝐶 − 1))⟩) = (√‘(𝐶 − 1)))
83	61, 63, 82	syl2anc 583	. . . . . . . . . 10 ⊢ (𝐶 ∈ ℂ → (2nd ‘⟨1, (√‘(𝐶 − 1))⟩) = (√‘(𝐶 − 1)))
84	83	oveq1d 7270	. . . . . . . . 9 ⊢ (𝐶 ∈ ℂ → ((2nd ‘⟨1, (√‘(𝐶 − 1))⟩)↑2) = ((√‘(𝐶 − 1))↑2))
85	62	sqsqrtd 15079	. . . . . . . . 9 ⊢ (𝐶 ∈ ℂ → ((√‘(𝐶 − 1))↑2) = (𝐶 − 1))
86	84, 85	eqtrd 2778	. . . . . . . 8 ⊢ (𝐶 ∈ ℂ → ((2nd ‘⟨1, (√‘(𝐶 − 1))⟩)↑2) = (𝐶 − 1))
87	81, 86	oveq12d 7273	. . . . . . 7 ⊢ (𝐶 ∈ ℂ → ((1st ‘⟨1, (√‘(𝐶 − 1))⟩) + ((2nd ‘⟨1, (√‘(𝐶 − 1))⟩)↑2)) = (1 + (𝐶 − 1)))
88	61, 57	pncan3d 11265	. . . . . . 7 ⊢ (𝐶 ∈ ℂ → (1 + (𝐶 − 1)) = 𝐶)
89	87, 88	eqtrd 2778	. . . . . 6 ⊢ (𝐶 ∈ ℂ → ((1st ‘⟨1, (√‘(𝐶 − 1))⟩) + ((2nd ‘⟨1, (√‘(𝐶 − 1))⟩)↑2)) = 𝐶)
90	79, 89	jca 511	. . . . 5 ⊢ (𝐶 ∈ ℂ → (((1st ‘⟨𝐶, 0⟩) + ((2nd ‘⟨𝐶, 0⟩)↑2)) = 𝐶 ∧ ((1st ‘⟨1, (√‘(𝐶 − 1))⟩) + ((2nd ‘⟨1, (√‘(𝐶 − 1))⟩)↑2)) = 𝐶))
91	90	adantr 480	. . . 4 ⊢ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 1) → (((1st ‘⟨𝐶, 0⟩) + ((2nd ‘⟨𝐶, 0⟩)↑2)) = 𝐶 ∧ ((1st ‘⟨1, (√‘(𝐶 − 1))⟩) + ((2nd ‘⟨1, (√‘(𝐶 − 1))⟩)↑2)) = 𝐶))
92		fveq2 6756	. . . . . . 7 ⊢ (𝑝 = ⟨𝐶, 0⟩ → (1st ‘𝑝) = (1st ‘⟨𝐶, 0⟩))
93		fveq2 6756	. . . . . . . 8 ⊢ (𝑝 = ⟨𝐶, 0⟩ → (2nd ‘𝑝) = (2nd ‘⟨𝐶, 0⟩))
94	93	oveq1d 7270	. . . . . . 7 ⊢ (𝑝 = ⟨𝐶, 0⟩ → ((2nd ‘𝑝)↑2) = ((2nd ‘⟨𝐶, 0⟩)↑2))
95	92, 94	oveq12d 7273	. . . . . 6 ⊢ (𝑝 = ⟨𝐶, 0⟩ → ((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = ((1st ‘⟨𝐶, 0⟩) + ((2nd ‘⟨𝐶, 0⟩)↑2)))
96	95	eqeq1d 2740	. . . . 5 ⊢ (𝑝 = ⟨𝐶, 0⟩ → (((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶 ↔ ((1st ‘⟨𝐶, 0⟩) + ((2nd ‘⟨𝐶, 0⟩)↑2)) = 𝐶))
97		fveq2 6756	. . . . . . 7 ⊢ (𝑝 = ⟨1, (√‘(𝐶 − 1))⟩ → (1st ‘𝑝) = (1st ‘⟨1, (√‘(𝐶 − 1))⟩))
98		fveq2 6756	. . . . . . . 8 ⊢ (𝑝 = ⟨1, (√‘(𝐶 − 1))⟩ → (2nd ‘𝑝) = (2nd ‘⟨1, (√‘(𝐶 − 1))⟩))
99	98	oveq1d 7270	. . . . . . 7 ⊢ (𝑝 = ⟨1, (√‘(𝐶 − 1))⟩ → ((2nd ‘𝑝)↑2) = ((2nd ‘⟨1, (√‘(𝐶 − 1))⟩)↑2))
100	97, 99	oveq12d 7273	. . . . . 6 ⊢ (𝑝 = ⟨1, (√‘(𝐶 − 1))⟩ → ((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = ((1st ‘⟨1, (√‘(𝐶 − 1))⟩) + ((2nd ‘⟨1, (√‘(𝐶 − 1))⟩)↑2)))
101	100	eqeq1d 2740	. . . . 5 ⊢ (𝑝 = ⟨1, (√‘(𝐶 − 1))⟩ → (((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶 ↔ ((1st ‘⟨1, (√‘(𝐶 − 1))⟩) + ((2nd ‘⟨1, (√‘(𝐶 − 1))⟩)↑2)) = 𝐶))
102	96, 101	2nreu 4372	. . . 4 ⊢ ((⟨𝐶, 0⟩ ∈ (ℂ × ℂ) ∧ ⟨1, (√‘(𝐶 − 1))⟩ ∈ (ℂ × ℂ) ∧ ⟨𝐶, 0⟩ ≠ ⟨1, (√‘(𝐶 − 1))⟩) → ((((1st ‘⟨𝐶, 0⟩) + ((2nd ‘⟨𝐶, 0⟩)↑2)) = 𝐶 ∧ ((1st ‘⟨1, (√‘(𝐶 − 1))⟩) + ((2nd ‘⟨1, (√‘(𝐶 − 1))⟩)↑2)) = 𝐶) → ¬ ∃!𝑝 ∈ (ℂ × ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶))
103	71, 91, 102	sylc 65	. . 3 ⊢ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 1) → ¬ ∃!𝑝 ∈ (ℂ × ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶)
104	103	expcom 413	. 2 ⊢ (𝐶 ≠ 1 → (𝐶 ∈ ℂ → ¬ ∃!𝑝 ∈ (ℂ × ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶))
105	56, 104	pm2.61ine 3027	1 ⊢ (𝐶 ∈ ℂ → ¬ ∃!𝑝 ∈ (ℂ × ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  ∃!wreu 3065  ⟨cop 4564   × cxp 5578  ‘cfv 6418  (class class class)co 7255  1^st c1st 7802  2^nd c2nd 7803  ℂcc 10800  0cc0 10802  1c1 10803   + caddc 10805   − cmin 11135  -cneg 11136  2c2 11958  3c3 11959  4c4 11960  ↑cexp 13710  √csqrt 14872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879  ax-pre-sup 10880

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-sup 9131  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-div 11563  df-nn 11904  df-2 11966  df-3 11967  df-4 11968  df-n0 12164  df-z 12250  df-uz 12512  df-rp 12660  df-seq 13650  df-exp 13711  df-cj 14738  df-re 14739  df-im 14740  df-sqrt 14874  df-abs 14875

This theorem is referenced by: (None)