Theorem zellaz

Description: An integer is an extended integer. (Contributed by AV, 24-Oct-2026)

	Ref	Expression
Assertion	zellaz	Could not format assertion : No typesetting found for |- ( ( S e. CC /\ A e. ZZ ) -> A e. ( Z[]l ` S ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		zcn	$$⊢A\in \mathbb{Z}\to A\in ℂ$$
2	1	adantl	$$⊢\left(S\in ℂ\wedge A\in \mathbb{Z}\right)\to A\in ℂ$$
3		oveq1	$$⊢a=A\to a+bS=A+bS$$
4	3	eqeq2d	$$⊢a=A\to \left(A=a+bS\leftrightarrow A=A+bS\right)$$
5		oveq1	$$⊢b=0\to bS=0\cdot S$$
6	5	oveq2d	$$⊢b=0\to A+bS=A+0\cdot S$$
7	6	eqeq2d	$$⊢b=0\to \left(A=A+bS\leftrightarrow A=A+0\cdot S\right)$$
8		simpr	$$⊢\left(S\in ℂ\wedge A\in \mathbb{Z}\right)\to A\in \mathbb{Z}$$
9		0zd	$$⊢\left(S\in ℂ\wedge A\in \mathbb{Z}\right)\to 0\in \mathbb{Z}$$
10		simpl	$$⊢\left(S\in ℂ\wedge A\in \mathbb{Z}\right)\to S\in ℂ$$
11	10	mul02d	$$⊢\left(S\in ℂ\wedge A\in \mathbb{Z}\right)\to 0\cdot S=0$$
12	11	oveq2d	$$⊢\left(S\in ℂ\wedge A\in \mathbb{Z}\right)\to A+0\cdot S=A+0$$
13	2	addridd	$$⊢\left(S\in ℂ\wedge A\in \mathbb{Z}\right)\to A+0=A$$
14	12 13	eqtr2d	$$⊢\left(S\in ℂ\wedge A\in \mathbb{Z}\right)\to A=A+0\cdot S$$
15	4 7 8 9 14	2rspcedvdw	$$⊢\left(S\in ℂ\wedge A\in \mathbb{Z}\right)\to \exists a\in \mathbb{Z}\exists b\in \mathbb{Z}A=a+bS$$
16		ellaz	Could not format ( S e. CC -> ( A e. ( Z[]l ` S ) <-> ( A e. CC /\ E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) ) ) : No typesetting found for |- ( S e. CC -> ( A e. ( Z[]l ` S ) <-> ( A e. CC /\ E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) ) ) with typecode |-
17	16	adantr	Could not format ( ( S e. CC /\ A e. ZZ ) -> ( A e. ( Z[]l ` S ) <-> ( A e. CC /\ E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) ) ) : No typesetting found for |- ( ( S e. CC /\ A e. ZZ ) -> ( A e. ( Z[]l ` S ) <-> ( A e. CC /\ E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) ) ) with typecode |-
18	2 15 17	mpbir2and	Could not format ( ( S e. CC /\ A e. ZZ ) -> A e. ( Z[]l ` S ) ) : No typesetting found for |- ( ( S e. CC /\ A e. ZZ ) -> A e. ( Z[]l ` S ) ) with typecode |-