This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sn-redivcld

Description: Closure law for real division. (Contributed by SN, 25-Nov-2025)

Ref Expression
Hypotheses redivvald.a ⊢ φ → A ∈ ℝ
redivvald.b ⊢ φ → B ∈ ℝ
redivvald.z ⊢ φ → B ≠ 0
Assertion sn-redivcld Could not format assertion : No typesetting found for |- ( ph -> ( A /R B ) e. RR ) with typecode |-

Proof

Step Hyp Ref Expression
1 redivvald.a ⊢ φ → A ∈ ℝ
2 redivvald.b ⊢ φ → B ∈ ℝ
3 redivvald.z ⊢ φ → B ≠ 0
4 1 2 3 redivvald Could not format ( ph -> ( A /R B ) = ( iota_ x e. RR ( B x. x ) = A ) ) : No typesetting found for |- ( ph -> ( A /R B ) = ( iota_ x e. RR ( B x. x ) = A ) ) with typecode |-
5 1 2 3 rediveud ⊢ φ → ∃! x ∈ ℝ B ⁢ x = A
6 riotacl ⊢ ∃! x ∈ ℝ B ⁢ x = A → ι x ∈ ℝ | B ⁢ x = A ∈ ℝ
7 5 6 syl ⊢ φ → ι x ∈ ℝ | B ⁢ x = A ∈ ℝ
8 4 7 eqeltrd Could not format ( ph -> ( A /R B ) e. RR ) : No typesetting found for |- ( ph -> ( A /R B ) e. RR ) with typecode |-