Description: The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | rpsqrtcl | ⊢ ( 𝐴 ∈ ℝ+ → ( √ ‘ 𝐴 ) ∈ ℝ+ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpre | ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ ) | |
2 | rpge0 | ⊢ ( 𝐴 ∈ ℝ+ → 0 ≤ 𝐴 ) | |
3 | resqrtcl | ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℝ ) | |
4 | 1 2 3 | syl2anc | ⊢ ( 𝐴 ∈ ℝ+ → ( √ ‘ 𝐴 ) ∈ ℝ ) |
5 | rpgt0 | ⊢ ( 𝐴 ∈ ℝ+ → 0 < 𝐴 ) | |
6 | sqrtgt0 | ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 < ( √ ‘ 𝐴 ) ) | |
7 | 1 5 6 | syl2anc | ⊢ ( 𝐴 ∈ ℝ+ → 0 < ( √ ‘ 𝐴 ) ) |
8 | 4 7 | elrpd | ⊢ ( 𝐴 ∈ ℝ+ → ( √ ‘ 𝐴 ) ∈ ℝ+ ) |