Metamath Proof Explorer

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 · ( √ ‘ 𝐴 ) ) )