rle_add

Theorem rle_add

Theorem. rle_add
a ∈ ℝ → b ∈ ℝ → a' ∈ ℝ → b' ∈ ℝ → a ≤ a' → b ≤ b' → a + b ≤ a' + b'

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ a' ∈ ℝ, hypo.
04. 4 ⊢ b' ∈ ℝ, hypo.
05. 5 ⊢ a ≤ a', hypo.
06. 6 ⊢ b ≤ b', hypo.
07. 1, 2, 3, 5 ⊢ a + b ≤ a' + b, rle_compat_add 1 3 2 5.
08. 2, 3, 4, 6 ⊢ a' + b ≤ a' + b', rle_compat_addl 2 4 3 6.
09. 1, 2 ⊢ a + b ∈ ℝ, radd_closed 1 2.
10. 2, 3 ⊢ a' + b ∈ ℝ, radd_closed 3 2.
11. 3, 4 ⊢ a' + b' ∈ ℝ, radd_closed 3 4.
12. 1, 2, 3, 4, 5, 6 ⊢ a + b ≤ a' + b', rle_trans 9 10 11 7 8.
13. 1, 2, 3, 4 ⊢ a ≤ a' → b ≤ b' → a + b ≤ a' + b', subj_intro_ii 12.
rle_add. ⊢ a ∈ ℝ → b ∈ ℝ → a' ∈ ℝ → b' ∈ ℝ →
  a ≤ a' → b ≤ b' → a + b ≤ a' + b', subj_intro_iv 13.

Dependencies
The given proof depends on five axioms:
eq_subst, radd_closed, radd_comm, rle_compat_add, rle_trans.