Proof 01. ⊢ 1 ∈ ℝ, calc. 02. ⊢ ¬1 = 0, calc. 03. ⊢ 1⋅(/1) = 1, rmul_inv 1 2. 04. ⊢ /1 ∈ ℝ, rinv_closed 1 2. 05. ⊢ 1⋅(/1) = /1, rmul_neutl 4. rinv_one. ⊢ 1 = /1, eq_trans_ll 3 5.
Dependencies
The given proof depends on six axioms:
eq_refl, eq_subst, rinv_closed, rmul_comm, rmul_inv, rmul_neutr.