Description: Equivalent characterization of nonzero rings: they have at least two elements. (Contributed by Stefan O'Rear, 24-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | isnzr2.b | |
|
Assertion | isnzr2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isnzr2.b | |
|
2 | eqid | |
|
3 | eqid | |
|
4 | 2 3 | isnzr | |
5 | 1 2 | ringidcl | |
6 | 5 | adantr | |
7 | 1 3 | ring0cl | |
8 | 7 | adantr | |
9 | simpr | |
|
10 | df-ne | |
|
11 | neeq1 | |
|
12 | 10 11 | bitr3id | |
13 | neeq2 | |
|
14 | 12 13 | rspc2ev | |
15 | 6 8 9 14 | syl3anc | |
16 | 15 | ex | |
17 | 1 2 3 | ring1eq0 | |
18 | 17 | 3expb | |
19 | 18 | necon3bd | |
20 | 19 | rexlimdvva | |
21 | 16 20 | impbid | |
22 | 1 | fvexi | |
23 | 1sdom | |
|
24 | 22 23 | ax-mp | |
25 | 21 24 | bitr4di | |
26 | 1onn | |
|
27 | sucdom | |
|
28 | 26 27 | ax-mp | |
29 | df-2o | |
|
30 | 29 | breq1i | |
31 | 28 30 | bitr4i | |
32 | 25 31 | bitrdi | |
33 | 32 | pm5.32i | |
34 | 4 33 | bitri | |