Proof 01. 1 ⊢ x ∈ ℝ, hypo. 02. 1 ⊢ -x ∈ ℝ, rneg_closed 1. 03. 1 ⊢ -(-x) ∈ ℝ, rneg_closed 2. 04. 1 ⊢ -x + -(-x) = 0, radd_inv 2. 05. 1 ⊢ -(-x) + -x = -x + -(-x), radd_comm 3 2. 06. 1 ⊢ -(-x) + -x = 0, eq_trans 5 4. 07. 1 ⊢ -(-x) + -x + x = 0 + x, eq_cong 6, f t = t + x. 08. 1 ⊢ -(-x) + -x + x = -(-x) + (-x + x), radd_assoc 3 2 1. 09. 1 ⊢ -x + x = x + -x, radd_comm 2 1. 10. 1 ⊢ x + -x = 0, radd_inv 1. 11. 1 ⊢ -x + x = 0, eq_trans 9 10. 12. 1 ⊢ -(-x) + (-x + x) = -(-x) + 0, eq_cong 11, f t = -(-x) + t. 13. 1 ⊢ -(-x) + 0 = -(-x), radd_neutr 3. 14. 1 ⊢ -(-x) + (-x + x) = -(-x), eq_trans 12 13. 15. 1 ⊢ -(-x) + -x + x = -(-x), eq_trans 8 14. 16. 1 ⊢ -(-x) = 0 + x, eq_trans_ll 15 7. 17. 1 ⊢ 0 + x = x, radd_neutl 1. 18. 1 ⊢ -(-x) = x, eq_trans 16 17. rneg_involution. ⊢ x ∈ ℝ → -(-x) = x, subj_intro 18.
Dependencies
The given proof depends on seven axioms:
eq_refl, eq_subst, radd_assoc, radd_comm, radd_inv, radd_neutr, rneg_closed.