Metamath Proof Explorer

Theorem gzilaz

Description: The Gaussian integers are the adjunction of _i to the ring of integers. (Contributed by AV, 25-Oct-2026)

Ref Expression
Assertion gzilaz 
|- Z[i] = ( Z[]l ` _i )

Proof

Step Hyp Ref Expression
1 3anass 
 |-  ( ( s e. CC /\ ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) <-> ( s e. CC /\ ( ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) ) )
2 oveq1 
 |-  ( a = ( Re ` s ) -> ( a + ( b x. _i ) ) = ( ( Re ` s ) + ( b x. _i ) ) )
3 2 eqeq2d 
 |-  ( a = ( Re ` s ) -> ( s = ( a + ( b x. _i ) ) <-> s = ( ( Re ` s ) + ( b x. _i ) ) ) )
4 oveq1 
 |-  ( b = ( Im ` s ) -> ( b x. _i ) = ( ( Im ` s ) x. _i ) )
5 4 oveq2d 
 |-  ( b = ( Im ` s ) -> ( ( Re ` s ) + ( b x. _i ) ) = ( ( Re ` s ) + ( ( Im ` s ) x. _i ) ) )
6 5 eqeq2d 
 |-  ( b = ( Im ` s ) -> ( s = ( ( Re ` s ) + ( b x. _i ) ) <-> s = ( ( Re ` s ) + ( ( Im ` s ) x. _i ) ) ) )
7 simprl 
 |-  ( ( s e. CC /\ ( ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) ) -> ( Re ` s ) e. ZZ )
8 simprr 
 |-  ( ( s e. CC /\ ( ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) ) -> ( Im ` s ) e. ZZ )
9 simpl 
 |-  ( ( s e. CC /\ ( ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) ) -> s e. CC )
10 9 replimd 
 |-  ( ( s e. CC /\ ( ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) ) -> s = ( ( Re ` s ) + ( _i x. ( Im ` s ) ) ) )
11 ax-icn 
 |-  _i e. CC
12 11 a1i 
 |-  ( ( s e. CC /\ ( ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) ) -> _i e. CC )
13 zcn 
 |-  ( ( Im ` s ) e. ZZ -> ( Im ` s ) e. CC )
14 13 ad2antll 
 |-  ( ( s e. CC /\ ( ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) ) -> ( Im ` s ) e. CC )
15 12 14 mulcomd 
 |-  ( ( s e. CC /\ ( ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) ) -> ( _i x. ( Im ` s ) ) = ( ( Im ` s ) x. _i ) )
16 15 oveq2d 
 |-  ( ( s e. CC /\ ( ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) ) -> ( ( Re ` s ) + ( _i x. ( Im ` s ) ) ) = ( ( Re ` s ) + ( ( Im ` s ) x. _i ) ) )
17 10 16 eqtrd 
 |-  ( ( s e. CC /\ ( ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) ) -> s = ( ( Re ` s ) + ( ( Im ` s ) x. _i ) ) )
18 3 6 7 8 17 2rspcedvdw 
 |-  ( ( s e. CC /\ ( ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) ) -> E. a e. ZZ E. b e. ZZ s = ( a + ( b x. _i ) ) )
19 18 ex 
 |-  ( s e. CC -> ( ( ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) -> E. a e. ZZ E. b e. ZZ s = ( a + ( b x. _i ) ) ) )
20 zcn 
 |-  ( b e. ZZ -> b e. CC )
21 20 ad2antll 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. CC )
22 11 a1i 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> _i e. CC )
23 21 22 mulcomd 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( b x. _i ) = ( _i x. b ) )
24 23 oveq2d 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a + ( b x. _i ) ) = ( a + ( _i x. b ) ) )
25 24 fveq2d 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( Re ` ( a + ( b x. _i ) ) ) = ( Re ` ( a + ( _i x. b ) ) ) )
26 zre 
 |-  ( a e. ZZ -> a e. RR )
