Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Decimal expansion
Division in the extended real number system
xdiv0
Next ⟩
xdiv0rp
Metamath Proof Explorer
Ascii
Unicode
Theorem
xdiv0
Description:
Division into zero is zero.
(Contributed by
Thierry Arnoux
, 18-Dec-2016)
Ref
Expression
Assertion
xdiv0
⊢
A
∈
ℝ
∧
A
≠
0
→
0
÷
𝑒
A
=
0
Proof
Step
Hyp
Ref
Expression
1
0re
⊢
0
∈
ℝ
2
rexdiv
⊢
0
∈
ℝ
∧
A
∈
ℝ
∧
A
≠
0
→
0
÷
𝑒
A
=
0
A
3
1
2
mp3an1
⊢
A
∈
ℝ
∧
A
≠
0
→
0
÷
𝑒
A
=
0
A
4
recn
⊢
A
∈
ℝ
→
A
∈
ℂ
5
div0
⊢
A
∈
ℂ
∧
A
≠
0
→
0
A
=
0
6
4
5
sylan
⊢
A
∈
ℝ
∧
A
≠
0
→
0
A
=
0
7
3
6
eqtrd
⊢
A
∈
ℝ
∧
A
≠
0
→
0
÷
𝑒
A
=
0