Theorem rmul_nn_np

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ 0 ≤ a, hypo.
04. 4 ⊢ b ≤ 0, hypo.
05. ⊢ 0 ∈ ℝ, calc.
06. 2, 4 ⊢ -0 ≤ -b, rle_neg_swaps 2 5 4.
07. ⊢ 0 = -0, calc.
08. 2, 4 ⊢ 0 ≤ -b, eq_le_trans 7 6.
09. 2 ⊢ -b ∈ ℝ, rneg_closed 2.
10. 1, 2, 3, 4 ⊢ 0 ≤ a⋅(-b), rle_compat_mul 1 9 3 8.
11. 1, 2 ⊢ -(a⋅b) = a⋅(-b), rmul_compatr_neg 1 2.
12. 1, 2 ⊢ a⋅(-b) = -(a⋅b), eq_symm 11.
13. 1, 2, 3, 4 ⊢ 0 ≤ -(a⋅b), le_eq_trans 10 12.
14. 1, 2 ⊢ a⋅b ∈ ℝ, rmul_closed 1 2.
15. 1, 2 ⊢ -(a⋅b) ∈ ℝ, rneg_closed 14.
16. 1, 2, 3, 4 ⊢ -(-(a⋅b)) ≤ 0, rneg_non_negative 15 13.
17. 1, 2 ⊢ -(-(a⋅b)) = a⋅b, rneg_involution 14.
18. 1, 2 ⊢ a⋅b = -(-(a⋅b)), eq_symm 17.
19. 1, 2, 3, 4 ⊢ a⋅b ≤ 0, eq_le_trans 18 16.
rmul_nn_np. ⊢ a ∈ ℝ → b ∈ ℝ →
  0 ≤ a → b ≤ 0 → a⋅b ≤ 0, subj_intro_iv 19.

Dependencies
The given proof depends on 12 axioms:
eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rle_compat_add, rle_compat_mul, rmul_closed, rmul_distl_add, rneg_closed.