Description: If a ring has at least two elements, its one and zero are different. (Contributed by AV, 13-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ring1ne0.b | |
|
ring1ne0.u | |
||
ring1ne0.z | |
||
Assertion | ring1ne0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ring1ne0.b | |
|
2 | ring1ne0.u | |
|
3 | ring1ne0.z | |
|
4 | 1 | fvexi | |
5 | hashgt12el | |
|
6 | 4 5 | mpan | |
7 | 6 | adantl | |
8 | 1 2 3 | ring1eq0 | |
9 | 8 | necon3d | |
10 | 9 | 3expib | |
11 | 10 | adantr | |
12 | 11 | com3l | |
13 | 12 | rexlimivv | |
14 | 7 13 | mpcom | |