Theorem rersubcl

Description: Closure for real subtraction. Based on subcl . (Contributed by Steven Nguyen, 7-Jan-2023)

	Ref	Expression
Assertion	rersubcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 −ℝ 𝐵 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		resubval	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 −ℝ 𝐵 ) = ( ℩ 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 ) )
2		resubeu	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ∃! 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 )
3	2	ancoms	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ∃! 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 )
4		riotacl	⊢ ( ∃! 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 → ( ℩ 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 ) ∈ ℝ )
5	3 4	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℩ 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 ) ∈ ℝ )
6	1 5	eqeltrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 −ℝ 𝐵 ) ∈ ℝ )