# Metamath Proof Explorer

## Theorem resqrtthlem

Description: Lemma for resqrtth . (Contributed by Mario Carneiro, 9-Jul-2013)

Ref Expression
Assertion resqrtthlem ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to \left({\sqrt{{A}}}^{2}={A}\wedge 0\le \Re \left(\sqrt{{A}}\right)\wedge \mathrm{i}\sqrt{{A}}\notin {ℝ}^{+}\right)$

### Proof

Step Hyp Ref Expression
1 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
2 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)$
3 2 eqcomd ${⊢}{A}\in ℂ\to \left(\iota {x}\in ℂ|\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)=\sqrt{{A}}$
4 1 3 syl ${⊢}{A}\in ℝ\to \left(\iota {x}\in ℂ|\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)=\sqrt{{A}}$
5 4 adantr ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to \left(\iota {x}\in ℂ|\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)=\sqrt{{A}}$
6 resqrtcl ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to \sqrt{{A}}\in ℝ$
7 6 recnd ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to \sqrt{{A}}\in ℂ$
8 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)$
9 oveq1 ${⊢}{x}=\sqrt{{A}}\to {{x}}^{2}={\sqrt{{A}}}^{2}$
10 9 eqeq1d ${⊢}{x}=\sqrt{{A}}\to \left({{x}}^{2}={A}↔{\sqrt{{A}}}^{2}={A}\right)$
11 fveq2 ${⊢}{x}=\sqrt{{A}}\to \Re \left({x}\right)=\Re \left(\sqrt{{A}}\right)$
12 11 breq2d ${⊢}{x}=\sqrt{{A}}\to \left(0\le \Re \left({x}\right)↔0\le \Re \left(\sqrt{{A}}\right)\right)$
13 oveq2 ${⊢}{x}=\sqrt{{A}}\to \mathrm{i}{x}=\mathrm{i}\sqrt{{A}}$
14 neleq1 ${⊢}\mathrm{i}{x}=\mathrm{i}\sqrt{{A}}\to \left(\mathrm{i}{x}\notin {ℝ}^{+}↔\mathrm{i}\sqrt{{A}}\notin {ℝ}^{+}\right)$
15 13 14 syl ${⊢}{x}=\sqrt{{A}}\to \left(\mathrm{i}{x}\notin {ℝ}^{+}↔\mathrm{i}\sqrt{{A}}\notin {ℝ}^{+}\right)$
16 10 12 15 3anbi123d ${⊢}{x}=\sqrt{{A}}\to \left(\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)↔\left({\sqrt{{A}}}^{2}={A}\wedge 0\le \Re \left(\sqrt{{A}}\right)\wedge \mathrm{i}\sqrt{{A}}\notin {ℝ}^{+}\right)\right)$
17 16 riota2 ${⊢}\left(\sqrt{{A}}\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({\sqrt{{A}}}^{2}={A}\wedge 0\le \Re \left(\sqrt{{A}}\right)\wedge \mathrm{i}\sqrt{{A}}\notin {ℝ}^{+}\right)↔\left(\iota {x}\in ℂ|\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)=\sqrt{{A}}\right)$
18 7 8 17 syl2anc ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to \left(\left({\sqrt{{A}}}^{2}={A}\wedge 0\le \Re \left(\sqrt{{A}}\right)\wedge \mathrm{i}\sqrt{{A}}\notin {ℝ}^{+}\right)↔\left(\iota {x}\in ℂ|\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)=\sqrt{{A}}\right)$
19 5 18 mpbird ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to \left({\sqrt{{A}}}^{2}={A}\wedge 0\le \Re \left(\sqrt{{A}}\right)\wedge \mathrm{i}\sqrt{{A}}\notin {ℝ}^{+}\right)$