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

Metamath Proof Explorer

Theorem leabs

Description: A real number is less than or equal to its absolute value. (Contributed by NM, 27-Feb-2005)

Ref Expression
Assertion leabs ( 𝐴 ∈ ℝ → 𝐴 ≤ ( abs ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 0red ⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
2 id ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
3 absid ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( abs ‘ 𝐴 ) = 𝐴 )
4 eqcom ⊢ ( ( abs ‘ 𝐴 ) = 𝐴 ↔ 𝐴 = ( abs ‘ 𝐴 ) )
5 eqle ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 = ( abs ‘ 𝐴 ) ) → 𝐴 ≤ ( abs ‘ 𝐴 ) )
6 4 5 sylan2b ⊢ ( ( 𝐴 ∈ ℝ ∧ ( abs ‘ 𝐴 ) = 𝐴 ) → 𝐴 ≤ ( abs ‘ 𝐴 ) )
7 3 6 syldan ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ≤ ( abs ‘ 𝐴 ) )
8 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
9 absge0 ⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( abs ‘ 𝐴 ) )
10 8 9 syl ⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( abs ‘ 𝐴 ) )
11 abscl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
12 8 11 syl ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) ∈ ℝ )
13 0re ⊢ 0 ∈ ℝ
14 letr ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ∧ ( abs ‘ 𝐴 ) ∈ ℝ ) → ( ( 𝐴 ≤ 0 ∧ 0 ≤ ( abs ‘ 𝐴 ) ) → 𝐴 ≤ ( abs ‘ 𝐴 ) ) )
15 13 14 mp3an2 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( abs ‘ 𝐴 ) ∈ ℝ ) → ( ( 𝐴 ≤ 0 ∧ 0 ≤ ( abs ‘ 𝐴 ) ) → 𝐴 ≤ ( abs ‘ 𝐴 ) ) )
16 12 15 mpdan ⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 ≤ 0 ∧ 0 ≤ ( abs ‘ 𝐴 ) ) → 𝐴 ≤ ( abs ‘ 𝐴 ) ) )
17 10 16 mpan2d ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ≤ 0 → 𝐴 ≤ ( abs ‘ 𝐴 ) ) )
18 17 imp ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) → 𝐴 ≤ ( abs ‘ 𝐴 ) )
19 1 2 7 18 lecasei ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ ( abs ‘ 𝐴 ) )