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 ⊢ A ∈ ℝ → A ≤ A

Proof

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