Database
BASIC ALGEBRAIC STRUCTURES
The complex numbers as an algebraic extensible structure
Ring of integers
zringrng
Next ⟩
zringabl
Metamath Proof Explorer
Ascii
Unicode
Theorem
zringrng
Description:
The ring of integers is a non-unital ring.
(Contributed by
AV
, 17-Mar-2025)
Ref
Expression
Assertion
zringrng
⊢
ℤ
ring
∈
Rng
Proof
Step
Hyp
Ref
Expression
1
zringring
⊢
ℤ
ring
∈
Ring
2
ringrng
⊢
ℤ
ring
∈
Ring
→
ℤ
ring
∈
Rng
3
1
2
ax-mp
⊢
ℤ
ring
∈
Rng