Metamath Proof Explorer


Theorem xdivcl

Description: Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017)

Ref Expression
Assertion xdivcl ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 /𝑒 𝐵 ) ∈ ℝ* )

Proof

Step Hyp Ref Expression
1 simp1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 𝐴 ∈ ℝ* )
2 simp2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℝ )
3 simp3 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 𝐵 ≠ 0 )
4 1 2 3 xdivcld ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 /𝑒 𝐵 ) ∈ ℝ* )