Metamath Proof Explorer

Theorem resqreu

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

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

Proof

Step Hyp Ref Expression
1 resqrex ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( 0 ≤ 𝑥 ∧ ( 𝑥 ↑ 2 ) = 𝐴 ) )
2 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
3 2 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 0 ≤ 𝑥 ∧ ( 𝑥 ↑ 2 ) = 𝐴 ) ) → 𝑥 ∈ ℂ )
4 simprr ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 0 ≤ 𝑥 ∧ ( 𝑥 ↑ 2 ) = 𝐴 ) ) → ( 𝑥 ↑ 2 ) = 𝐴 )
5 rere ⊢ ( 𝑥 ∈ ℝ → ( ℜ ‘ 𝑥 ) = 𝑥 )
6 5 breq2d ⊢ ( 𝑥 ∈ ℝ → ( 0 ≤ ( ℜ ‘ 𝑥 ) ↔ 0 ≤ 𝑥 ) )
7 6 biimpar ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → 0 ≤ ( ℜ ‘ 𝑥 ) )
8 7 adantrr ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 0 ≤ 𝑥 ∧ ( 𝑥 ↑ 2 ) = 𝐴 ) ) → 0 ≤ ( ℜ ‘ 𝑥 ) )
9 rennim ⊢ ( 𝑥 ∈ ℝ → ( i · 𝑥 ) ∉ ℝ+ )
10 9 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 0 ≤ 𝑥 ∧ ( 𝑥 ↑ 2 ) = 𝐴 ) ) → ( i · 𝑥 ) ∉ ℝ+ )
11 4 8 10 3jca ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 0 ≤ 𝑥 ∧ ( 𝑥 ↑ 2 ) = 𝐴 ) ) → ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
12 3 11 jca ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 0 ≤ 𝑥 ∧ ( 𝑥 ↑ 2 ) = 𝐴 ) ) → ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
13 12 reximi2 ⊢ ( ∃ 𝑥 ∈ ℝ ( 0 ≤ 𝑥 ∧ ( 𝑥 ↑ 2 ) = 𝐴 ) → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
14 1 13 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
15 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
16 15 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℂ )
17 sqrmo ⊢ ( 𝐴 ∈ ℂ → ∃* 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
18 16 17 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ∃* 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
19 reu5 ⊢ ( ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ ( ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ∧ ∃* 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
20 14 18 19 sylanbrc ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )