Description: Equivalent characterization of nonzero rings: they have at least two elements. Analogous to isnzr2 . (Contributed by AV, 14-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | isnzr2hash.b | |
|
Assertion | isnzr2hash | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isnzr2hash.b | |
|
2 | eqid | |
|
3 | eqid | |
|
4 | 2 3 | isnzr | |
5 | 1 2 | ringidcl | |
6 | 1 3 | ring0cl | |
7 | 1xr | |
|
8 | 7 | a1i | |
9 | prex | |
|
10 | hashxrcl | |
|
11 | 9 10 | mp1i | |
12 | 1 | fvexi | |
13 | hashxrcl | |
|
14 | 12 13 | mp1i | |
15 | 1lt2 | |
|
16 | hashprg | |
|
17 | 16 | biimpa | |
18 | 15 17 | breqtrrid | |
19 | simpl | |
|
20 | fvex | |
|
21 | fvex | |
|
22 | 20 21 | prss | |
23 | 19 22 | sylib | |
24 | hashss | |
|
25 | 12 23 24 | sylancr | |
26 | 8 11 14 18 25 | xrltletrd | |
27 | 26 | ex | |
28 | 5 6 27 | syl2anc | |
29 | 28 | imdistani | |
30 | simpl | |
|
31 | 1 2 3 | ring1ne0 | |
32 | 30 31 | jca | |
33 | 29 32 | impbii | |
34 | 4 33 | bitri | |