Description: R is a (multiplicative) magma. (Contributed by AV, 11-Feb-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 2zrng.e | |
|
2zrngbas.r | |
||
2zrngmmgm.1 | |
||
Assertion | 2zrngmmgm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2zrng.e | |
|
2 | 2zrngbas.r | |
|
3 | 2zrngmmgm.1 | |
|
4 | eqeq1 | |
|
5 | 4 | rexbidv | |
6 | 5 1 | elrab2 | |
7 | eqeq1 | |
|
8 | 7 | rexbidv | |
9 | 8 1 | elrab2 | |
10 | zmulcl | |
|
11 | 10 | ad2ant2r | |
12 | nfv | |
|
13 | nfv | |
|
14 | nfre1 | |
|
15 | 13 14 | nfan | |
16 | nfv | |
|
17 | 15 16 | nfim | |
18 | 12 17 | nfim | |
19 | simpll | |
|
20 | simpl | |
|
21 | zmulcl | |
|
22 | 19 20 21 | syl2an | |
23 | oveq2 | |
|
24 | 23 | eqeq2d | |
25 | 24 | adantl | |
26 | oveq1 | |
|
27 | 26 | ad3antlr | |
28 | 2cnd | |
|
29 | zcn | |
|
30 | 29 | ad3antrrr | |
31 | zcn | |
|
32 | 31 | adantr | |
33 | 32 | adantl | |
34 | 28 30 33 | mulassd | |
35 | 27 34 | eqtrd | |
36 | 22 25 35 | rspcedvd | |
37 | 36 | exp41 | |
38 | 18 37 | rexlimi | |
39 | 38 | impcom | |
40 | 39 | imp | |
41 | eqeq1 | |
|
42 | 41 | rexbidv | |
43 | 42 1 | elrab2 | |
44 | oveq2 | |
|
45 | 44 | eqeq2d | |
46 | 45 | cbvrexvw | |
47 | 46 | anbi2i | |
48 | 43 47 | bitri | |
49 | 11 40 48 | sylanbrc | |
50 | 6 9 49 | syl2anb | |
51 | 50 | rgen2 | |
52 | 1 | 0even | |
53 | 1 2 | 2zrngbas | |
54 | 3 53 | mgpbas | |
55 | 1 2 | 2zrngmul | |
56 | 3 55 | mgpplusg | |
57 | 54 56 | ismgmn0 | |
58 | 52 57 | ax-mp | |
59 | 51 58 | mpbir | |