Proof 01. 1 ⊢ x ∈ ℝ, hypo. 02. 2 ⊢ ¬0 ≤ x, hypo. 03. 1 ⊢ -x ∈ ℝ, rneg_closed 1. 04. 1 ⊢ set (-x), set_intro 3. 05. 1, 2 ⊢ if (0 ≤ x) x (-x) = -x, cond_eqr 4 2. 06. ⊢ abs x = if (0 ≤ x) x (-x), abs_eq. 07. 1, 2 ⊢ abs x = -x, eq_trans 6 5. rabs_eqr. ⊢ x ∈ ℝ → ¬0 ≤ x → abs x = -x, subj_intro_ii 7.
Dependencies
The given proof depends on six axioms:
comp, efq, eq_refl, eq_subst, ext, rneg_closed.