Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. 2 ⊢ b ∈ ℝ, hypo. 03. 3 ⊢ a ≤ 0, hypo. 04. 4 ⊢ b ≤ 0, hypo. 05. ⊢ 0 ∈ ℝ, calc. 06. ⊢ 0 = -0, calc. 07. 1, 3 ⊢ -0 ≤ -a, rle_neg_swaps 1 5 3. 08. 2, 4 ⊢ -0 ≤ -b, rle_neg_swaps 2 5 4. 09. 1, 3 ⊢ 0 ≤ -a, eq_le_trans 6 7. 10. 2, 4 ⊢ 0 ≤ -b, eq_le_trans 6 8. 11. 1 ⊢ -a ∈ ℝ, rneg_closed 1. 12. 2 ⊢ -b ∈ ℝ, rneg_closed 2. 13. 1, 2, 3, 4 ⊢ 0 ≤ (-a)⋅(-b), rle_compat_mul 11 12 9 10. 14. 1, 2 ⊢ -(a⋅b) = a⋅(-b), rmul_compatr_neg 1 2. 15. 1, 2 ⊢ -(-(a⋅b)) = -(a⋅(-b)), eq_cong 14, f t = -t. 16. 1, 2 ⊢ a⋅b ∈ ℝ, rmul_closed 1 2. 17. 1, 2 ⊢ -(-(a⋅b)) = a⋅b, rneg_involution 16. 18. 1, 2 ⊢ -(a⋅(-b)) = a⋅b, eq_trans_ll 15 17. 19. 1, 2 ⊢ -(a⋅(-b)) = (-a)⋅(-b), rmul_compatl_neg 1 12. 20. 1, 2 ⊢ (-a)⋅(-b) = a⋅b, eq_trans_ll 19 18. 21. 1, 2, 3, 4 ⊢ 0 ≤ a⋅b, le_eq_trans 13 20. rmul_np_np. ⊢ a ∈ ℝ → b ∈ ℝ → a ≤ 0 → b ≤ 0 → 0 ≤ a⋅b, subj_intro_iv 21.
Dependencies
The given proof depends on 13 axioms:
eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rle_compat_add, rle_compat_mul, rmul_closed, rmul_comm, rmul_distl_add, rneg_closed.