Theorem lazlinz

Description: Construct an extended integer. (Contributed by AV, 25-Oct-2026)

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

Proof

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