Description: The opposite of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 17-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | opprnzr.1 | |
|
Assertion | opprnzr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opprnzr.1 | |
|
2 | nzrring | |
|
3 | 1 | opprring | |
4 | 2 3 | syl | |
5 | eqid | |
|
6 | 5 | isnzr2 | |
7 | 6 | simprbi | |
8 | 1 5 | opprbas | |
9 | 8 | isnzr2 | |
10 | 4 7 9 | sylanbrc | |