Description: A ring is a zero ring iff it is not a nonzero ring. (Contributed by AV, 14-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | 0ringnnzr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re | |
|
2 | 1 | ltnri | |
3 | breq2 | |
|
4 | 2 3 | mtbiri | |
5 | 4 | adantl | |
6 | 5 | intnand | |
7 | 6 | ex | |
8 | ianor | |
|
9 | pm2.21 | |
|
10 | fvex | |
|
11 | hashxrcl | |
|
12 | 10 11 | ax-mp | |
13 | 1xr | |
|
14 | xrlenlt | |
|
15 | 12 13 14 | mp2an | |
16 | 15 | bicomi | |
17 | simpr | |
|
18 | 1nn0 | |
|
19 | hashbnd | |
|
20 | 10 18 17 19 | mp3an12i | |
21 | hashcl | |
|
22 | simpr | |
|
23 | hasheq0 | |
|
24 | 10 23 | mp1i | |
25 | 24 | biimpd | |
26 | 25 | necon3d | |
27 | 26 | impcom | |
28 | elnnne0 | |
|
29 | 22 27 28 | sylanbrc | |
30 | 29 | ex | |
31 | 30 | adantr | |
32 | 21 31 | syl5com | |
33 | 20 32 | mpcom | |
34 | nnle1eq1 | |
|
35 | 33 34 | syl | |
36 | 17 35 | mpbid | |
37 | 36 | ex | |
38 | ringgrp | |
|
39 | eqid | |
|
40 | 39 | grpbn0 | |
41 | 38 40 | syl | |
42 | 37 41 | syl11 | |
43 | 16 42 | sylbi | |
44 | 9 43 | jaoi | |
45 | 8 44 | sylbi | |
46 | 45 | com12 | |
47 | 7 46 | impbid | |
48 | 39 | isnzr2hash | |
49 | 48 | bicomi | |
50 | 49 | notbii | |
51 | 47 50 | bitrdi | |