Metamath Proof Explorer


Theorem isnzr2

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 B=BaseR
Assertion isnzr2 RNzRingRRing2𝑜B

Proof

Step Hyp Ref Expression
1 isnzr2.b B=BaseR
2 eqid 1R=1R
3 eqid 0R=0R
4 2 3 isnzr RNzRingRRing1R0R
5 1 2 ringidcl RRing1RB
6 5 adantr RRing1R0R1RB
7 1 3 ring0cl RRing0RB
8 7 adantr RRing1R0R0RB
9 simpr RRing1R0R1R0R
10 df-ne xy¬x=y
11 neeq1 x=1Rxy1Ry
12 10 11 bitr3id x=1R¬x=y1Ry
13 neeq2 y=0R1Ry1R0R
14 12 13 rspc2ev 1RB0RB1R0RxByB¬x=y
15 6 8 9 14 syl3anc RRing1R0RxByB¬x=y
16 15 ex RRing1R0RxByB¬x=y
17 1 2 3 ring1eq0 RRingxByB1R=0Rx=y
18 17 3expb RRingxByB1R=0Rx=y
19 18 necon3bd RRingxByB¬x=y1R0R
20 19 rexlimdvva RRingxByB¬x=y1R0R
21 16 20 impbid RRing1R0RxByB¬x=y
22 1 fvexi BV
23 1sdom BV1𝑜BxByB¬x=y
24 22 23 ax-mp 1𝑜BxByB¬x=y
25 21 24 bitr4di RRing1R0R1𝑜B
26 1onn 1𝑜ω
27 sucdom 1𝑜ω1𝑜Bsuc1𝑜B
28 26 27 ax-mp 1𝑜Bsuc1𝑜B
29 df-2o 2𝑜=suc1𝑜
30 29 breq1i 2𝑜Bsuc1𝑜B
31 28 30 bitr4i 1𝑜B2𝑜B
32 25 31 bitrdi RRing1R0R2𝑜B
33 32 pm5.32i RRing1R0RRRing2𝑜B
34 4 33 bitri RNzRingRRing2𝑜B