Metamath Proof Explorer


Theorem sqrtneg

Description: The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013)

Ref Expression
Assertion sqrtneg A0AA=iA

Proof

Step Hyp Ref Expression
1 recn AA
2 1 adantr A0AA
3 2 negcld A0AA
4 sqrtval AA=ιx|x2=A0xix+
5 3 4 syl A0AA=ιx|x2=A0xix+
6 sqrtneglem A0AiA2=A0iAiiA+
7 ax-icn i
8 resqrtcl A0AA
9 8 recnd A0AA
10 mulcl iAiA
11 7 9 10 sylancr A0AiA
12 oveq1 x=iAx2=iA2
13 12 eqeq1d x=iAx2=AiA2=A
14 fveq2 x=iAx=iA
15 14 breq2d x=iA0x0iA
16 oveq2 x=iAix=iiA
17 neleq1 ix=iiAix+iiA+
18 16 17 syl x=iAix+iiA+
19 13 15 18 3anbi123d x=iAx2=A0xix+iA2=A0iAiiA+
20 19 rspcev iAiA2=A0iAiiA+xx2=A0xix+
21 11 6 20 syl2anc A0Axx2=A0xix+
22 sqrmo A*xx2=A0xix+
23 3 22 syl A0A*xx2=A0xix+
24 reu5 ∃!xx2=A0xix+xx2=A0xix+*xx2=A0xix+
25 21 23 24 sylanbrc A0A∃!xx2=A0xix+
26 19 riota2 iA∃!xx2=A0xix+iA2=A0iAiiA+ιx|x2=A0xix+=iA
27 11 25 26 syl2anc A0AiA2=A0iAiiA+ιx|x2=A0xix+=iA
28 6 27 mpbid A0Aιx|x2=A0xix+=iA
29 5 28 eqtrd A0AA=iA