Step |
Hyp |
Ref |
Expression |
1 |
|
2zrng.e |
|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } |
2 |
|
2zrngbas.r |
|- R = ( CCfld |`s E ) |
3 |
|
eqeq1 |
|- ( z = a -> ( z = ( 2 x. x ) <-> a = ( 2 x. x ) ) ) |
4 |
3
|
rexbidv |
|- ( z = a -> ( E. x e. ZZ z = ( 2 x. x ) <-> E. x e. ZZ a = ( 2 x. x ) ) ) |
5 |
4 1
|
elrab2 |
|- ( a e. E <-> ( a e. ZZ /\ E. x e. ZZ a = ( 2 x. x ) ) ) |
6 |
|
eqeq1 |
|- ( z = b -> ( z = ( 2 x. x ) <-> b = ( 2 x. x ) ) ) |
7 |
6
|
rexbidv |
|- ( z = b -> ( E. x e. ZZ z = ( 2 x. x ) <-> E. x e. ZZ b = ( 2 x. x ) ) ) |
8 |
7 1
|
elrab2 |
|- ( b e. E <-> ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) ) |
9 |
|
oveq2 |
|- ( x = y -> ( 2 x. x ) = ( 2 x. y ) ) |
10 |
9
|
eqeq2d |
|- ( x = y -> ( a = ( 2 x. x ) <-> a = ( 2 x. y ) ) ) |
11 |
10
|
cbvrexvw |
|- ( E. x e. ZZ a = ( 2 x. x ) <-> E. y e. ZZ a = ( 2 x. y ) ) |
12 |
|
zaddcl |
|- ( ( a e. ZZ /\ b e. ZZ ) -> ( a + b ) e. ZZ ) |
13 |
12
|
ancoms |
|- ( ( b e. ZZ /\ a e. ZZ ) -> ( a + b ) e. ZZ ) |
14 |
13
|
adantr |
|- ( ( ( b e. ZZ /\ a e. ZZ ) /\ ( E. x e. ZZ b = ( 2 x. x ) /\ E. y e. ZZ a = ( 2 x. y ) ) ) -> ( a + b ) e. ZZ ) |
15 |
|
simpl |
|- ( ( y e. ZZ /\ a = ( 2 x. y ) ) -> y e. ZZ ) |
16 |
|
simpl |
|- ( ( x e. ZZ /\ b = ( 2 x. x ) ) -> x e. ZZ ) |
17 |
|
zaddcl |
|- ( ( y e. ZZ /\ x e. ZZ ) -> ( y + x ) e. ZZ ) |
18 |
15 16 17
|
syl2anr |
|- ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) -> ( y + x ) e. ZZ ) |
19 |
18
|
adantr |
|- ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> ( y + x ) e. ZZ ) |
20 |
|
oveq2 |
|- ( z = ( y + x ) -> ( 2 x. z ) = ( 2 x. ( y + x ) ) ) |
21 |
20
|
eqeq2d |
|- ( z = ( y + x ) -> ( ( 2 x. ( y + x ) ) = ( 2 x. z ) <-> ( 2 x. ( y + x ) ) = ( 2 x. ( y + x ) ) ) ) |
22 |
21
|
adantl |
|- ( ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) /\ z = ( y + x ) ) -> ( ( 2 x. ( y + x ) ) = ( 2 x. z ) <-> ( 2 x. ( y + x ) ) = ( 2 x. ( y + x ) ) ) ) |
23 |
|
eqidd |
|- ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> ( 2 x. ( y + x ) ) = ( 2 x. ( y + x ) ) ) |
24 |
19 22 23
|
rspcedvd |
|- ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> E. z e. ZZ ( 2 x. ( y + x ) ) = ( 2 x. z ) ) |
25 |
|
simpr |
|- ( ( y e. ZZ /\ a = ( 2 x. y ) ) -> a = ( 2 x. y ) ) |
26 |
|
simpr |
|- ( ( x e. ZZ /\ b = ( 2 x. x ) ) -> b = ( 2 x. x ) ) |
27 |
25 26
|
oveqan12rd |
|- ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) -> ( a + b ) = ( ( 2 x. y ) + ( 2 x. x ) ) ) |
28 |
27
|
adantr |
|- ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> ( a + b ) = ( ( 2 x. y ) + ( 2 x. x ) ) ) |
29 |
|
2cnd |
|- ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) -> 2 e. CC ) |
30 |
|
zcn |
|- ( y e. ZZ -> y e. CC ) |
31 |
30
|
adantr |
|- ( ( y e. ZZ /\ a = ( 2 x. y ) ) -> y e. CC ) |
32 |
31
|
adantl |
|- ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) -> y e. CC ) |
33 |
|
zcn |
|- ( x e. ZZ -> x e. CC ) |
34 |
33
|
adantr |
|- ( ( x e. ZZ /\ b = ( 2 x. x ) ) -> x e. CC ) |
35 |
34
|
adantr |
|- ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) -> x e. CC ) |
36 |
29 32 35
|
adddid |
|- ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) -> ( 2 x. ( y + x ) ) = ( ( 2 x. y ) + ( 2 x. x ) ) ) |
37 |
36
|
adantr |
|- ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> ( 2 x. ( y + x ) ) = ( ( 2 x. y ) + ( 2 x. x ) ) ) |
38 |
28 37
|
eqtr4d |
|- ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> ( a + b ) = ( 2 x. ( y + x ) ) ) |
39 |
38
|
eqeq1d |
|- ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> ( ( a + b ) = ( 2 x. z ) <-> ( 2 x. ( y + x ) ) = ( 2 x. z ) ) ) |
40 |
39
|
rexbidv |
|- ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> ( E. z e. ZZ ( a + b ) = ( 2 x. z ) <-> E. z e. ZZ ( 2 x. ( y + x ) ) = ( 2 x. z ) ) ) |
41 |
24 40
|
mpbird |
|- ( ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) /\ ( b e. ZZ /\ a e. ZZ ) ) -> E. z e. ZZ ( a + b ) = ( 2 x. z ) ) |
42 |
41
|
ex |
|- ( ( ( x e. ZZ /\ b = ( 2 x. x ) ) /\ ( y e. ZZ /\ a = ( 2 x. y ) ) ) -> ( ( b e. ZZ /\ a e. ZZ ) -> E. z e. ZZ ( a + b ) = ( 2 x. z ) ) ) |
43 |
42
|
rexlimdvaa |
|- ( ( x e. ZZ /\ b = ( 2 x. x ) ) -> ( E. y e. ZZ a = ( 2 x. y ) -> ( ( b e. ZZ /\ a e. ZZ ) -> E. z e. ZZ ( a + b ) = ( 2 x. z ) ) ) ) |
44 |
43
|
rexlimiva |
|- ( E. x e. ZZ b = ( 2 x. x ) -> ( E. y e. ZZ a = ( 2 x. y ) -> ( ( b e. ZZ /\ a e. ZZ ) -> E. z e. ZZ ( a + b ) = ( 2 x. z ) ) ) ) |
45 |
44
|
imp |
|- ( ( E. x e. ZZ b = ( 2 x. x ) /\ E. y e. ZZ a = ( 2 x. y ) ) -> ( ( b e. ZZ /\ a e. ZZ ) -> E. z e. ZZ ( a + b ) = ( 2 x. z ) ) ) |
46 |
|
oveq2 |
|- ( x = z -> ( 2 x. x ) = ( 2 x. z ) ) |
47 |
46
|
eqeq2d |
|- ( x = z -> ( ( a + b ) = ( 2 x. x ) <-> ( a + b ) = ( 2 x. z ) ) ) |
48 |
47
|
cbvrexvw |
|- ( E. x e. ZZ ( a + b ) = ( 2 x. x ) <-> E. z e. ZZ ( a + b ) = ( 2 x. z ) ) |
49 |
45 48
|
syl6ibr |
|- ( ( E. x e. ZZ b = ( 2 x. x ) /\ E. y e. ZZ a = ( 2 x. y ) ) -> ( ( b e. ZZ /\ a e. ZZ ) -> E. x e. ZZ ( a + b ) = ( 2 x. x ) ) ) |
50 |
49
|
impcom |
|- ( ( ( b e. ZZ /\ a e. ZZ ) /\ ( E. x e. ZZ b = ( 2 x. x ) /\ E. y e. ZZ a = ( 2 x. y ) ) ) -> E. x e. ZZ ( a + b ) = ( 2 x. x ) ) |
51 |
|
eqeq1 |
|- ( z = ( a + b ) -> ( z = ( 2 x. x ) <-> ( a + b ) = ( 2 x. x ) ) ) |
52 |
51
|
rexbidv |
|- ( z = ( a + b ) -> ( E. x e. ZZ z = ( 2 x. x ) <-> E. x e. ZZ ( a + b ) = ( 2 x. x ) ) ) |
53 |
52 1
|
elrab2 |
|- ( ( a + b ) e. E <-> ( ( a + b ) e. ZZ /\ E. x e. ZZ ( a + b ) = ( 2 x. x ) ) ) |
54 |
14 50 53
|
sylanbrc |
|- ( ( ( b e. ZZ /\ a e. ZZ ) /\ ( E. x e. ZZ b = ( 2 x. x ) /\ E. y e. ZZ a = ( 2 x. y ) ) ) -> ( a + b ) e. E ) |
55 |
54
|
exp32 |
|- ( ( b e. ZZ /\ a e. ZZ ) -> ( E. x e. ZZ b = ( 2 x. x ) -> ( E. y e. ZZ a = ( 2 x. y ) -> ( a + b ) e. E ) ) ) |
56 |
55
|
impancom |
|- ( ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) -> ( a e. ZZ -> ( E. y e. ZZ a = ( 2 x. y ) -> ( a + b ) e. E ) ) ) |
57 |
56
|
com13 |
|- ( E. y e. ZZ a = ( 2 x. y ) -> ( a e. ZZ -> ( ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) -> ( a + b ) e. E ) ) ) |
58 |
11 57
|
sylbi |
|- ( E. x e. ZZ a = ( 2 x. x ) -> ( a e. ZZ -> ( ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) -> ( a + b ) e. E ) ) ) |
59 |
58
|
impcom |
|- ( ( a e. ZZ /\ E. x e. ZZ a = ( 2 x. x ) ) -> ( ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) -> ( a + b ) e. E ) ) |
60 |
59
|
imp |
|- ( ( ( a e. ZZ /\ E. x e. ZZ a = ( 2 x. x ) ) /\ ( b e. ZZ /\ E. x e. ZZ b = ( 2 x. x ) ) ) -> ( a + b ) e. E ) |
61 |
5 8 60
|
syl2anb |
|- ( ( a e. E /\ b e. E ) -> ( a + b ) e. E ) |
62 |
61
|
rgen2 |
|- A. a e. E A. b e. E ( a + b ) e. E |
63 |
|
0z |
|- 0 e. ZZ |
64 |
|
2cn |
|- 2 e. CC |
65 |
|
0zd |
|- ( 2 e. CC -> 0 e. ZZ ) |
66 |
|
oveq2 |
|- ( x = 0 -> ( 2 x. x ) = ( 2 x. 0 ) ) |
67 |
66
|
eqeq2d |
|- ( x = 0 -> ( 0 = ( 2 x. x ) <-> 0 = ( 2 x. 0 ) ) ) |
68 |
67
|
adantl |
|- ( ( 2 e. CC /\ x = 0 ) -> ( 0 = ( 2 x. x ) <-> 0 = ( 2 x. 0 ) ) ) |
69 |
|
mul01 |
|- ( 2 e. CC -> ( 2 x. 0 ) = 0 ) |
70 |
69
|
eqcomd |
|- ( 2 e. CC -> 0 = ( 2 x. 0 ) ) |
71 |
65 68 70
|
rspcedvd |
|- ( 2 e. CC -> E. x e. ZZ 0 = ( 2 x. x ) ) |
72 |
64 71
|
ax-mp |
|- E. x e. ZZ 0 = ( 2 x. x ) |
73 |
|
eqeq1 |
|- ( z = 0 -> ( z = ( 2 x. x ) <-> 0 = ( 2 x. x ) ) ) |
74 |
73
|
rexbidv |
|- ( z = 0 -> ( E. x e. ZZ z = ( 2 x. x ) <-> E. x e. ZZ 0 = ( 2 x. x ) ) ) |
75 |
74
|
elrab |
|- ( 0 e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } <-> ( 0 e. ZZ /\ E. x e. ZZ 0 = ( 2 x. x ) ) ) |
76 |
63 72 75
|
mpbir2an |
|- 0 e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } |
77 |
76 1
|
eleqtrri |
|- 0 e. E |
78 |
1 2
|
2zrngbas |
|- E = ( Base ` R ) |
79 |
1 2
|
2zrngadd |
|- + = ( +g ` R ) |
80 |
78 79
|
ismgmn0 |
|- ( 0 e. E -> ( R e. Mgm <-> A. a e. E A. b e. E ( a + b ) e. E ) ) |
81 |
77 80
|
ax-mp |
|- ( R e. Mgm <-> A. a e. E A. b e. E ( a + b ) e. E ) |
82 |
62 81
|
mpbir |
|- R e. Mgm |