Metamath Proof Explorer


Theorem xdivcld

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

Ref Expression
Hypotheses xdivcld.1 φ A *
xdivcld.2 φ B
xdivcld.3 φ B 0
Assertion xdivcld φ A ÷ 𝑒 B *

Proof

Step Hyp Ref Expression
1 xdivcld.1 φ A *
2 xdivcld.2 φ B
3 xdivcld.3 φ B 0
4 xdivval A * B B 0 A ÷ 𝑒 B = ι x * | B 𝑒 x = A
5 1 2 3 4 syl3anc φ A ÷ 𝑒 B = ι x * | B 𝑒 x = A
6 xreceu A * B B 0 ∃! x * B 𝑒 x = A
7 1 2 3 6 syl3anc φ ∃! x * B 𝑒 x = A
8 riotacl ∃! x * B 𝑒 x = A ι x * | B 𝑒 x = A *
9 7 8 syl φ ι x * | B 𝑒 x = A *
10 5 9 eqeltrd φ A ÷ 𝑒 B *