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 ℤ[i] = ( Z[]l ‘ i )

Proof

Step Hyp Ref Expression
1 3anass ⊢ ( ( 𝑠 ∈ ℂ ∧ ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ↔ ( 𝑠 ∈ ℂ ∧ ( ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ) )
2 oveq1 ⊢ ( 𝑎 = ( ℜ ‘ 𝑠 ) → ( 𝑎 + ( 𝑏 · i ) ) = ( ( ℜ ‘ 𝑠 ) + ( 𝑏 · i ) ) )
3 2 eqeq2d ⊢ ( 𝑎 = ( ℜ ‘ 𝑠 ) → ( 𝑠 = ( 𝑎 + ( 𝑏 · i ) ) ↔ 𝑠 = ( ( ℜ ‘ 𝑠 ) + ( 𝑏 · i ) ) ) )
4 oveq1 ⊢ ( 𝑏 = ( ℑ ‘ 𝑠 ) → ( 𝑏 · i ) = ( ( ℑ ‘ 𝑠 ) · i ) )
5 4 oveq2d ⊢ ( 𝑏 = ( ℑ ‘ 𝑠 ) → ( ( ℜ ‘ 𝑠 ) + ( 𝑏 · i ) ) = ( ( ℜ ‘ 𝑠 ) + ( ( ℑ ‘ 𝑠 ) · i ) ) )
6 5 eqeq2d ⊢ ( 𝑏 = ( ℑ ‘ 𝑠 ) → ( 𝑠 = ( ( ℜ ‘ 𝑠 ) + ( 𝑏 · i ) ) ↔ 𝑠 = ( ( ℜ ‘ 𝑠 ) + ( ( ℑ ‘ 𝑠 ) · i ) ) ) )
7 simprl ⊢ ( ( 𝑠 ∈ ℂ ∧ ( ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ) → ( ℜ ‘ 𝑠 ) ∈ ℤ )
8 simprr ⊢ ( ( 𝑠 ∈ ℂ ∧ ( ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ) → ( ℑ ‘ 𝑠 ) ∈ ℤ )
9 simpl ⊢ ( ( 𝑠 ∈ ℂ ∧ ( ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ) → 𝑠 ∈ ℂ )
10 9 replimd ⊢ ( ( 𝑠 ∈ ℂ ∧ ( ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ) → 𝑠 = ( ( ℜ ‘ 𝑠 ) + ( i · ( ℑ ‘ 𝑠 ) ) ) )
11 ax-icn ⊢ i ∈ ℂ
12 11 a1i ⊢ ( ( 𝑠 ∈ ℂ ∧ ( ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ) → i ∈ ℂ )
13 zcn ⊢ ( ( ℑ ‘ 𝑠 ) ∈ ℤ → ( ℑ ‘ 𝑠 ) ∈ ℂ )
14 13 ad2antll ⊢ ( ( 𝑠 ∈ ℂ ∧ ( ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ) → ( ℑ ‘ 𝑠 ) ∈ ℂ )
15 12 14 mulcomd ⊢ ( ( 𝑠 ∈ ℂ ∧ ( ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ) → ( i · ( ℑ ‘ 𝑠 ) ) = ( ( ℑ ‘ 𝑠 ) · i ) )
16 15 oveq2d ⊢ ( ( 𝑠 ∈ ℂ ∧ ( ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ) → ( ( ℜ ‘ 𝑠 ) + ( i · ( ℑ ‘ 𝑠 ) ) ) = ( ( ℜ ‘ 𝑠 ) + ( ( ℑ ‘ 𝑠 ) · i ) ) )
17 10 16 eqtrd ⊢ ( ( 𝑠 ∈ ℂ ∧ ( ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ) → 𝑠 = ( ( ℜ ‘ 𝑠 ) + ( ( ℑ ‘ 𝑠 ) · i ) ) )
18 3 6 7 8 17 2rspcedvdw ⊢ ( ( 𝑠 ∈ ℂ ∧ ( ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑠 = ( 𝑎 + ( 𝑏 · i ) ) )
19 18 ex ⊢ ( 𝑠 ∈ ℂ → ( ( ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑠 = ( 𝑎 + ( 𝑏 · i ) ) ) )
20 zcn ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
21 20 ad2antll ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℂ )
22 11 a1i ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → i ∈ ℂ )
23 21 22 mulcomd ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑏 · i ) = ( i · 𝑏 ) )
24 23 oveq2d ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 + ( 𝑏 · i ) ) = ( 𝑎 + ( i · 𝑏 ) ) )
25 24 fveq2d ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ℜ ‘ ( 𝑎 + ( 𝑏 · i ) ) ) = ( ℜ ‘ ( 𝑎 + ( i · 𝑏 ) ) ) )
26 zre ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℝ )
27 26 ad2antrl ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℝ )
28 zre ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℝ )
29 28 ad2antll ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℝ )
30 27 29 crred ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ℜ ‘ ( 𝑎 + ( i · 𝑏 ) ) ) = 𝑎 )
31 25 30 eqtrd ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ℜ ‘ ( 𝑎 + ( 𝑏 · i ) ) ) = 𝑎 )
32 simprl ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℤ )
33 31 32 eqeltrd ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ℜ ‘ ( 𝑎 + ( 𝑏 · i ) ) ) ∈ ℤ )
34 24 fveq2d ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ℑ ‘ ( 𝑎 + ( 𝑏 · i ) ) ) = ( ℑ ‘ ( 𝑎 + ( i · 𝑏 ) ) ) )
35 27 29 crimd ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ℑ ‘ ( 𝑎 + ( i · 𝑏 ) ) ) = 𝑏 )
36 34 35 eqtrd ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ℑ ‘ ( 𝑎 + ( 𝑏 · i ) ) ) = 𝑏 )
37 simprr ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℤ )
38 36 37 eqeltrd ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ℑ ‘ ( 𝑎 + ( 𝑏 · i ) ) ) ∈ ℤ )
39 33 38 jca ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( ℜ ‘ ( 𝑎 + ( 𝑏 · i ) ) ) ∈ ℤ ∧ ( ℑ ‘ ( 𝑎 + ( 𝑏 · i ) ) ) ∈ ℤ ) )
40 fveq2 ⊢ ( 𝑠 = ( 𝑎 + ( 𝑏 · i ) ) → ( ℜ ‘ 𝑠 ) = ( ℜ ‘ ( 𝑎 + ( 𝑏 · i ) ) ) )
41 40 eleq1d ⊢ ( 𝑠 = ( 𝑎 + ( 𝑏 · i ) ) → ( ( ℜ ‘ 𝑠 ) ∈ ℤ ↔ ( ℜ ‘ ( 𝑎 + ( 𝑏 · i ) ) ) ∈ ℤ ) )
42 fveq2 ⊢ ( 𝑠 = ( 𝑎 + ( 𝑏 · i ) ) → ( ℑ ‘ 𝑠 ) = ( ℑ ‘ ( 𝑎 + ( 𝑏 · i ) ) ) )
43 42 eleq1d ⊢ ( 𝑠 = ( 𝑎 + ( 𝑏 · i ) ) → ( ( ℑ ‘ 𝑠 ) ∈ ℤ ↔ ( ℑ ‘ ( 𝑎 + ( 𝑏 · i ) ) ) ∈ ℤ ) )
44 41 43 anbi12d ⊢ ( 𝑠 = ( 𝑎 + ( 𝑏 · i ) ) → ( ( ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ↔ ( ( ℜ ‘ ( 𝑎 + ( 𝑏 · i ) ) ) ∈ ℤ ∧ ( ℑ ‘ ( 𝑎 + ( 𝑏 · i ) ) ) ∈ ℤ ) ) )
45 39 44 syl5ibrcom ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑠 = ( 𝑎 + ( 𝑏 · i ) ) → ( ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ) )
46 45 rexlimdvva ⊢ ( 𝑠 ∈ ℂ → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑠 = ( 𝑎 + ( 𝑏 · i ) ) → ( ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ) )
47 19 46 impbid ⊢ ( 𝑠 ∈ ℂ → ( ( ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑠 = ( 𝑎 + ( 𝑏 · i ) ) ) )
48 47 pm5.32i ⊢ ( ( 𝑠 ∈ ℂ ∧ ( ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ) ↔ ( 𝑠 ∈ ℂ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑠 = ( 𝑎 + ( 𝑏 · i ) ) ) )
49 1 48 bitri ⊢ ( ( 𝑠 ∈ ℂ ∧ ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) ↔ ( 𝑠 ∈ ℂ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑠 = ( 𝑎 + ( 𝑏 · i ) ) ) )
50 elgz ⊢ ( 𝑠 ∈ ℤ[i] ↔ ( 𝑠 ∈ ℂ ∧ ( ℜ ‘ 𝑠 ) ∈ ℤ ∧ ( ℑ ‘ 𝑠 ) ∈ ℤ ) )
51 ellaz ⊢ ( i ∈ ℂ → ( 𝑠 ∈ ( Z[]l ‘ i ) ↔ ( 𝑠 ∈ ℂ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑠 = ( 𝑎 + ( 𝑏 · i ) ) ) ) )
52 11 51 ax-mp ⊢ ( 𝑠 ∈ ( Z[]l ‘ i ) ↔ ( 𝑠 ∈ ℂ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑠 = ( 𝑎 + ( 𝑏 · i ) ) ) )
53 49 50 52 3bitr4i ⊢ ( 𝑠 ∈ ℤ[i] ↔ 𝑠 ∈ ( Z[]l ‘ i ) )
54 53 eqriv ⊢ ℤ[i] = ( Z[]l ‘ i )