Theorem adcnlaz

Description: The adjunction of an integer to the ring of integers yields the integers. (Contributed by AV, 25-Oct-2026)

	Ref	Expression
Assertion	adcnlaz	⊢ ( 𝑆 ∈ ℤ → ( Z[]l ‘ 𝑆 ) = ℤ )

Proof

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝑆 ∈ ℤ → 𝑆 ∈ ℂ )
2		ellaz	⊢ ( 𝑆 ∈ ℂ → ( 𝑠 ∈ ( Z[]l ‘ 𝑆 ) ↔ ( 𝑠 ∈ ℂ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑠 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) ) )
3	1 2	syl	⊢ ( 𝑆 ∈ ℤ → ( 𝑠 ∈ ( Z[]l ‘ 𝑆 ) ↔ ( 𝑠 ∈ ℂ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑠 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) ) )
4		simprl	⊢ ( ( ( 𝑆 ∈ ℤ ∧ 𝑠 ∈ ℂ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℤ )
5		simpr	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 𝑏 ∈ ℤ )
6		simpl	⊢ ( ( 𝑆 ∈ ℤ ∧ 𝑠 ∈ ℂ ) → 𝑆 ∈ ℤ )
7		zmulcl	⊢ ( ( 𝑏 ∈ ℤ ∧ 𝑆 ∈ ℤ ) → ( 𝑏 · 𝑆 ) ∈ ℤ )
8	5 6 7	syl2anr	⊢ ( ( ( 𝑆 ∈ ℤ ∧ 𝑠 ∈ ℂ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑏 · 𝑆 ) ∈ ℤ )
9	4 8	zaddcld	⊢ ( ( ( 𝑆 ∈ ℤ ∧ 𝑠 ∈ ℂ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∈ ℤ )
10		eleq1	⊢ ( 𝑠 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → ( 𝑠 ∈ ℤ ↔ ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∈ ℤ ) )
11	9 10	syl5ibrcom	⊢ ( ( ( 𝑆 ∈ ℤ ∧ 𝑠 ∈ ℂ ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑠 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → 𝑠 ∈ ℤ ) )
12	11	rexlimdvva	⊢ ( ( 𝑆 ∈ ℤ ∧ 𝑠 ∈ ℂ ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑠 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → 𝑠 ∈ ℤ ) )
13	12	expimpd	⊢ ( 𝑆 ∈ ℤ → ( ( 𝑠 ∈ ℂ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑠 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) → 𝑠 ∈ ℤ ) )
14	3 13	sylbid	⊢ ( 𝑆 ∈ ℤ → ( 𝑠 ∈ ( Z[]l ‘ 𝑆 ) → 𝑠 ∈ ℤ ) )
15		zellaz	⊢ ( ( 𝑆 ∈ ℂ ∧ 𝑠 ∈ ℤ ) → 𝑠 ∈ ( Z[]l ‘ 𝑆 ) )
16	15	ex	⊢ ( 𝑆 ∈ ℂ → ( 𝑠 ∈ ℤ → 𝑠 ∈ ( Z[]l ‘ 𝑆 ) ) )
17	1 16	syl	⊢ ( 𝑆 ∈ ℤ → ( 𝑠 ∈ ℤ → 𝑠 ∈ ( Z[]l ‘ 𝑆 ) ) )
18	14 17	impbid	⊢ ( 𝑆 ∈ ℤ → ( 𝑠 ∈ ( Z[]l ‘ 𝑆 ) ↔ 𝑠 ∈ ℤ ) )
19	18	eqrdv	⊢ ( 𝑆 ∈ ℤ → ( Z[]l ‘ 𝑆 ) = ℤ )