Metamath Proof Explorer

Theorem lazlinz

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

Ref Expression
Assertion lazlinz 
|- ( S e. CC -> ( ( A e. ZZ /\ B e. ZZ ) -> ( A + ( B x. S ) ) e. ( Z[]l ` S ) ) )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( A e. ZZ -> A e. CC )
2 1 adantr 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> A e. CC )
3 2 adantl 
 |-  ( ( S e. CC /\ ( A e. ZZ /\ B e. ZZ ) ) -> A e. CC )
4 zcn 
 |-  ( B e. ZZ -> B e. CC )
5 4 adantl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> B e. CC )
6 5 adantl 
 |-  ( ( S e. CC /\ ( A e. ZZ /\ B e. ZZ ) ) -> B e. CC )
7 simpl 
 |-  ( ( S e. CC /\ ( A e. ZZ /\ B e. ZZ ) ) -> S e. CC )
8 6 7 mulcld 
 |-  ( ( S e. CC /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( B x. S ) e. CC )
9 3 8 addcld 
 |-  ( ( S e. CC /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( A + ( B x. S ) ) e. CC )
10 oveq1 
 |-  ( a = A -> ( a + ( b x. S ) ) = ( A + ( b x. S ) ) )
11 10 eqeq2d 
 |-  ( a = A -> ( ( A + ( B x. S ) ) = ( a + ( b x. S ) ) <-> ( A + ( B x. S ) ) = ( A + ( b x. S ) ) ) )
12 oveq1 
 |-  ( b = B -> ( b x. S ) = ( B x. S ) )
13 12 oveq2d 
 |-  ( b = B -> ( A + ( b x. S ) ) = ( A + ( B x. S ) ) )
14 13 eqeq2d 
 |-  ( b = B -> ( ( A + ( B x. S ) ) = ( A + ( b x. S ) ) <-> ( A + ( B x. S ) ) = ( A + ( B x. S ) ) ) )
15 simpl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> A e. ZZ )
16 15 adantl 
 |-  ( ( S e. CC /\ ( A e. ZZ /\ B e. ZZ ) ) -> A e. ZZ )
17 simprr 
 |-  ( ( S e. CC /\ ( A e. ZZ /\ B e. ZZ ) ) -> B e. ZZ )
18 eqidd 
 |-  ( ( S e. CC /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( A + ( B x. S ) ) = ( A + ( B x. S ) ) )
19 11 14 16 17 18 2rspcedvdw 
 |-  ( ( S e. CC /\ ( A e. ZZ /\ B e. ZZ ) ) -> E. a e. ZZ E. b e. ZZ ( A + ( B x. S ) ) = ( a + ( b x. S ) ) )
20 ellaz 
 |-  ( 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 ) ) ) ) )
21 20 adantr 
 |-  ( ( 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 ) ) ) ) )
22 9 19 21 mpbir2and 
 |-  ( ( S e. CC /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( A + ( B x. S ) ) e. ( Z[]l ` S ) )
23 22 ex 
 |-  ( S e. CC -> ( ( A e. ZZ /\ B e. ZZ ) -> ( A + ( B x. S ) ) e. ( Z[]l ` S ) ) )