rle_lt_trans

Theorem rle_lt_trans

Theorem. rle_lt_trans
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a ≤ b → b < c → a < c

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ c ∈ ℝ, hypo.
04. 4 ⊢ a ≤ b, hypo.
05. 5 ⊢ b < c, hypo.
06. 5 ⊢ b ≤ c, le_from_lt 5.
07. 1, 2, 3, 4, 5 ⊢ a ≤ c, rle_trans 1 2 3 4 6.
08. 8 ⊢ a = c, hypo.
09. 5, 8 ⊢ b < a, eq_subst_rev 8 5, P t ↔ b < t.
10. 5, 8 ⊢ b ≤ a, le_from_lt 9.
11. 1, 2, 4, 5, 8 ⊢ a = b, rle_antisym 1 2 4 10.
12. 5, 8 ⊢ ¬b = a, neq_from_lt 9.
13. 5, 8 ⊢ ¬a = b, neq_symm 12.
14. 1, 2, 4, 5, 8 ⊢ ⊥, neg_elim 13 11.
15. 1, 2, 4, 5 ⊢ ¬a = c, neg_intro 14.
16. 1, 2, 3, 4, 5 ⊢ a < c, lt_intro 7 15.
17. 1, 2, 3 ⊢ a ≤ b → b < c → a < c, subj_intro_ii 16.
rle_lt_trans. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  a ≤ b → b < c → a < c, subj_intro_iii 17.

Dependencies
The given proof depends on four axioms:
eq_refl, eq_subst, rle_antisym, rle_trans.