27 26 ad2antrl 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. RR )
28 zre 
 |-  ( b e. ZZ -> b e. RR )
29 28 ad2antll 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. RR )
30 27 29 crred 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( Re ` ( a + ( _i x. b ) ) ) = a )
31 25 30 eqtrd 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( Re ` ( a + ( b x. _i ) ) ) = a )
32 simprl 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. ZZ )
33 31 32 eqeltrd 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( Re ` ( a + ( b x. _i ) ) ) e. ZZ )
34 24 fveq2d 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( Im ` ( a + ( b x. _i ) ) ) = ( Im ` ( a + ( _i x. b ) ) ) )
35 27 29 crimd 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( Im ` ( a + ( _i x. b ) ) ) = b )
36 34 35 eqtrd 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( Im ` ( a + ( b x. _i ) ) ) = b )
37 simprr 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. ZZ )
38 36 37 eqeltrd 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( Im ` ( a + ( b x. _i ) ) ) e. ZZ )
39 33 38 jca 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( Re ` ( a + ( b x. _i ) ) ) e. ZZ /\ ( Im ` ( a + ( b x. _i ) ) ) e. ZZ ) )
40 fveq2 
 |-  ( s = ( a + ( b x. _i ) ) -> ( Re ` s ) = ( Re ` ( a + ( b x. _i ) ) ) )
41 40 eleq1d 
 |-  ( s = ( a + ( b x. _i ) ) -> ( ( Re ` s ) e. ZZ <-> ( Re ` ( a + ( b x. _i ) ) ) e. ZZ ) )
42 fveq2 
 |-  ( s = ( a + ( b x. _i ) ) -> ( Im ` s ) = ( Im ` ( a + ( b x. _i ) ) ) )
43 42 eleq1d 
 |-  ( s = ( a + ( b x. _i ) ) -> ( ( Im ` s ) e. ZZ <-> ( Im ` ( a + ( b x. _i ) ) ) e. ZZ ) )
44 41 43 anbi12d 
 |-  ( s = ( a + ( b x. _i ) ) -> ( ( ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) <-> ( ( Re ` ( a + ( b x. _i ) ) ) e. ZZ /\ ( Im ` ( a + ( b x. _i ) ) ) e. ZZ ) ) )
45 39 44 syl5ibrcom 
 |-  ( ( s e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( s = ( a + ( b x. _i ) ) -> ( ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) ) )
46 45 rexlimdvva 
 |-  ( s e. CC -> ( E. a e. ZZ E. b e. ZZ s = ( a + ( b x. _i ) ) -> ( ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) ) )
47 19 46 impbid 
 |-  ( s e. CC -> ( ( ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) <-> E. a e. ZZ E. b e. ZZ s = ( a + ( b x. _i ) ) ) )
48 47 pm5.32i 
 |-  ( ( s e. CC /\ ( ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) ) <-> ( s e. CC /\ E. a e. ZZ E. b e. ZZ s = ( a + ( b x. _i ) ) ) )
49 1 48 bitri 
 |-  ( ( s e. CC /\ ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) <-> ( s e. CC /\ E. a e. ZZ E. b e. ZZ s = ( a + ( b x. _i ) ) ) )
50 elgz 
 |-  ( s e. Z[i] <-> ( s e. CC /\ ( Re ` s ) e. ZZ /\ ( Im ` s ) e. ZZ ) )
51 ellaz 
 |-  ( _i e. CC -> ( s e. ( Z[]l ` _i ) <-> ( s e. CC /\ E. a e. ZZ E. b e. ZZ s = ( a + ( b x. _i ) ) ) ) )
52 11 51 ax-mp 
 |-  ( s e. ( Z[]l ` _i ) <-> ( s e. CC /\ E. a e. ZZ E. b e. ZZ s = ( a + ( b x. _i ) ) ) )
53 49 50 52 3bitr4i 
 |-  ( s e. Z[i] <-> s e. ( Z[]l ` _i ) )
54 53 eqriv 
 |-  Z[i] = ( Z[]l ` _i )