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 ⊢ abs x ∈ ℝ, eq_subst_rev 4 1, P t ↔ t ∈ ℝ. 06. 6 ⊢ ¬0 ≤ x, hypo. 07. 1, 6 ⊢ abs x = -x, rabs_eqr 1 6. 08. 1 ⊢ -x ∈ ℝ, rneg_closed 1. 09. 1, 6 ⊢ abs x ∈ ℝ, eq_subst_rev 7 8, P t ↔ t ∈ ℝ. 10. 1 ⊢ abs x ∈ ℝ, disj_elim 2 5 9. rabs_closed. ⊢ x ∈ ℝ → abs x ∈ ℝ, subj_intro 10.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, rneg_closed.