rdiv_neut

Theorem rdiv_neut

Theorem. rdiv_neut
a ∈ ℝ → a/1 = a

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. ⊢ a/1 = a⋅(/1), rdiv_eq.
03. ⊢ 1 ∈ ℝ, calc.
04. ⊢ a⋅1 = a⋅(/1), eq_cong rinv_one, f t = a⋅t.
05. ⊢ a/1 = a⋅1, eq_trans_rr 2 4.
06. 1 ⊢ a⋅1 = a, rmul_neutr 1.
07. 1 ⊢ a/1 = a, eq_trans 5 6.
rdiv_neut. ⊢ a ∈ ℝ → a/1 = a, subj_intro 7.

Dependencies
The given proof depends on six axioms:
eq_refl, eq_subst, rinv_closed, rmul_comm, rmul_inv, rmul_neutr.