This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (A \in ℂ \land A \neq 0) \to \|A\| \in ℝ^{+}$

Proof

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