Theorem zringgrp

Description: The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019)

	Ref	Expression
Assertion	zringgrp	⊢ ℤring ∈ Grp

Proof

Step	Hyp	Ref	Expression
1		zringring	⊢ ℤring ∈ Ring
2		ringgrp	⊢ ( ℤring ∈ Ring → ℤring ∈ Grp )
3	1 2	ax-mp	⊢ ℤring ∈ Grp