Proof 01. 1 ⊢ x ∈ ℝ, hypo. 02. ⊢ 0 ≤ x ∨ ¬0 ≤ x, lem. 03. 3 ⊢ 0 ≤ x, hypo. 04. 1 ⊢ set x, set_intro 1. 05. 1, 3 ⊢ if (0 ≤ x) x (-x) = x, cond_eql 4 3. 06. ⊢ abs x = if (0 ≤ x) x (-x), abs_eq. 07. 1, 3 ⊢ abs x = x, eq_trans 6 5. 08. 1 ⊢ x ≤ x, rle_refl 1. 09. 1, 3 ⊢ x ≤ abs x, eq_subst_rev 7 8, P t ↔ x ≤ t. 10. 10 ⊢ ¬0 ≤ x, hypo. 11. 1 ⊢ -x ∈ ℝ, rneg_closed 1. 12. 1 ⊢ set (-x), set_intro 11. 13. 1, 10 ⊢ if (0 ≤ x) x (-x) = -x, cond_eqr 12 10. 14. 1, 10 ⊢ abs x = -x, eq_trans 6 13. 15. ⊢ 0 ∈ ℝ, calc. 16. 1, 10 ⊢ x ≤ 0, rle_neg 15 1 10. 17. 1, 10 ⊢ x + x ≤ 0 + 0, rle_add 1 1 15 15 16 16. 18. ⊢ 0 + 0 = 0, radd_neutr 15. 19. 1, 10 ⊢ x + x ≤ 0, le_eq_trans 17 18. 20. 1 ⊢ x + x ∈ ℝ, radd_closed 1 1. 21. 1, 10 ⊢ x + x - x ≤ 0 - x, rle_compat_sub 20 15 1 19. 22. 1 ⊢ x + x - x = x, radd_cancel 1 1. 23. 1, 10 ⊢ x ≤ 0 - x, eq_subst 22 21, P t ↔ t ≤ 0 - x. 24. 1 ⊢ 0 - x = -x, rsub_from_zero 1. 25. 1, 10 ⊢ x ≤ -x, le_eq_trans 23 24. 26. 1, 10 ⊢ x ≤ abs x, eq_subst_rev 14 25, P t ↔ x ≤ t. 27. 1 ⊢ x ≤ abs x, disj_elim 2 9 26. rabs_ge_arg. ⊢ x ∈ ℝ → x ≤ abs x, subj_intro 27.
Dependencies
The given proof depends on 16 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, rneg_closed.