Metamath Proof Explorer
Description: Square root theorem over the reals. Theorem I.35 of Apostol p. 29.
(Contributed by Mario Carneiro, 9Jul2013)


Ref 
Expression 

Assertion 
resqrtth 
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

resqrtthlem 
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( √ ‘ 𝐴 ) ) ∧ ( i · ( √ ‘ 𝐴 ) ) ∉ ℝ^{+} ) ) 
2 
1

simp1d 
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 ) 