Description: Existence and uniqueness for the real square root function. (Contributed by Mario Carneiro, 9-Jul-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | resqreu | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resqrex | |
|
2 | recn | |
|
3 | 2 | adantr | |
4 | simprr | |
|
5 | rere | |
|
6 | 5 | breq2d | |
7 | 6 | biimpar | |
8 | 7 | adantrr | |
9 | rennim | |
|
10 | 9 | adantr | |
11 | 4 8 10 | 3jca | |
12 | 3 11 | jca | |
13 | 12 | reximi2 | |
14 | 1 13 | syl | |
15 | recn | |
|
16 | 15 | adantr | |
17 | sqrmo | |
|
18 | 16 17 | syl | |
19 | reu5 | |
|
20 | 14 18 19 | sylanbrc | |