Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. 2 ⊢ ¬a = 0, hypo. 03. 1, 2 ⊢ 1/a = /a, rdiv_reci 1 2. 04. 1, 2 ⊢ a⋅(1/a) = a⋅(/a), eq_cong 3, f t = a⋅t. 05. 1, 2 ⊢ a⋅(/a) = 1, rmul_inv 1 2. 06. 1, 2 ⊢ a⋅(1/a) = 1, eq_trans 4 5. rmul_reci_cancel. ⊢ a ∈ ℝ → ¬a = 0 → a⋅(1/a) = 1, subj_intro_ii 6.
Dependencies
The given proof depends on six axioms:
eq_refl, eq_subst, rinv_closed, rmul_comm, rmul_inv, rmul_neutr.