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 ‘ 𝐴 ) )