Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. 2 ⊢ b ∈ ℝ, hypo. 03. 1, 2 ⊢ ¬a = 0 → ¬b = 0 → ¬a⋅b = 0, rmul_non_zero 1 2. 04. 1, 2 ⊢ a⋅b = 0 → a = 0 ∨ b = 0, contraposition_rev_ii 3. zero_product_property. ⊢ a ∈ ℝ → b ∈ ℝ → a⋅b = 0 → a = 0 ∨ b = 0, subj_intro_ii 4.
Dependencies
The given proof depends on 17 axioms:
efq, eq_refl, eq_subst, lem, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rinv_closed, rmul_assoc, rmul_closed, rmul_comm, rmul_distl_add, rmul_inv, rmul_neutr, rneg_closed.