Proof 01. 1 ⊢ x ∈ ℝ, hypo. 02. ⊢ 1 ∈ ℝ, calc. 03. ⊢ -1 ∈ ℝ, rneg_closed 2. 04. ⊢ -1 + 1 = 0, calc. 05. ⊢ (-1 + 1)⋅x = 0⋅x, eq_cong 4, f t = t⋅x. 06. 1 ⊢ (-1 + 1)⋅x = (-1)⋅x + 1⋅x, rmul_distr_add 3 2 1. 07. 1 ⊢ (-1)⋅x + 1⋅x = 0⋅x, eq_trans_ll 6 5. 08. 1 ⊢ 1⋅x = x, rmul_neutl 1. 09. 1 ⊢ (-1)⋅x + x = 0⋅x, eq_subst 8 7, P t ↔ (-1)⋅x + t = 0⋅x. 10. 1 ⊢ 0⋅x = 0, rmul_lzero 1. 11. 1 ⊢ (-1)⋅x + x = 0, eq_trans 9 10. 12. 1 ⊢ (-1)⋅x + x - x = 0 - x, eq_cong 11, f t = t - x. 13. 1 ⊢ (-1)⋅x ∈ ℝ, rmul_closed 3 1. 14. 1 ⊢ (-1)⋅x + x - x = (-1)⋅x, radd_cancel 13 1. 15. 1 ⊢ (-1)⋅x = 0 - x, eq_trans_ll 14 12. 16. 1 ⊢ 0 - x = -x, rsub_from_zero 1. 17. 1 ⊢ (-1)⋅x = -x, eq_trans 15 16. rmul_minus_one. ⊢ x ∈ ℝ → (-1)⋅x = -x, subj_intro 17.
Dependencies
The given proof depends on 12 axioms:
eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rmul_closed, rmul_comm, rmul_distl_add, rmul_neutr, rneg_closed.