Metamath Proof Explorer


Theorem 0ringnnzr

Description: A ring is a zero ring iff it is not a nonzero ring. (Contributed by AV, 14-Apr-2019)

Ref Expression
Assertion 0ringnnzr RRingBaseR=1¬RNzRing

Proof

Step Hyp Ref Expression
1 1re 1
2 1 ltnri ¬1<1
3 breq2 BaseR=11<BaseR1<1
4 2 3 mtbiri BaseR=1¬1<BaseR
5 4 adantl RRingBaseR=1¬1<BaseR
6 5 intnand RRingBaseR=1¬RRing1<BaseR
7 6 ex RRingBaseR=1¬RRing1<BaseR
8 ianor ¬RRing1<BaseR¬RRing¬1<BaseR
9 pm2.21 ¬RRingRRingBaseR=1
10 fvex BaseRV
11 hashxrcl BaseRVBaseR*
12 10 11 ax-mp BaseR*
13 1xr 1*
14 xrlenlt BaseR*1*BaseR1¬1<BaseR
15 12 13 14 mp2an BaseR1¬1<BaseR
16 15 bicomi ¬1<BaseRBaseR1
17 simpr BaseRBaseR1BaseR1
18 1nn0 10
19 hashbnd BaseRV10BaseR1BaseRFin
20 10 18 17 19 mp3an12i BaseRBaseR1BaseRFin
21 hashcl BaseRFinBaseR0
22 simpr BaseRBaseR0BaseR0
23 hasheq0 BaseRVBaseR=0BaseR=
24 10 23 mp1i BaseR0BaseR=0BaseR=
25 24 biimpd BaseR0BaseR=0BaseR=
26 25 necon3d BaseR0BaseRBaseR0
27 26 impcom BaseRBaseR0BaseR0
28 elnnne0 BaseRBaseR0BaseR0
29 22 27 28 sylanbrc BaseRBaseR0BaseR
30 29 ex BaseRBaseR0BaseR
31 30 adantr BaseRBaseR1BaseR0BaseR
32 21 31 syl5com BaseRFinBaseRBaseR1BaseR
33 20 32 mpcom BaseRBaseR1BaseR
34 nnle1eq1 BaseRBaseR1BaseR=1
35 33 34 syl BaseRBaseR1BaseR1BaseR=1
36 17 35 mpbid BaseRBaseR1BaseR=1
37 36 ex BaseRBaseR1BaseR=1
38 ringgrp RRingRGrp
39 eqid BaseR=BaseR
40 39 grpbn0 RGrpBaseR
41 38 40 syl RRingBaseR
42 37 41 syl11 BaseR1RRingBaseR=1
43 16 42 sylbi ¬1<BaseRRRingBaseR=1
44 9 43 jaoi ¬RRing¬1<BaseRRRingBaseR=1
45 8 44 sylbi ¬RRing1<BaseRRRingBaseR=1
46 45 com12 RRing¬RRing1<BaseRBaseR=1
47 7 46 impbid RRingBaseR=1¬RRing1<BaseR
48 39 isnzr2hash RNzRingRRing1<BaseR
49 48 bicomi RRing1<BaseRRNzRing
50 49 notbii ¬RRing1<BaseR¬RNzRing
51 47 50 bitrdi RRingBaseR=1¬RNzRing