Metamath Proof Explorer

Theorem 0ringnnzr

Description: A ring is a zero ring iff it is not a nonzero ring. (Contributed by AV, 14-Apr-2019)

Ref Expression
Assertion 0ringnnzr ⊢ R ∈ Ring → Base R = 1 ↔ ¬ R ∈ NzRing

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 1 ltnri ⊢ ¬ 1 < 1
3 breq2 ⊢ Base R = 1 → 1 < Base R ↔ 1 < 1
4 2 3 mtbiri ⊢ Base R = 1 → ¬ 1 < Base R
5 4 adantl ⊢ R ∈ Ring ∧ Base R = 1 → ¬ 1 < Base R
6 5 intnand ⊢ R ∈ Ring ∧ Base R = 1 → ¬ R ∈ Ring ∧ 1 < Base R
7 6 ex ⊢ R ∈ Ring → Base R = 1 → ¬ R ∈ Ring ∧ 1 < Base R
8 ianor ⊢ ¬ R ∈ Ring ∧ 1 < Base R ↔ ¬ R ∈ Ring ∨ ¬ 1 < Base R
9 pm2.21 ⊢ ¬ R ∈ Ring → R ∈ Ring → Base R = 1
10 fvex ⊢ Base R ∈ V
11 hashxrcl ⊢ Base R ∈ V → Base R ∈ ℝ *
12 10 11 ax-mp ⊢ Base R ∈ ℝ *
13 1xr ⊢ 1 ∈ ℝ *
14 xrlenlt ⊢ Base R ∈ ℝ * ∧ 1 ∈ ℝ * → Base R ≤ 1 ↔ ¬ 1 < Base R
15 12 13 14 mp2an ⊢ Base R ≤ 1 ↔ ¬ 1 < Base R
16 15 bicomi ⊢ ¬ 1 < Base R ↔ Base R ≤ 1
17 simpr ⊢ Base R ≠ ∅ ∧ Base R ≤ 1 → Base R ≤ 1
18 1nn0 ⊢ 1 ∈ ℕ 0
19 hashbnd ⊢ Base R ∈ V ∧ 1 ∈ ℕ 0 ∧ Base R ≤ 1 → Base R ∈ Fin
20 10 18 17 19 mp3an12i ⊢ Base R ≠ ∅ ∧ Base R ≤ 1 → Base R ∈ Fin
21 hashcl ⊢ Base R ∈ Fin → Base R ∈ ℕ 0
22 simpr ⊢ Base R ≠ ∅ ∧ Base R ∈ ℕ 0 → Base R ∈ ℕ 0
23 hasheq0 ⊢ Base R ∈ V → Base R = 0 ↔ Base R = ∅
24 10 23 mp1i ⊢ Base R ∈ ℕ 0 → Base R = 0 ↔ Base R = ∅
25 24 biimpd ⊢ Base R ∈ ℕ 0 → Base R = 0 → Base R = ∅
26 25 necon3d ⊢ Base R ∈ ℕ 0 → Base R ≠ ∅ → Base R ≠ 0
27 26 impcom ⊢ Base R ≠ ∅ ∧ Base R ∈ ℕ 0 → Base R ≠ 0
28 elnnne0 ⊢ Base R ∈ ℕ ↔ Base R ∈ ℕ 0 ∧ Base R ≠ 0
29 22 27 28 sylanbrc ⊢ Base R ≠ ∅ ∧ Base R ∈ ℕ 0 → Base R ∈ ℕ
30 29 ex ⊢ Base R ≠ ∅ → Base R ∈ ℕ 0 → Base R ∈ ℕ
31 30 adantr ⊢ Base R ≠ ∅ ∧ Base R ≤ 1 → Base R ∈ ℕ 0 → Base R ∈ ℕ
32 21 31 syl5com ⊢ Base R ∈ Fin → Base R ≠ ∅ ∧ Base R ≤ 1 → Base R ∈ ℕ
33 20 32 mpcom ⊢ Base R ≠ ∅ ∧ Base R ≤ 1 → Base R ∈ ℕ
34 nnle1eq1 ⊢ Base R ∈ ℕ → Base R ≤ 1 ↔ Base R = 1
35 33 34 syl ⊢ Base R ≠ ∅ ∧ Base R ≤ 1 → Base R ≤ 1 ↔ Base R = 1
36 17 35 mpbid ⊢ Base R ≠ ∅ ∧ Base R ≤ 1 → Base R = 1
37 36 ex ⊢ Base R ≠ ∅ → Base R ≤ 1 → Base R = 1
38 ringgrp ⊢ R ∈ Ring → R ∈ Grp
39 eqid ⊢ Base R = Base R
40 39 grpbn0 ⊢ R ∈ Grp → Base R ≠ ∅
41 38 40 syl ⊢ R ∈ Ring → Base R ≠ ∅
42 37 41 syl11 ⊢ Base R ≤ 1 → R ∈ Ring → Base R = 1
43 16 42 sylbi ⊢ ¬ 1 < Base R → R ∈ Ring → Base R = 1
44 9 43 jaoi ⊢ ¬ R ∈ Ring ∨ ¬ 1 < Base R → R ∈ Ring → Base R = 1
45 8 44 sylbi ⊢ ¬ R ∈ Ring ∧ 1 < Base R → R ∈ Ring → Base R = 1
46 45 com12 ⊢ R ∈ Ring → ¬ R ∈ Ring ∧ 1 < Base R → Base R = 1
47 7 46 impbid ⊢ R ∈ Ring → Base R = 1 ↔ ¬ R ∈ Ring ∧ 1 < Base R
48 39 isnzr2hash ⊢ R ∈ NzRing ↔ R ∈ Ring ∧ 1 < Base R
49 48 bicomi ⊢ R ∈ Ring ∧ 1 < Base R ↔ R ∈ NzRing
50 49 notbii ⊢ ¬ R ∈ Ring ∧ 1 < Base R ↔ ¬ R ∈ NzRing
51 47 50 bitrdi ⊢ R ∈ Ring → Base R = 1 ↔ ¬ R ∈ NzRing