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	|- ( S e. ZZ -> ( Z[]l ` S ) = ZZ )

Proof

Step	Hyp	Ref	Expression
1		zcn	|- ( S e. ZZ -> S e. CC )
2		ellaz	|- ( S e. CC -> ( s e. ( Z[]l ` S ) <-> ( s e. CC /\ E. a e. ZZ E. b e. ZZ s = ( a + ( b x. S ) ) ) ) )
3	1 2	syl	|- ( S e. ZZ -> ( s e. ( Z[]l ` S ) <-> ( s e. CC /\ E. a e. ZZ E. b e. ZZ s = ( a + ( b x. S ) ) ) ) )
4		simprl	|- ( ( ( S e. ZZ /\ s e. CC ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. ZZ )
5		simpr	|- ( ( a e. ZZ /\ b e. ZZ ) -> b e. ZZ )
6		simpl	|- ( ( S e. ZZ /\ s e. CC ) -> S e. ZZ )
7		zmulcl	|- ( ( b e. ZZ /\ S e. ZZ ) -> ( b x. S ) e. ZZ )
8	5 6 7	syl2anr	|- ( ( ( S e. ZZ /\ s e. CC ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( b x. S ) e. ZZ )
9	4 8	zaddcld	|- ( ( ( S e. ZZ /\ s e. CC ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a + ( b x. S ) ) e. ZZ )
10		eleq1	|- ( s = ( a + ( b x. S ) ) -> ( s e. ZZ <-> ( a + ( b x. S ) ) e. ZZ ) )
11	9 10	syl5ibrcom	|- ( ( ( S e. ZZ /\ s e. CC ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( s = ( a + ( b x. S ) ) -> s e. ZZ ) )
12	11	rexlimdvva	|- ( ( S e. ZZ /\ s e. CC ) -> ( E. a e. ZZ E. b e. ZZ s = ( a + ( b x. S ) ) -> s e. ZZ ) )
13	12	expimpd	|- ( S e. ZZ -> ( ( s e. CC /\ E. a e. ZZ E. b e. ZZ s = ( a + ( b x. S ) ) ) -> s e. ZZ ) )
14	3 13	sylbid	|- ( S e. ZZ -> ( s e. ( Z[]l ` S ) -> s e. ZZ ) )
15		zellaz	|- ( ( S e. CC /\ s e. ZZ ) -> s e. ( Z[]l ` S ) )
16	15	ex	|- ( S e. CC -> ( s e. ZZ -> s e. ( Z[]l ` S ) ) )
17	1 16	syl	|- ( S e. ZZ -> ( s e. ZZ -> s e. ( Z[]l ` S ) ) )
18	14 17	impbid	|- ( S e. ZZ -> ( s e. ( Z[]l ` S ) <-> s e. ZZ ) )
19	18	eqrdv	|- ( S e. ZZ -> ( Z[]l ` S ) = ZZ )