# Metamath Proof Explorer

## Theorem sqrtgt0

Description: The square root function is positive for positive input. (Contributed by Mario Carneiro, 10-Jul-2013) (Revised by Mario Carneiro, 6-Sep-2013)

Ref Expression
Assertion sqrtgt0 ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to 0<\sqrt{{A}}$

### Proof

Step Hyp Ref Expression
1 0re ${⊢}0\in ℝ$
2 ltle ${⊢}\left(0\in ℝ\wedge {A}\in ℝ\right)\to \left(0<{A}\to 0\le {A}\right)$
3 1 2 mpan ${⊢}{A}\in ℝ\to \left(0<{A}\to 0\le {A}\right)$
4 3 imp ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to 0\le {A}$
5 resqrtcl ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to \sqrt{{A}}\in ℝ$
6 4 5 syldan ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \sqrt{{A}}\in ℝ$
7 sqrtge0 ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to 0\le \sqrt{{A}}$
8 4 7 syldan ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to 0\le \sqrt{{A}}$
9 gt0ne0 ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to {A}\ne 0$
10 sq0i ${⊢}\sqrt{{A}}=0\to {\sqrt{{A}}}^{2}=0$
11 resqrtth ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to {\sqrt{{A}}}^{2}={A}$
12 4 11 syldan ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to {\sqrt{{A}}}^{2}={A}$
13 12 eqeq1d ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \left({\sqrt{{A}}}^{2}=0↔{A}=0\right)$
14 10 13 syl5ib ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \left(\sqrt{{A}}=0\to {A}=0\right)$
15 14 necon3d ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \left({A}\ne 0\to \sqrt{{A}}\ne 0\right)$
16 9 15 mpd ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \sqrt{{A}}\ne 0$
17 6 8 16 ne0gt0d ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to 0<\sqrt{{A}}$