Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. 2 ⊢ b ∈ ℝ, hypo. 03. 3 ⊢ a ≤ 0, hypo. 04. 4 ⊢ 0 ≤ b, hypo. 05. 1, 2, 3, 4 ⊢ b⋅a ≤ 0, rmul_nn_np 2 1 4 3. 06. 1, 2 ⊢ a⋅b = b⋅a, rmul_comm 1 2. 07. 1, 2, 3, 4 ⊢ a⋅b ≤ 0, eq_le_trans 6 5. rmul_np_nn. ⊢ a ∈ ℝ → b ∈ ℝ → a ≤ 0 → 0 ≤ b → a⋅b ≤ 0, subj_intro_iv 7.
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.