Theorem chrnzr

Description: Nonzero rings are precisely those with characteristic not 1. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Assertion	chrnzr	|- ( R e. Ring -> ( R e. NzRing <-> ( chr ` R ) =/= 1 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( 1r ` R ) = ( 1r ` R )
2		eqid	|- ( 0g ` R ) = ( 0g ` R )
3	1 2	isnzr	|- ( R e. NzRing <-> ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) )
4	3	baib	|- ( R e. Ring -> ( R e. NzRing <-> ( 1r ` R ) =/= ( 0g ` R ) ) )
5		1z	|- 1 e. ZZ
6		eqid	|- ( chr ` R ) = ( chr ` R )
7		eqid	|- ( ZRHom ` R ) = ( ZRHom ` R )
8	6 7 2	chrdvds	|- ( ( R e. Ring /\ 1 e. ZZ ) -> ( ( chr ` R ) || 1 <-> ( ( ZRHom ` R ) ` 1 ) = ( 0g ` R ) ) )
9	5 8	mpan2	|- ( R e. Ring -> ( ( chr ` R ) || 1 <-> ( ( ZRHom ` R ) ` 1 ) = ( 0g ` R ) ) )
10	6	chrcl	|- ( R e. Ring -> ( chr ` R ) e. NN0 )
11		dvds1	|- ( ( chr ` R ) e. NN0 -> ( ( chr ` R ) || 1 <-> ( chr ` R ) = 1 ) )
12	10 11	syl	|- ( R e. Ring -> ( ( chr ` R ) || 1 <-> ( chr ` R ) = 1 ) )
13	7 1	zrh1	|- ( R e. Ring -> ( ( ZRHom ` R ) ` 1 ) = ( 1r ` R ) )
14	13	eqeq1d	|- ( R e. Ring -> ( ( ( ZRHom ` R ) ` 1 ) = ( 0g ` R ) <-> ( 1r ` R ) = ( 0g ` R ) ) )
15	9 12 14	3bitr3d	|- ( R e. Ring -> ( ( chr ` R ) = 1 <-> ( 1r ` R ) = ( 0g ` R ) ) )
16	15	necon3bid	|- ( R e. Ring -> ( ( chr ` R ) =/= 1 <-> ( 1r ` R ) =/= ( 0g ` R ) ) )
17	4 16	bitr4d	|- ( R e. Ring -> ( R e. NzRing <-> ( chr ` R ) =/= 1 ) )