This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC ALGEBRAIC STRUCTURES The complex numbers as an algebraic extensible structure Ring of integers zringmpg
Description: The multiplicative group of the ring of integers is the restriction of the
multiplicative group of the complex numbers to the integers. (Contributed by AV , 15-Jun-2019)
Ref
Expression
Assertion
zringmpg ⊢ mulGrp ℂ fld ↾ 𝑠 ℤ = mulGrp ℤ ring
Proof
Step
Hyp
Ref
Expression
1
cndrng ⊢ ℂ fld ∈ DivRing
2
zex ⊢ ℤ ∈ V
3
df-zring ⊢ ℤ ring = ℂ fld ↾ 𝑠 ℤ
4
eqid ⊢ mulGrp ℂ fld = mulGrp ℂ fld
5
3 4
mgpress ⊢ ℂ fld ∈ DivRing ∧ ℤ ∈ V → mulGrp ℂ fld ↾ 𝑠 ℤ = mulGrp ℤ ring
6
1 2 5
mp2an ⊢ mulGrp ℂ fld ↾ 𝑠 ℤ = mulGrp ℤ ring