Proof 01. 1 ⊢ x ∈ ℝ, hypo. 02. ⊢ 0 ≤ x ∨ ¬0 ≤ x, lem. 03. 3 ⊢ 0 ≤ x, hypo. 04. 1, 3 ⊢ abs x = x, rabs_eql 1 3. 05. 1, 3 ⊢ -x ≤ 0, rneg_non_negative 1 3. 06. ⊢ 0 ∈ ℝ, calc. 07. 1 ⊢ -x ∈ ℝ, rneg_closed 1. 08. 1, 3 ⊢ -x ≤ x, rle_trans 7 6 1 5 3. 09. 1, 3 ⊢ -x ≤ abs x, eq_subst_rev 4 8, P t ↔ -x ≤ t. 10. 10 ⊢ ¬0 ≤ x, hypo. 11. 1, 10 ⊢ abs x = -x, rabs_eqr 1 10. 12. 1 ⊢ -x ≤ -x, rle_refl 7. 13. 1, 10 ⊢ -x ≤ abs x, eq_subst_rev 11 12, P t ↔ -x ≤ t. 14. 1 ⊢ -x ≤ abs x, disj_elim 2 9 13. rabs_ge_neg_arg. ⊢ x ∈ ℝ → -x ≤ abs x, subj_intro 14.
Dependencies
The given proof depends on 13 axioms:
comp, efq, eq_refl, eq_subst, ext, lem, radd_comm, radd_inv, radd_neutr, rle_compat_add, rle_refl, rle_trans, rneg_closed.