Metamath Proof Explorer

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

Proof

Step	Hyp	Ref	Expression
1		zcn	$⊢ S \in ℤ \to S \in ℂ$
2		ellaz	Could not format ( S e. CC -> ( s e. ( Z[]l ` S ) <-> ( s e. CC /\ E. a e. ZZ E. b e. ZZ s = ( a + ( b x. S ) ) ) ) ) : No typesetting found for \|- ( S e. CC -> ( s e. ( Z[]l ` S ) <-> ( s e. CC /\ E. a e. ZZ E. b e. ZZ s = ( a + ( b x. S ) ) ) ) ) with typecode \|-
3	1 2	syl	Could not format ( S e. ZZ -> ( s e. ( Z[]l ` S ) <-> ( s e. CC /\ E. a e. ZZ E. b e. ZZ s = ( a + ( b x. S ) ) ) ) ) : No typesetting found for \|- ( S e. ZZ -> ( s e. ( Z[]l ` S ) <-> ( s e. CC /\ E. a e. ZZ E. b e. ZZ s = ( a + ( b x. S ) ) ) ) ) with typecode \|-
4		simprl	$⊢ ((S \in ℤ \land s \in ℂ) \land (a \in ℤ \land b \in ℤ)) \to a \in ℤ$
5		simpr	$⊢ (a \in ℤ \land b \in ℤ) \to b \in ℤ$
6		simpl	$⊢ (S \in ℤ \land s \in ℂ) \to S \in ℤ$
7		zmulcl	$⊢ (b \in ℤ \land S \in ℤ) \to b S \in ℤ$
8	5 6 7	syl2anr	$⊢ ((S \in ℤ \land s \in ℂ) \land (a \in ℤ \land b \in ℤ)) \to b S \in ℤ$
9	4 8	zaddcld	$⊢ ((S \in ℤ \land s \in ℂ) \land (a \in ℤ \land b \in ℤ)) \to a + b S \in ℤ$
10		eleq1	$⊢ s = a + b S \to (s \in ℤ \leftrightarrow a + b S \in ℤ)$
11	9 10	syl5ibrcom	$⊢ ((S \in ℤ \land s \in ℂ) \land (a \in ℤ \land b \in ℤ)) \to (s = a + b S \to s \in ℤ)$
12	11	rexlimdvva	$⊢ (S \in ℤ \land s \in ℂ) \to (\exists a \in ℤ \exists b \in ℤ s = a + b S \to s \in ℤ)$
13	12	expimpd	$⊢ S \in ℤ \to ((s \in ℂ \land \exists a \in ℤ \exists b \in ℤ s = a + b S) \to s \in ℤ)$
14	3 13	sylbid	Could not format ( S e. ZZ -> ( s e. ( Z[]l ` S ) -> s e. ZZ ) ) : No typesetting found for \|- ( S e. ZZ -> ( s e. ( Z[]l ` S ) -> s e. ZZ ) ) with typecode \|-
15		zellaz	Could not format ( ( S e. CC /\ s e. ZZ ) -> s e. ( Z[]l ` S ) ) : No typesetting found for \|- ( ( S e. CC /\ s e. ZZ ) -> s e. ( Z[]l ` S ) ) with typecode \|-
16	15	ex	Could not format ( S e. CC -> ( s e. ZZ -> s e. ( Z[]l ` S ) ) ) : No typesetting found for \|- ( S e. CC -> ( s e. ZZ -> s e. ( Z[]l ` S ) ) ) with typecode \|-
17	1 16	syl	Could not format ( S e. ZZ -> ( s e. ZZ -> s e. ( Z[]l ` S ) ) ) : No typesetting found for \|- ( S e. ZZ -> ( s e. ZZ -> s e. ( Z[]l ` S ) ) ) with typecode \|-
18	14 17	impbid	Could not format ( S e. ZZ -> ( s e. ( Z[]l ` S ) <-> s e. ZZ ) ) : No typesetting found for \|- ( S e. ZZ -> ( s e. ( Z[]l ` S ) <-> s e. ZZ ) ) with typecode \|-
19	18	eqrdv	Could not format ( S e. ZZ -> ( Z[]l ` S ) = ZZ ) : No typesetting found for \|- ( S e. ZZ -> ( Z[]l ` S ) = ZZ ) with typecode \|-