Theorem sqrtmsq

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

	Ref	Expression
Assertion	sqrtmsq	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ ( 𝐴 · 𝐴 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
2	1	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℂ )
3	2	sqvald	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
4	3	fveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ ( 𝐴 ↑ 2 ) ) = ( √ ‘ ( 𝐴 · 𝐴 ) ) )
5		sqrtsq	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ ( 𝐴 ↑ 2 ) ) = 𝐴 )
6	4 5	eqtr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ ( 𝐴 · 𝐴 ) ) = 𝐴 )