Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Decimal expansion
Division in the extended real number system
xdivcld
Next ⟩
xdivcl
Metamath Proof Explorer
Ascii
Unicode
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
∈
ℝ
*