Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( A ^ 2 ) = ( A ^ 2 ) |
2 |
|
resqcl |
|- ( A e. RR -> ( A ^ 2 ) e. RR ) |
3 |
|
sqge0 |
|- ( A e. RR -> 0 <_ ( A ^ 2 ) ) |
4 |
2 3
|
jca |
|- ( A e. RR -> ( ( A ^ 2 ) e. RR /\ 0 <_ ( A ^ 2 ) ) ) |
5 |
4
|
adantr |
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( A ^ 2 ) e. RR /\ 0 <_ ( A ^ 2 ) ) ) |
6 |
|
sqrtsq2 |
|- ( ( ( ( A ^ 2 ) e. RR /\ 0 <_ ( A ^ 2 ) ) /\ ( A e. RR /\ 0 <_ A ) ) -> ( ( sqrt ` ( A ^ 2 ) ) = A <-> ( A ^ 2 ) = ( A ^ 2 ) ) ) |
7 |
5 6
|
mpancom |
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqrt ` ( A ^ 2 ) ) = A <-> ( A ^ 2 ) = ( A ^ 2 ) ) ) |
8 |
1 7
|
mpbiri |
|- ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` ( A ^ 2 ) ) = A ) |