| Step |
Hyp |
Ref |
Expression |
| 1 |
|
gzcn |
|- ( A e. Z[i] -> A e. CC ) |
| 2 |
|
gzcn |
|- ( B e. Z[i] -> B e. CC ) |
| 3 |
|
addcl |
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC ) |
| 4 |
1 2 3
|
syl2an |
|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( A + B ) e. CC ) |
| 5 |
|
readd |
|- ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A + B ) ) = ( ( Re ` A ) + ( Re ` B ) ) ) |
| 6 |
1 2 5
|
syl2an |
|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( Re ` ( A + B ) ) = ( ( Re ` A ) + ( Re ` B ) ) ) |
| 7 |
|
elgz |
|- ( A e. Z[i] <-> ( A e. CC /\ ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) ) |
| 8 |
7
|
simp2bi |
|- ( A e. Z[i] -> ( Re ` A ) e. ZZ ) |
| 9 |
|
elgz |
|- ( B e. Z[i] <-> ( B e. CC /\ ( Re ` B ) e. ZZ /\ ( Im ` B ) e. ZZ ) ) |
| 10 |
9
|
simp2bi |
|- ( B e. Z[i] -> ( Re ` B ) e. ZZ ) |
| 11 |
|
zaddcl |
|- ( ( ( Re ` A ) e. ZZ /\ ( Re ` B ) e. ZZ ) -> ( ( Re ` A ) + ( Re ` B ) ) e. ZZ ) |
| 12 |
8 10 11
|
syl2an |
|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( Re ` A ) + ( Re ` B ) ) e. ZZ ) |
| 13 |
6 12
|
eqeltrd |
|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( Re ` ( A + B ) ) e. ZZ ) |
| 14 |
|
imadd |
|- ( ( A e. CC /\ B e. CC ) -> ( Im ` ( A + B ) ) = ( ( Im ` A ) + ( Im ` B ) ) ) |
| 15 |
1 2 14
|
syl2an |
|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( Im ` ( A + B ) ) = ( ( Im ` A ) + ( Im ` B ) ) ) |
| 16 |
7
|
simp3bi |
|- ( A e. Z[i] -> ( Im ` A ) e. ZZ ) |
| 17 |
9
|
simp3bi |
|- ( B e. Z[i] -> ( Im ` B ) e. ZZ ) |
| 18 |
|
zaddcl |
|- ( ( ( Im ` A ) e. ZZ /\ ( Im ` B ) e. ZZ ) -> ( ( Im ` A ) + ( Im ` B ) ) e. ZZ ) |
| 19 |
16 17 18
|
syl2an |
|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( Im ` A ) + ( Im ` B ) ) e. ZZ ) |
| 20 |
15 19
|
eqeltrd |
|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( Im ` ( A + B ) ) e. ZZ ) |
| 21 |
|
elgz |
|- ( ( A + B ) e. Z[i] <-> ( ( A + B ) e. CC /\ ( Re ` ( A + B ) ) e. ZZ /\ ( Im ` ( A + B ) ) e. ZZ ) ) |
| 22 |
4 13 20 21
|
syl3anbrc |
|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( A + B ) e. Z[i] ) |