# Metamath Proof Explorer

## Theorem sqrmo

Description: Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013) (Revised by NM, 17-Jun-2017)

Ref Expression
Assertion sqrmo ${⊢}{A}\in ℂ\to {\exists }^{*}{x}\in ℂ\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)$

### Proof

Step Hyp Ref Expression
1 simplr1 ${⊢}\left(\left({x}\in ℂ\wedge \left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)\wedge \left({y}\in ℂ\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\right)\to {{x}}^{2}={A}$
2 simprr1 ${⊢}\left(\left({x}\in ℂ\wedge \left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)\wedge \left({y}\in ℂ\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\right)\to {{y}}^{2}={A}$
3 1 2 eqtr4d ${⊢}\left(\left({x}\in ℂ\wedge \left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)\wedge \left({y}\in ℂ\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\right)\to {{x}}^{2}={{y}}^{2}$
4 sqeqor ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to \left({{x}}^{2}={{y}}^{2}↔\left({x}={y}\vee {x}=-{y}\right)\right)$
5 4 ad2ant2r ${⊢}\left(\left({x}\in ℂ\wedge \left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)\wedge \left({y}\in ℂ\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\right)\to \left({{x}}^{2}={{y}}^{2}↔\left({x}={y}\vee {x}=-{y}\right)\right)$
6 3 5 mpbid ${⊢}\left(\left({x}\in ℂ\wedge \left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)\wedge \left({y}\in ℂ\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\right)\to \left({x}={y}\vee {x}=-{y}\right)$
7 6 ord ${⊢}\left(\left({x}\in ℂ\wedge \left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)\wedge \left({y}\in ℂ\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\right)\to \left(¬{x}={y}\to {x}=-{y}\right)$
8 3simpc ${⊢}\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\to \left(0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)$
9 fveq2 ${⊢}{x}=-{y}\to \Re \left({x}\right)=\Re \left(-{y}\right)$
10 9 breq2d ${⊢}{x}=-{y}\to \left(0\le \Re \left({x}\right)↔0\le \Re \left(-{y}\right)\right)$
11 oveq2 ${⊢}{x}=-{y}\to \mathrm{i}{x}=\mathrm{i}\left(-{y}\right)$
12 neleq1 ${⊢}\mathrm{i}{x}=\mathrm{i}\left(-{y}\right)\to \left(\mathrm{i}{x}\notin {ℝ}^{+}↔\mathrm{i}\left(-{y}\right)\notin {ℝ}^{+}\right)$
13 11 12 syl ${⊢}{x}=-{y}\to \left(\mathrm{i}{x}\notin {ℝ}^{+}↔\mathrm{i}\left(-{y}\right)\notin {ℝ}^{+}\right)$
14 10 13 anbi12d ${⊢}{x}=-{y}\to \left(\left(0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)↔\left(0\le \Re \left(-{y}\right)\wedge \mathrm{i}\left(-{y}\right)\notin {ℝ}^{+}\right)\right)$
15 8 14 syl5ibcom ${⊢}\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\to \left({x}=-{y}\to \left(0\le \Re \left(-{y}\right)\wedge \mathrm{i}\left(-{y}\right)\notin {ℝ}^{+}\right)\right)$
16 15 ad2antlr ${⊢}\left(\left({x}\in ℂ\wedge \left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)\wedge \left({y}\in ℂ\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\right)\to \left({x}=-{y}\to \left(0\le \Re \left(-{y}\right)\wedge \mathrm{i}\left(-{y}\right)\notin {ℝ}^{+}\right)\right)$
17 7 16 syld ${⊢}\left(\left({x}\in ℂ\wedge \left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)\wedge \left({y}\in ℂ\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\right)\to \left(¬{x}={y}\to \left(0\le \Re \left(-{y}\right)\wedge \mathrm{i}\left(-{y}\right)\notin {ℝ}^{+}\right)\right)$
18 negeq ${⊢}{y}=0\to -{y}=-0$
19 neg0 ${⊢}-0=0$
20 18 19 syl6eq ${⊢}{y}=0\to -{y}=0$
21 20 eqeq2d ${⊢}{y}=0\to \left({x}=-{y}↔{x}=0\right)$
22 eqeq2 ${⊢}{y}=0\to \left({x}={y}↔{x}=0\right)$
23 21 22 bitr4d ${⊢}{y}=0\to \left({x}=-{y}↔{x}={y}\right)$
24 23 biimpcd ${⊢}{x}=-{y}\to \left({y}=0\to {x}={y}\right)$
25 24 necon3bd ${⊢}{x}=-{y}\to \left(¬{x}={y}\to {y}\ne 0\right)$
26 7 25 syli ${⊢}\left(\left({x}\in ℂ\wedge \left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)\wedge \left({y}\in ℂ\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\right)\to \left(¬{x}={y}\to {y}\ne 0\right)$
27 3simpc ${⊢}\left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\to \left(0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)$
28 cnpart ${⊢}\left({y}\in ℂ\wedge {y}\ne 0\right)\to \left(\left(0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)↔¬\left(0\le \Re \left(-{y}\right)\wedge \mathrm{i}\left(-{y}\right)\notin {ℝ}^{+}\right)\right)$
29 27 28 syl5ib ${⊢}\left({y}\in ℂ\wedge {y}\ne 0\right)\to \left(\left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\to ¬\left(0\le \Re \left(-{y}\right)\wedge \mathrm{i}\left(-{y}\right)\notin {ℝ}^{+}\right)\right)$
30 29 impancom ${⊢}\left({y}\in ℂ\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\to \left({y}\ne 0\to ¬\left(0\le \Re \left(-{y}\right)\wedge \mathrm{i}\left(-{y}\right)\notin {ℝ}^{+}\right)\right)$
31 30 adantl ${⊢}\left(\left({x}\in ℂ\wedge \left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)\wedge \left({y}\in ℂ\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\right)\to \left({y}\ne 0\to ¬\left(0\le \Re \left(-{y}\right)\wedge \mathrm{i}\left(-{y}\right)\notin {ℝ}^{+}\right)\right)$
32 26 31 syld ${⊢}\left(\left({x}\in ℂ\wedge \left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)\wedge \left({y}\in ℂ\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\right)\to \left(¬{x}={y}\to ¬\left(0\le \Re \left(-{y}\right)\wedge \mathrm{i}\left(-{y}\right)\notin {ℝ}^{+}\right)\right)$
33 17 32 pm2.65d ${⊢}\left(\left({x}\in ℂ\wedge \left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)\wedge \left({y}\in ℂ\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\right)\to ¬¬{x}={y}$
34 33 notnotrd ${⊢}\left(\left({x}\in ℂ\wedge \left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\right)\wedge \left({y}\in ℂ\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\right)\to {x}={y}$
35 34 an4s ${⊢}\left(\left({x}\in ℂ\wedge {y}\in ℂ\right)\wedge \left(\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\right)\to {x}={y}$
36 35 ex ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to \left(\left(\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\to {x}={y}\right)$
37 36 a1i ${⊢}{A}\in ℂ\to \left(\left({x}\in ℂ\wedge {y}\in ℂ\right)\to \left(\left(\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\to {x}={y}\right)\right)$
38 37 ralrimivv ${⊢}{A}\in ℂ\to \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left(\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\to {x}={y}\right)$
39 oveq1 ${⊢}{x}={y}\to {{x}}^{2}={{y}}^{2}$
40 39 eqeq1d ${⊢}{x}={y}\to \left({{x}}^{2}={A}↔{{y}}^{2}={A}\right)$
41 fveq2 ${⊢}{x}={y}\to \Re \left({x}\right)=\Re \left({y}\right)$
42 41 breq2d ${⊢}{x}={y}\to \left(0\le \Re \left({x}\right)↔0\le \Re \left({y}\right)\right)$
43 oveq2 ${⊢}{x}={y}\to \mathrm{i}{x}=\mathrm{i}{y}$
44 neleq1 ${⊢}\mathrm{i}{x}=\mathrm{i}{y}\to \left(\mathrm{i}{x}\notin {ℝ}^{+}↔\mathrm{i}{y}\notin {ℝ}^{+}\right)$
45 43 44 syl ${⊢}{x}={y}\to \left(\mathrm{i}{x}\notin {ℝ}^{+}↔\mathrm{i}{y}\notin {ℝ}^{+}\right)$
46 40 42 45 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)$
47 46 rmo4 ${⊢}{\exists }^{*}{x}\in ℂ\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)↔\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left(\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)\wedge \left({{y}}^{2}={A}\wedge 0\le \Re \left({y}\right)\wedge \mathrm{i}{y}\notin {ℝ}^{+}\right)\right)\to {x}={y}\right)$
48 38 47 sylibr ${⊢}{A}\in ℂ\to {\exists }^{*}{x}\in ℂ\left({{x}}^{2}={A}\wedge 0\le \Re \left({x}\right)\wedge \mathrm{i}{x}\notin {ℝ}^{+}\right)$