Theorem sqrtneg

Description: The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013)

	Ref	Expression
Assertion	sqrtneg	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ - 𝐴 ) = ( i · ( √ ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℂ )
3	2	negcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → - 𝐴 ∈ ℂ )
4		sqrtval	⊢ ( - 𝐴 ∈ ℂ → ( √ ‘ - 𝐴 ) = ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
5	3 4	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ - 𝐴 ) = ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
6		sqrtneglem	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( ( i · ( √ ‘ 𝐴 ) ) ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∉ ℝ+ ) )
7		ax-icn	⊢ i ∈ ℂ
8		resqrtcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℝ )
9	8	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℂ )
10		mulcl	⊢ ( ( i ∈ ℂ ∧ ( √ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( √ ‘ 𝐴 ) ) ∈ ℂ )
11	7 9 10	sylancr	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( i · ( √ ‘ 𝐴 ) ) ∈ ℂ )
12		oveq1	⊢ ( 𝑥 = ( i · ( √ ‘ 𝐴 ) ) → ( 𝑥 ↑ 2 ) = ( ( i · ( √ ‘ 𝐴 ) ) ↑ 2 ) )
13	12	eqeq1d	⊢ ( 𝑥 = ( i · ( √ ‘ 𝐴 ) ) → ( ( 𝑥 ↑ 2 ) = - 𝐴 ↔ ( ( i · ( √ ‘ 𝐴 ) ) ↑ 2 ) = - 𝐴 ) )
14		fveq2	⊢ ( 𝑥 = ( i · ( √ ‘ 𝐴 ) ) → ( ℜ ‘ 𝑥 ) = ( ℜ ‘ ( i · ( √ ‘ 𝐴 ) ) ) )
15	14	breq2d	⊢ ( 𝑥 = ( i · ( √ ‘ 𝐴 ) ) → ( 0 ≤ ( ℜ ‘ 𝑥 ) ↔ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ 𝐴 ) ) ) ) )
16		oveq2	⊢ ( 𝑥 = ( i · ( √ ‘ 𝐴 ) ) → ( i · 𝑥 ) = ( i · ( i · ( √ ‘ 𝐴 ) ) ) )
17		neleq1	⊢ ( ( i · 𝑥 ) = ( i · ( i · ( √ ‘ 𝐴 ) ) ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∉ ℝ+ ) )
18	16 17	syl	⊢ ( 𝑥 = ( i · ( √ ‘ 𝐴 ) ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∉ ℝ+ ) )
19	13 15 18	3anbi123d	⊢ ( 𝑥 = ( i · ( √ ‘ 𝐴 ) ) → ( ( ( 𝑥 ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ ( ( ( i · ( √ ‘ 𝐴 ) ) ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∉ ℝ+ ) ) )
20	19	rspcev	⊢ ( ( ( i · ( √ ‘ 𝐴 ) ) ∈ ℂ ∧ ( ( ( i · ( √ ‘ 𝐴 ) ) ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∉ ℝ+ ) ) → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
21	11 6 20	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
22		sqrmo	⊢ ( - 𝐴 ∈ ℂ → ∃* 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
23	3 22	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ∃* 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
24		reu5	⊢ ( ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ ( ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ∧ ∃* 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
25	21 23 24	sylanbrc	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
26	19	riota2	⊢ ( ( ( i · ( √ ‘ 𝐴 ) ) ∈ ℂ ∧ ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) → ( ( ( ( i · ( √ ‘ 𝐴 ) ) ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∉ ℝ+ ) ↔ ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) = ( i · ( √ ‘ 𝐴 ) ) ) )
27	11 25 26	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( ( ( i · ( √ ‘ 𝐴 ) ) ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∉ ℝ+ ) ↔ ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) = ( i · ( √ ‘ 𝐴 ) ) ) )
28	6 27	mpbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) = ( i · ( √ ‘ 𝐴 ) ) )
29	5 28	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ - 𝐴 ) = ( i · ( √ ‘ 𝐴 ) ) )