Theorem absrpcl

Description: The absolute value of a nonzero number is a positive real. (Contributed by FL, 27-Dec-2007) (Proof shortened by Mario Carneiro, 29-May-2016)

	Ref	Expression
Assertion	absrpcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		absval	$$⊢A\in ℂ\to \left|A\right|=\sqrt{A\bar{A}}$$
2	1	adantr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|=\sqrt{A\bar{A}}$$
3		simpl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to A\in ℂ$$
4	3	cjmulrcld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to A\bar{A}\in ℝ$$
5	3	cjmulge0d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to 0\le A\bar{A}$$
6	3	cjcld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \bar{A}\in ℂ$$
7		simpr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to A\ne 0$$
8	3 7	cjne0d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \bar{A}\ne 0$$
9	3 6 7 8	mulne0d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to A\bar{A}\ne 0$$
10	4 5 9	ne0gt0d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to 0<A\bar{A}$$
11	4 10	elrpd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to A\bar{A}\in {ℝ}^{+}$$
12		rpsqrtcl	$$⊢A\bar{A}\in {ℝ}^{+}\to \sqrt{A\bar{A}}\in {ℝ}^{+}$$
13	11 12	syl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \sqrt{A\bar{A}}\in {ℝ}^{+}$$
14	2 13	eqeltrd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\in {ℝ}^{+}$$