Theorem ellaz

Description: Elementhood in an adjunction of a complex number to the ring of integers. Such an element is also called "extended integer" in the following. (Contributed by AV, 24-Oct-2026)

	Ref	Expression
Assertion	ellaz	⊢ ( 𝑆 ∈ ℂ → ( 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lazval	⊢ ( 𝑆 ∈ ℂ → ( Z[]l ‘ 𝑆 ) = { 𝑥 ∈ ℂ ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) } )
2	1	eleq2d	⊢ ( 𝑆 ∈ ℂ → ( 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ↔ 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) } ) )
3		eqeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ↔ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) )
4	3	2rexbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) )
5		eqid	⊢ { 𝑥 ∈ ℂ ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) } = { 𝑥 ∈ ℂ ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) }
6	4 5	elrab2	⊢ ( 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) } ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) )
7	2 6	bitrdi	⊢ ( 𝑆 ∈ ℂ → ( 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) ) )