Description: The square root function is one-to-one. (Contributed by NM, 27-Jul-1999)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sqrtthi.1 | |- A e. RR |
|
sqr11.1 | |- B e. RR |
||
Assertion | sqrt11i | |- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( sqrt ` A ) = ( sqrt ` B ) <-> A = B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sqrtthi.1 | |- A e. RR |
|
2 | sqr11.1 | |- B e. RR |
|
3 | sqrt11 | |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqrt ` A ) = ( sqrt ` B ) <-> A = B ) ) |
|
4 | 2 3 | mpanr1 | |- ( ( ( A e. RR /\ 0 <_ A ) /\ 0 <_ B ) -> ( ( sqrt ` A ) = ( sqrt ` B ) <-> A = B ) ) |
5 | 1 4 | mpanl1 | |- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( sqrt ` A ) = ( sqrt ` B ) <-> A = B ) ) |