rdiv_closed

Theorem rdiv_closed

Theorem. rdiv_closed
a ∈ ℝ → b ∈ ℝ → ¬b = 0 → a/b ∈ ℝ

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ ¬b = 0, hypo.
04. ⊢ a/b = a⋅(/b), rdiv_eq.
05. 2, 3 ⊢ /b ∈ ℝ, rinv_closed 2 3.
06. 1, 2, 3 ⊢ a⋅(/b) ∈ ℝ, rmul_closed 1 5.
07. 1, 2, 3 ⊢ a/b ∈ ℝ, eq_subst_rev 4 6, P t ↔ t ∈ ℝ.
rdiv_closed. ⊢ a ∈ ℝ → b ∈ ℝ → ¬b = 0 → a/b ∈ ℝ,
  subj_intro_iii 7.

Dependencies
The given proof depends on four axioms:
eq_refl, eq_subst, rinv_closed, rmul_closed.