Theorem chrnzr

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

	Ref	Expression
Assertion	chrnzr	⊢ ( 𝑅 ∈ Ring → ( 𝑅 ∈ NzRing ↔ ( chr ‘ 𝑅 ) ≠ 1 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
2		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
3	1 2	isnzr	⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) )
4	3	baib	⊢ ( 𝑅 ∈ Ring → ( 𝑅 ∈ NzRing ↔ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) )
5		1z	⊢ 1 ∈ ℤ
6		eqid	⊢ ( chr ‘ 𝑅 ) = ( chr ‘ 𝑅 )
7		eqid	⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
8	6 7 2	chrdvds	⊢ ( ( 𝑅 ∈ Ring ∧ 1 ∈ ℤ ) → ( ( chr ‘ 𝑅 ) ∥ 1 ↔ ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) = ( 0g ‘ 𝑅 ) ) )
9	5 8	mpan2	⊢ ( 𝑅 ∈ Ring → ( ( chr ‘ 𝑅 ) ∥ 1 ↔ ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) = ( 0g ‘ 𝑅 ) ) )
10	6	chrcl	⊢ ( 𝑅 ∈ Ring → ( chr ‘ 𝑅 ) ∈ ℕ0 )
11		dvds1	⊢ ( ( chr ‘ 𝑅 ) ∈ ℕ0 → ( ( chr ‘ 𝑅 ) ∥ 1 ↔ ( chr ‘ 𝑅 ) = 1 ) )
12	10 11	syl	⊢ ( 𝑅 ∈ Ring → ( ( chr ‘ 𝑅 ) ∥ 1 ↔ ( chr ‘ 𝑅 ) = 1 ) )
13	7 1	zrh1	⊢ ( 𝑅 ∈ Ring → ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) = ( 1r ‘ 𝑅 ) )
14	13	eqeq1d	⊢ ( 𝑅 ∈ Ring → ( ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) = ( 0g ‘ 𝑅 ) ↔ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ) )
15	9 12 14	3bitr3d	⊢ ( 𝑅 ∈ Ring → ( ( chr ‘ 𝑅 ) = 1 ↔ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ) )
16	15	necon3bid	⊢ ( 𝑅 ∈ Ring → ( ( chr ‘ 𝑅 ) ≠ 1 ↔ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) )
17	4 16	bitr4d	⊢ ( 𝑅 ∈ Ring → ( 𝑅 ∈ NzRing ↔ ( chr ‘ 𝑅 ) ≠ 1 ) )