Metamath Proof Explorer

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 ∈ Ring → R ∈ NzRing ↔ chr ⁡ R ≠ 1

Proof

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