Proof 01. 1 ⊢ x ∈ ℝ, hypo. 02. 2 ⊢ 0 ≤ x, hypo. 03. ⊢ 0 ∈ ℝ, calc. 04. 1, 2 ⊢ 0 - x ≤ x - x, rle_compat_sub 3 1 1 2. 05. 1 ⊢ 0 - x = -x, rsub_from_zero 1. 06. 1, 2 ⊢ -x ≤ x - x, eq_subst 5 4, P t ↔ t ≤ x - x. 07. ⊢ x - x = x + -x, rsub_eq. 08. 1 ⊢ x + -x = 0, radd_inv 1. 09. 1 ⊢ x - x = 0, eq_trans 7 8. 10. 1, 2 ⊢ -x ≤ 0, le_eq_trans 6 9. rneg_non_negative. ⊢ x ∈ ℝ → 0 ≤ x → -x ≤ 0, subj_intro_ii 10.
Dependencies
The given proof depends on seven axioms:
eq_refl, eq_subst, radd_comm, radd_inv, radd_neutr, rle_compat_add, rneg_closed.