Theorem sqrtsq

Description: Square root of square. (Contributed by NM, 14-Jan-2006) (Revised by Mario Carneiro, 29-May-2016)

	Ref	Expression
Assertion	sqrtsq	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ ( 𝐴 ↑ 2 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 )
2		resqcl	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ↑ 2 ) ∈ ℝ )
3		sqge0	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( 𝐴 ↑ 2 ) )
4	2 3	jca	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 ↑ 2 ) ) )
5	4	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝐴 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 ↑ 2 ) ) )
6		sqrtsq2	⊢ ( ( ( ( 𝐴 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 ↑ 2 ) ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( ( √ ‘ ( 𝐴 ↑ 2 ) ) = 𝐴 ↔ ( 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 ) ) )
7	5 6	mpancom	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( √ ‘ ( 𝐴 ↑ 2 ) ) = 𝐴 ↔ ( 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 ) ) )
8	1 7	mpbiri	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ ( 𝐴 ↑ 2 ) ) = 𝐴 )