Description: The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | sqrtneg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recn | |
|
2 | 1 | adantr | |
3 | 2 | negcld | |
4 | sqrtval | |
|
5 | 3 4 | syl | |
6 | sqrtneglem | |
|
7 | ax-icn | |
|
8 | resqrtcl | |
|
9 | 8 | recnd | |
10 | mulcl | |
|
11 | 7 9 10 | sylancr | |
12 | oveq1 | |
|
13 | 12 | eqeq1d | |
14 | fveq2 | |
|
15 | 14 | breq2d | |
16 | oveq2 | |
|
17 | neleq1 | |
|
18 | 16 17 | syl | |
19 | 13 15 18 | 3anbi123d | |
20 | 19 | rspcev | |
21 | 11 6 20 | syl2anc | |
22 | sqrmo | |
|
23 | 3 22 | syl | |
24 | reu5 | |
|
25 | 21 23 24 | sylanbrc | |
26 | 19 | riota2 | |
27 | 11 25 26 | syl2anc | |
28 | 6 27 | mpbid | |
29 | 5 28 | eqtrd | |