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