Theorem sqreu

Description: Existence and uniqueness for the square root function in general. (Contributed by Mario Carneiro, 9-Jul-2013)

	Ref	Expression
Assertion	sqreu	⊢ ( 𝐴 ∈ ℂ → ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )

Proof

Step	Hyp	Ref	Expression
1		abscl	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
2	1	recnd	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℂ )
3		subneg	⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( abs ‘ 𝐴 ) − - 𝐴 ) = ( ( abs ‘ 𝐴 ) + 𝐴 ) )
4	2 3	mpancom	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) − - 𝐴 ) = ( ( abs ‘ 𝐴 ) + 𝐴 ) )
5	4	eqeq1d	⊢ ( 𝐴 ∈ ℂ → ( ( ( abs ‘ 𝐴 ) − - 𝐴 ) = 0 ↔ ( ( abs ‘ 𝐴 ) + 𝐴 ) = 0 ) )
6		negcl	⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
7	2 6	subeq0ad	⊢ ( 𝐴 ∈ ℂ → ( ( ( abs ‘ 𝐴 ) − - 𝐴 ) = 0 ↔ ( abs ‘ 𝐴 ) = - 𝐴 ) )
8	5 7	bitr3d	⊢ ( 𝐴 ∈ ℂ → ( ( ( abs ‘ 𝐴 ) + 𝐴 ) = 0 ↔ ( abs ‘ 𝐴 ) = - 𝐴 ) )
9		ax-icn	⊢ i ∈ ℂ
10		absge0	⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( abs ‘ 𝐴 ) )
11	1 10	jca	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) )
12		eleq1	⊢ ( ( abs ‘ 𝐴 ) = - 𝐴 → ( ( abs ‘ 𝐴 ) ∈ ℝ ↔ - 𝐴 ∈ ℝ ) )
13		breq2	⊢ ( ( abs ‘ 𝐴 ) = - 𝐴 → ( 0 ≤ ( abs ‘ 𝐴 ) ↔ 0 ≤ - 𝐴 ) )
14	12 13	anbi12d	⊢ ( ( abs ‘ 𝐴 ) = - 𝐴 → ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) ↔ ( - 𝐴 ∈ ℝ ∧ 0 ≤ - 𝐴 ) ) )
15	11 14	imbitrid	⊢ ( ( abs ‘ 𝐴 ) = - 𝐴 → ( 𝐴 ∈ ℂ → ( - 𝐴 ∈ ℝ ∧ 0 ≤ - 𝐴 ) ) )
16	15	impcom	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ( - 𝐴 ∈ ℝ ∧ 0 ≤ - 𝐴 ) )
17		resqrtcl	⊢ ( ( - 𝐴 ∈ ℝ ∧ 0 ≤ - 𝐴 ) → ( √ ‘ - 𝐴 ) ∈ ℝ )
18	16 17	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ( √ ‘ - 𝐴 ) ∈ ℝ )
19	18	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ( √ ‘ - 𝐴 ) ∈ ℂ )
20		mulcl	⊢ ( ( i ∈ ℂ ∧ ( √ ‘ - 𝐴 ) ∈ ℂ ) → ( i · ( √ ‘ - 𝐴 ) ) ∈ ℂ )
21	9 19 20	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ( i · ( √ ‘ - 𝐴 ) ) ∈ ℂ )
22		sqrtneglem	⊢ ( ( - 𝐴 ∈ ℝ ∧ 0 ≤ - 𝐴 ) → ( ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = - - 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) )
23	16 22	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ( ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = - - 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) )
24		negneg	⊢ ( 𝐴 ∈ ℂ → - - 𝐴 = 𝐴 )
25	24	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → - - 𝐴 = 𝐴 )
26	25	eqeq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ( ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = - - 𝐴 ↔ ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = 𝐴 ) )
27	26	3anbi1d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ( ( ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = - - 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) ↔ ( ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) ) )
28	23 27	mpbid	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ( ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) )
29		oveq1	⊢ ( 𝑥 = ( i · ( √ ‘ - 𝐴 ) ) → ( 𝑥 ↑ 2 ) = ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) )
30	29	eqeq1d	⊢ ( 𝑥 = ( i · ( √ ‘ - 𝐴 ) ) → ( ( 𝑥 ↑ 2 ) = 𝐴 ↔ ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = 𝐴 ) )
31		fveq2	⊢ ( 𝑥 = ( i · ( √ ‘ - 𝐴 ) ) → ( ℜ ‘ 𝑥 ) = ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) )
32	31	breq2d	⊢ ( 𝑥 = ( i · ( √ ‘ - 𝐴 ) ) → ( 0 ≤ ( ℜ ‘ 𝑥 ) ↔ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) ) )
33		oveq2	⊢ ( 𝑥 = ( i · ( √ ‘ - 𝐴 ) ) → ( i · 𝑥 ) = ( i · ( i · ( √ ‘ - 𝐴 ) ) ) )
34		neleq1	⊢ ( ( i · 𝑥 ) = ( i · ( i · ( √ ‘ - 𝐴 ) ) ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) )
35	33 34	syl	⊢ ( 𝑥 = ( i · ( √ ‘ - 𝐴 ) ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) )
36	30 32 35	3anbi123d	⊢ ( 𝑥 = ( i · ( √ ‘ - 𝐴 ) ) → ( ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ ( ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) ) )
37	36	rspcev	⊢ ( ( ( i · ( √ ‘ - 𝐴 ) ) ∈ ℂ ∧ ( ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) ) → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
38	21 28 37	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
39	38	ex	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) = - 𝐴 → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
40	8 39	sylbid	⊢ ( 𝐴 ∈ ℂ → ( ( ( abs ‘ 𝐴 ) + 𝐴 ) = 0 → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
41		resqrtcl	⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) → ( √ ‘ ( abs ‘ 𝐴 ) ) ∈ ℝ )
42	1 10 41	syl2anc	⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( abs ‘ 𝐴 ) ) ∈ ℝ )
43	42	recnd	⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( abs ‘ 𝐴 ) ) ∈ ℂ )
44	43	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ( √ ‘ ( abs ‘ 𝐴 ) ) ∈ ℂ )
45		addcl	⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( abs ‘ 𝐴 ) + 𝐴 ) ∈ ℂ )
46	2 45	mpancom	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) + 𝐴 ) ∈ ℂ )
47	46	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ( ( abs ‘ 𝐴 ) + 𝐴 ) ∈ ℂ )
48		abscl	⊢ ( ( ( abs ‘ 𝐴 ) + 𝐴 ) ∈ ℂ → ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ∈ ℝ )
49	46 48	syl	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ∈ ℝ )
50	49	recnd	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ∈ ℂ )
51	50	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ∈ ℂ )
52	46	abs00ad	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) = 0 ↔ ( ( abs ‘ 𝐴 ) + 𝐴 ) = 0 ) )
53	52	necon3bid	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ≠ 0 ↔ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) )
54	53	biimpar	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ≠ 0 )
55	47 51 54	divcld	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ∈ ℂ )
56	44 55	mulcld	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ∈ ℂ )
57		eqid	⊢ ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) )
58	57	sqreulem	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ( ( ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∧ ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∉ ℝ+ ) )
59		oveq1	⊢ ( 𝑥 = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) → ( 𝑥 ↑ 2 ) = ( ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ↑ 2 ) )
60	59	eqeq1d	⊢ ( 𝑥 = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) → ( ( 𝑥 ↑ 2 ) = 𝐴 ↔ ( ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ↑ 2 ) = 𝐴 ) )
61		fveq2	⊢ ( 𝑥 = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) → ( ℜ ‘ 𝑥 ) = ( ℜ ‘ ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) )
62	61	breq2d	⊢ ( 𝑥 = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) → ( 0 ≤ ( ℜ ‘ 𝑥 ) ↔ 0 ≤ ( ℜ ‘ ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ) )
63		oveq2	⊢ ( 𝑥 = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) → ( i · 𝑥 ) = ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) )
64		neleq1	⊢ ( ( i · 𝑥 ) = ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∉ ℝ+ ) )
65	63 64	syl	⊢ ( 𝑥 = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∉ ℝ+ ) )
66	60 62 65	3anbi123d	⊢ ( 𝑥 = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) → ( ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ ( ( ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∧ ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∉ ℝ+ ) ) )
67	66	rspcev	⊢ ( ( ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ∈ ℂ ∧ ( ( ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∧ ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∉ ℝ+ ) ) → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
68	56 58 67	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
69	68	ex	⊢ ( 𝐴 ∈ ℂ → ( ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
70	40 69	pm2.61dne	⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
71		sqrmo	⊢ ( 𝐴 ∈ ℂ → ∃* 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
72		reu5	⊢ ( ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ ( ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ∧ ∃* 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
73	70 71 72	sylanbrc	⊢ ( 𝐴 ∈ ℂ → ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )