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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		absval	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) = ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) = ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) )
3		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
4	3	cjmulrcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ )
5	3	cjmulge0d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 0 ≤ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
6	3	cjcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
7		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐴 ≠ 0 )
8	3 7	cjne0d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ 𝐴 ) ≠ 0 )
9	3 6 7 8	mulne0d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ≠ 0 )
10	4 5 9	ne0gt0d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 0 < ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
11	4 10	elrpd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ+ )
12		rpsqrtcl	⊢ ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ+ → ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ∈ ℝ+ )
13	11 12	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ∈ ℝ+ )
14	2 13	eqeltrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )