# 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 ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to \exists !{x}\in ℂ\phantom{\rule{.4em}{0ex}}\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)$

### Proof

Step Hyp Ref Expression
1 resqrex ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left(0\le {x}\wedge {{x}}^{2}={A}\right)$
2 recn ${⊢}{x}\in ℝ\to {x}\in ℂ$
3 2 adantr ${⊢}\left({x}\in ℝ\wedge \left(0\le {x}\wedge {{x}}^{2}={A}\right)\right)\to {x}\in ℂ$
4 simprr ${⊢}\left({x}\in ℝ\wedge \left(0\le {x}\wedge {{x}}^{2}={A}\right)\right)\to {{x}}^{2}={A}$
5 rere ${⊢}{x}\in ℝ\to \Re \left({x}\right)={x}$
6 5 breq2d ${⊢}{x}\in ℝ\to \left(0\le \Re \left({x}\right)↔0\le {x}\right)$
7 6 biimpar ${⊢}\left({x}\in ℝ\wedge 0\le {x}\right)\to 0\le \Re \left({x}\right)$
8 7 adantrr ${⊢}\left({x}\in ℝ\wedge \left(0\le {x}\wedge {{x}}^{2}={A}\right)\right)\to 0\le \Re \left({x}\right)$
9 rennim ${⊢}{x}\in ℝ\to \mathrm{i}{x}\notin {ℝ}^{+}$
10 9 adantr ${⊢}\left({x}\in ℝ\wedge \left(0\le {x}\wedge {{x}}^{2}={A}\right)\right)\to \mathrm{i}{x}\notin {ℝ}^{+}$
11 4 8 10 3jca ${⊢}\left({x}\in ℝ\wedge \left(0\le {x}\wedge {{x}}^{2}={A}\right)\right)\to \left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)$
12 3 11 jca ${⊢}\left({x}\in ℝ\wedge \left(0\le {x}\wedge {{x}}^{2}={A}\right)\right)\to \left({x}\in ℂ\wedge \left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)$
13 12 reximi2 ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left(0\le {x}\wedge {{x}}^{2}={A}\right)\to \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)$
14 1 13 syl ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)$
15 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
16 15 adantr ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to {A}\in ℂ$
17 sqrmo ${⊢}{A}\in ℂ\to {\exists }^{*}{x}\in ℂ\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)$
18 16 17 syl ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to {\exists }^{*}{x}\in ℂ\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)$
19 reu5 ${⊢}\exists !{x}\in ℂ\phantom{\rule{.4em}{0ex}}\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)↔\left(\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\wedge {\exists }^{*}{x}\in ℂ\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)$
20 14 18 19 sylanbrc ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to \exists !{x}\in ℂ\phantom{\rule{.4em}{0ex}}\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)$