Database
SURREAL NUMBERS
Surreal arithmetic
Multiplication
muls02
Next ⟩
mulslid
Metamath Proof Explorer
Ascii
Unicode
Theorem
muls02
Description:
Surreal multiplication by zero.
(Contributed by
Scott Fenton
, 4-Feb-2025)
Ref
Expression
Assertion
muls02
⊢
A
∈
No
→
0
s
⋅
s
A
=
0
s
Proof
Step
Hyp
Ref
Expression
1
0sno
⊢
0
s
∈
No
2
mulscom
⊢
0
s
∈
No
∧
A
∈
No
→
0
s
⋅
s
A
=
A
⋅
s
0
s
3
1
2
mpan
⊢
A
∈
No
→
0
s
⋅
s
A
=
A
⋅
s
0
s
4
muls01
⊢
A
∈
No
→
A
⋅
s
0
s
=
0
s
5
3
4
eqtrd
⊢
A
∈
No
→
0
s
⋅
s
A
=
0
s