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	Could not format assertion : No typesetting found for \|- Z[i] = ( Z[]l ` _i ) with typecode \|-

Proof

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

Metamath Proof Explorer

Theorem gzilaz

Proof