Description: The square root function is one-to-one. (Contributed by Mario Carneiro, 29-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | resqrcld.1 | |- ( ph -> A e. RR ) |
|
resqrcld.2 | |- ( ph -> 0 <_ A ) |
||
sqr11d.3 | |- ( ph -> B e. RR ) |
||
sqr11d.4 | |- ( ph -> 0 <_ B ) |
||
sqrt11d.5 | |- ( ph -> ( sqrt ` A ) = ( sqrt ` B ) ) |
||
Assertion | sqr11d | |- ( ph -> A = B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resqrcld.1 | |- ( ph -> A e. RR ) |
|
2 | resqrcld.2 | |- ( ph -> 0 <_ A ) |
|
3 | sqr11d.3 | |- ( ph -> B e. RR ) |
|
4 | sqr11d.4 | |- ( ph -> 0 <_ B ) |
|
5 | sqrt11d.5 | |- ( ph -> ( sqrt ` A ) = ( sqrt ` B ) ) |
|
6 | sqrt11 | |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqrt ` A ) = ( sqrt ` B ) <-> A = B ) ) |
|
7 | 1 2 3 4 6 | syl22anc | |- ( ph -> ( ( sqrt ` A ) = ( sqrt ` B ) <-> A = B ) ) |
8 | 5 7 | mpbid | |- ( ph -> A = B ) |