chrnzr

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

		Ref	Expression
	Assertion	chrnzr	$⊢ R \in Ring \to (R \in NzRing \leftrightarrow chr (R) \neq 1)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ 1_{R} = 1_{R}$
2		eqid	$⊢ 0_{R} = 0_{R}$
3	1 2	isnzr	$⊢ R \in NzRing \leftrightarrow (R \in Ring \land 1_{R} \neq 0_{R})$
4	3	baib	$⊢ R \in Ring \to (R \in NzRing \leftrightarrow 1_{R} \neq 0_{R})$
5		1z	$⊢ 1 \in ℤ$
6		eqid	$⊢ chr (R) = chr (R)$
7		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
8	6 7 2	chrdvds	$⊢ (R \in Ring \land 1 \in ℤ) \to (chr (R) ∥ 1 \leftrightarrow ℤRHom (R) (1) = 0_{R})$
9	5 8	mpan2	$⊢ R \in Ring \to (chr (R) ∥ 1 \leftrightarrow ℤRHom (R) (1) = 0_{R})$
10	6	chrcl	$⊢ R \in Ring \to chr (R) \in ℕ_{0}$
11		dvds1	$⊢ chr (R) \in ℕ_{0} \to (chr (R) ∥ 1 \leftrightarrow chr (R) = 1)$
12	10 11	syl	$⊢ R \in Ring \to (chr (R) ∥ 1 \leftrightarrow chr (R) = 1)$
13	7 1	zrh1	$⊢ R \in Ring \to ℤRHom (R) (1) = 1_{R}$
14	13	eqeq1d	$⊢ R \in Ring \to (ℤRHom (R) (1) = 0_{R} \leftrightarrow 1_{R} = 0_{R})$
15	9 12 14	3bitr3d	$⊢ R \in Ring \to (chr (R) = 1 \leftrightarrow 1_{R} = 0_{R})$
16	15	necon3bid	$⊢ R \in Ring \to (chr (R) \neq 1 \leftrightarrow 1_{R} \neq 0_{R})$
17	4 16	bitr4d	$⊢ R \in Ring \to (R \in NzRing \leftrightarrow chr (R) \neq 1)$

Metamath Proof Explorer