Theorem rabs_triangle_ineq

The "triangle inequality" for absolute values.

Proof sketch
In general, we have x ≤ |x| and y ≤ |y|, thus x + y ≤ |x| + |y|. Furthermore, in general, we have -x ≤ |x| and -y ≤ |y|, thus -|x| ≤ x and -|y| ≤ y, and therefore
  -(|x| + |y|) ≤ x + y.
Thus |x + y| ≤ |x| + |y| by rabs_bounded. q.e.d.

Proof
01. 1 ⊢ x ∈ ℝ, hypo.
02. 2 ⊢ y ∈ ℝ, hypo.
03. 1 ⊢ abs x ∈ ℝ, rabs_closed 1.
04. 2 ⊢ abs y ∈ ℝ, rabs_closed 2.
05. 1 ⊢ x ≤ abs x, rabs_ge_arg 1.
06. 2 ⊢ y ≤ abs y, rabs_ge_arg 2.
07. 1, 2 ⊢ x + y ≤ abs x + abs y, rle_add 1 2 3 4 5 6.
09. 1 ⊢ -x ≤ abs x, rabs_ge_neg_arg 1.
10. 2 ⊢ -y ≤ abs y, rabs_ge_neg_arg 2.
11. 1 ⊢ -x ∈ ℝ, rneg_closed 1.
12. 2 ⊢ -y ∈ ℝ, rneg_closed 2.
13. 1 ⊢ -abs x ≤ -(-x), rle_neg_swaps 11 3 9.
14. 2 ⊢ -abs y ≤ -(-y), rle_neg_swaps 12 4 10.
15. 1 ⊢ -(-x) = x, rneg_involution 1.
16. 2 ⊢ -(-y) = y, rneg_involution 2.
17. 1 ⊢ -abs x ≤ x, le_eq_trans 13 15.
18. 2 ⊢ -abs y ≤ y, le_eq_trans 14 16.
19. 1 ⊢ -abs x ∈ ℝ, rneg_closed 3.
20. 2 ⊢ -abs y ∈ ℝ, rneg_closed 4.
21. 1, 2 ⊢ -abs x + -abs y ≤ x + y, rle_add 19 20 1 2 17 18.
22. 1, 2 ⊢ -(abs x + abs y) = -abs x + -abs y, rneg_dist_add 3 4.
23. 1, 2 ⊢ -(abs x + abs y) ≤ x + y, eq_le_trans 22 21.
24. 1, 2 ⊢ abs x + abs y ∈ ℝ, radd_closed 3 4.
25. 1, 2 ⊢ x + y ∈ ℝ, radd_closed 1 2.
26. 1, 2 ⊢ abs (x + y) ≤ abs x + abs y, rabs_bounded 24 25 23 7.
rabs_triangle_ineq. ⊢ x ∈ ℝ → y ∈ ℝ →
  abs (x + y) ≤ abs x + abs y, subj_intro_ii 26.

Dependencies
The given proof depends on 20 axioms:
comp, efq, eq_refl, eq_subst, ext, lem, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rle_compat_add, rle_refl, rle_total, rle_trans, rmul_closed, rmul_comm, rmul_distl_add, rmul_neutr, rneg_closed.