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 ⊢ A ∈ ℝ ∧ 0 ≤ A → ∃! x ∈ ℂ x 2 = A ∧ 0 ≤ ℜ ⁡ x ∧ i ⁢ x ∉ ℝ +

Proof

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