Theorem rabs_bounded

From -a ≤ x ≤ a it follows that |x| ≤ a.

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ x ∈ ℝ, hypo.
03. 3 ⊢ -a ≤ x, hypo.
04. 4 ⊢ x ≤ a, hypo.
05. ⊢ 0 ≤ x ∨ ¬0 ≤ x, lem.
06. 6 ⊢ 0 ≤ x, hypo.
07. 2, 6 ⊢ abs x = x, rabs_eql 2 6.
08. 2, 4, 6 ⊢ abs x ≤ a, eq_le_trans 7 4.
09. 9 ⊢ ¬0 ≤ x, hypo.
10. 2, 9 ⊢ abs x = -x, rabs_eqr 2 9.
11. 1 ⊢ -a ∈ ℝ, rneg_closed 1.
12. 1, 2, 3 ⊢ -x ≤ -(-a), rle_neg_swaps 11 2 3.
13. 1 ⊢ -(-a) = a, rneg_involution 1.
14. 1, 2, 3 ⊢ -x ≤ a, le_eq_trans 12 13.
15. 1, 2, 3, 9 ⊢ abs x ≤ a, eq_le_trans 10 14.
16. 1, 2, 3, 4 ⊢ abs x ≤ a, disj_elim 5 8 15.
rabs_bounded. ⊢ a ∈ ℝ → x ∈ ℝ → -a ≤ x → x ≤ a →
  abs x ≤ a, subj_intro_iv 16.

Dependencies
The given proof depends on 13 axioms:
comp, efq, eq_refl, eq_subst, ext, lem, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rle_compat_add, rneg_closed.