# Metamath Proof Explorer

## Theorem resqrtcl

Description: Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013)

Ref Expression
Assertion resqrtcl ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to \sqrt{{A}}\in ℝ$

### Proof

Step Hyp Ref Expression
1 resqrex ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left(0\le {y}\wedge {{y}}^{2}={A}\right)$
2 simp1l ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {y}\in ℝ\wedge \left(0\le {y}\wedge {{y}}^{2}={A}\right)\right)\to {A}\in ℝ$
3 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
4 sqrtval ${⊢}{A}\in ℂ\to \sqrt{{A}}=\left(\iota {x}\in ℂ|\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)$
5 2 3 4 3syl ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {y}\in ℝ\wedge \left(0\le {y}\wedge {{y}}^{2}={A}\right)\right)\to \sqrt{{A}}=\left(\iota {x}\in ℂ|\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)$
6 simp3r ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {y}\in ℝ\wedge \left(0\le {y}\wedge {{y}}^{2}={A}\right)\right)\to {{y}}^{2}={A}$
7 simp3l ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {y}\in ℝ\wedge \left(0\le {y}\wedge {{y}}^{2}={A}\right)\right)\to 0\le {y}$
8 rere ${⊢}{y}\in ℝ\to \Re \left({y}\right)={y}$
9 8 3ad2ant2 ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {y}\in ℝ\wedge \left(0\le {y}\wedge {{y}}^{2}={A}\right)\right)\to \Re \left({y}\right)={y}$
10 7 9 breqtrrd ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {y}\in ℝ\wedge \left(0\le {y}\wedge {{y}}^{2}={A}\right)\right)\to 0\le \Re \left({y}\right)$
11 rennim ${⊢}{y}\in ℝ\to \mathrm{i}{y}\notin {ℝ}^{+}$
12 11 3ad2ant2 ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {y}\in ℝ\wedge \left(0\le {y}\wedge {{y}}^{2}={A}\right)\right)\to \mathrm{i}{y}\notin {ℝ}^{+}$
13 6 10 12 3jca ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {y}\in ℝ\wedge \left(0\le {y}\wedge {{y}}^{2}={A}\right)\right)\to \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)$
14 recn ${⊢}{y}\in ℝ\to {y}\in ℂ$
15 14 3ad2ant2 ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {y}\in ℝ\wedge \left(0\le {y}\wedge {{y}}^{2}={A}\right)\right)\to {y}\in ℂ$
16 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)$
17 16 3ad2ant1 ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {y}\in ℝ\wedge \left(0\le {y}\wedge {{y}}^{2}={A}\right)\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)$
18 oveq1 ${⊢}{x}={y}\to {{x}}^{2}={{y}}^{2}$
19 18 eqeq1d ${⊢}{x}={y}\to \left({{x}}^{2}={A}↔{{y}}^{2}={A}\right)$
20 fveq2 ${⊢}{x}={y}\to \Re \left({x}\right)=\Re \left({y}\right)$
21 20 breq2d ${⊢}{x}={y}\to \left(0\le \Re \left({x}\right)↔0\le \Re \left({y}\right)\right)$
22 oveq2 ${⊢}{x}={y}\to \mathrm{i}{x}=\mathrm{i}{y}$
23 neleq1 ${⊢}\mathrm{i}{x}=\mathrm{i}{y}\to \left(\mathrm{i}{x}\notin {ℝ}^{+}↔\mathrm{i}{y}\notin {ℝ}^{+}\right)$
24 22 23 syl ${⊢}{x}={y}\to \left(\mathrm{i}{x}\notin {ℝ}^{+}↔\mathrm{i}{y}\notin {ℝ}^{+}\right)$
25 19 21 24 3anbi123d ${⊢}{x}={y}\to \left(\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)↔\left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)$
26 25 riota2 ${⊢}\left({y}\in ℂ\wedge \exists !{x}\in ℂ\phantom{\rule{.4em}{0ex}}\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)\to \left(\left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)↔\left(\iota {x}\in ℂ|\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)={y}\right)$
27 15 17 26 syl2anc ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {y}\in ℝ\wedge \left(0\le {y}\wedge {{y}}^{2}={A}\right)\right)\to \left(\left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)↔\left(\iota {x}\in ℂ|\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)={y}\right)$
28 13 27 mpbid ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {y}\in ℝ\wedge \left(0\le {y}\wedge {{y}}^{2}={A}\right)\right)\to \left(\iota {x}\in ℂ|\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)={y}$
29 5 28 eqtrd ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {y}\in ℝ\wedge \left(0\le {y}\wedge {{y}}^{2}={A}\right)\right)\to \sqrt{{A}}={y}$
30 simp2 ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {y}\in ℝ\wedge \left(0\le {y}\wedge {{y}}^{2}={A}\right)\right)\to {y}\in ℝ$
31 29 30 eqeltrd ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {y}\in ℝ\wedge \left(0\le {y}\wedge {{y}}^{2}={A}\right)\right)\to \sqrt{{A}}\in ℝ$
32 31 rexlimdv3a ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to \left(\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left(0\le {y}\wedge {{y}}^{2}={A}\right)\to \sqrt{{A}}\in ℝ\right)$
33 1 32 mpd ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to \sqrt{{A}}\in ℝ$