Metamath Proof Explorer

Theorem sqrtmsq

Description: Square root of square. (Contributed by NM, 2-Aug-1999) (Revised by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion sqrtmsq 
|- ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` ( A x. A ) ) = A )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> A e. RR )
2 1 recnd 
 |-  ( ( A e. RR /\ 0 <_ A ) -> A e. CC )
3 2 sqvald 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( A ^ 2 ) = ( A x. A ) )
4 3 fveq2d 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` ( A ^ 2 ) ) = ( sqrt ` ( A x. A ) ) )
5 sqrtsq 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` ( A ^ 2 ) ) = A )
6 4 5 eqtr3d 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` ( A x. A ) ) = A )