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