Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. 2 ⊢ b ∈ ℝ, hypo. 03. 1, 2 ⊢ -(a⋅b) = (-a)⋅b, rmul_compatl_neg 1 2. 04. 1, 2 ⊢ -(-(a⋅b)) = -((-a)⋅b), eq_cong 3, f t = -t. 05. 1 ⊢ -a ∈ ℝ, rneg_closed 1. 06. 1, 2 ⊢ -((-a)⋅b) = (-a)⋅(-b), rmul_compatr_neg 5 2. 07. 1, 2 ⊢ -(-(a⋅b)) = (-a)⋅(-b), eq_trans 4 6. 08. 1, 2 ⊢ a⋅b ∈ ℝ, rmul_closed 1 2. 09. 1, 2 ⊢ -(-(a⋅b)) = a⋅b, rneg_involution 8. 10. 1, 2 ⊢ (-a)⋅(-b) = -(-(a⋅b)), eq_symm 7. 11. 1, 2 ⊢ (-a)⋅(-b) = a⋅b, eq_trans 10 9. rmul_cancel_neg. ⊢ a ∈ ℝ → b ∈ ℝ → (-a)⋅(-b) = a⋅b, subj_intro_ii 11.
Dependencies
The given proof depends on 11 axioms:
eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rmul_closed, rmul_comm, rmul_distl_add, rneg_closed.