Metamath Proof Explorer

Theorem zringnzr

Description: The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020)

Ref Expression
Assertion zringnzr 
|- ZZring e. NzRing

Proof

Step Hyp Ref Expression
1 zringring 
 |-  ZZring e. Ring
2 ax-1ne0 
 |-  1 =/= 0
3 zring1 
 |-  1 = ( 1r ` ZZring )
4 zring0 
 |-  0 = ( 0g ` ZZring )
5 3 4 isnzr 
 |-  ( ZZring e. NzRing <-> ( ZZring e. Ring /\ 1 =/= 0 ) )
6 1 2 5 mpbir2an 
 |-  ZZring e. NzRing