Theorem divcl

Description: Closure law for division. (Contributed by NM, 21-Jul-2001) (Proof shortened by Mario Carneiro, 17-Feb-2014)

	Ref	Expression
Assertion	divcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		divval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) = ( ℩ 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 ) )
2		receu	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ∃! 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 )
3		riotacl	⊢ ( ∃! 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 → ( ℩ 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 ) ∈ ℂ )
4	2 3	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ℩ 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 ) ∈ ℂ )
5	1 4	eqeltrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℂ )