Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. 2 ⊢ b ∈ ℝ, hypo. 03. 3 ⊢ ¬a = 0, hypo. 04. 4 ⊢ ¬b = 0, hypo. 05. 5 ⊢ a⋅b = 0, hypo. 06. 5 ⊢ a⋅b⋅(1/b) = 0⋅(1/b), eq_cong 5, f t = t⋅(1/b). 07. 2, 4 ⊢ 1/b ∈ ℝ, rreci_closed 2 4. 08. 2, 4 ⊢ 0⋅(1/b) = 0, rmul_lzero 7. 09. 2, 4, 5 ⊢ a⋅b⋅(1/b) = 0, eq_trans 6 8. 10. 1, 2, 4 ⊢ a⋅b⋅(1/b) = a⋅(b⋅(1/b)), rmul_assoc 1 2 7. 11. 2, 4 ⊢ b⋅(1/b) = 1, rmul_reci_cancel 2 4. 12. 1, 2, 4 ⊢ a⋅b⋅(1/b) = a⋅1, eq_subst 11 10, P t ↔ a⋅b⋅(1/b) = a⋅t. 13. 1, 2, 4, 5 ⊢ a⋅1 = 0, eq_trans_ll 12 9. 14. 1 ⊢ a⋅1 = a, rmul_neutr 1. 15. 1, 2, 4, 5 ⊢ a = 0, eq_trans_ll 14 13. 16. 1, 2, 3, 4, 5 ⊢ ⊥, neg_elim 3 15. 17. 1, 2, 3, 4 ⊢ ¬a⋅b = 0, neg_intro 16. rmul_non_zero. ⊢ a ∈ ℝ → b ∈ ℝ → ¬a = 0 → ¬b = 0 → ¬a⋅b = 0, subj_intro_iv 17.
Dependencies
The given proof depends on 15 axioms:
eq_refl, eq_subst, 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.