Metamath Proof Explorer

Theorem lazmulzcl

Description: The extended integers are closed under multiplication with an integer. (Contributed by AV, 25-Oct-2026)

Ref Expression
Hypothesis laznegcl.r 
|- R = ( Z[]l ` S )
Assertion lazmulzcl 
|- ( S e. CC -> ( ( B e. ZZ /\ A e. R ) -> ( B x. A ) e. R ) )

Proof

Step Hyp Ref Expression
1 laznegcl.r 
 |-  R = ( Z[]l ` S )
2 1 eleq2i 
 |-  ( A e. R <-> A e. ( Z[]l ` S ) )
3 ellazim 
 |-  ( ( S e. CC /\ A e. ( Z[]l ` S ) ) -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) )
4 3 ex 
 |-  ( S e. CC -> ( A e. ( Z[]l ` S ) -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) )
5 4 adantr 
 |-  ( ( S e. CC /\ B e. ZZ ) -> ( A e. ( Z[]l ` S ) -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) )
6 2 5 biimtrid 
 |-  ( ( S e. CC /\ B e. ZZ ) -> ( A e. R -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) )
7 zcn 
 |-  ( B e. ZZ -> B e. CC )
8 7 adantl 
 |-  ( ( S e. CC /\ B e. ZZ ) -> B e. CC )
9 8 adantr 
 |-  ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> B e. CC )
10 zcn 
 |-  ( b e. ZZ -> b e. CC )
11 10 adantl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> b e. CC )
12 11 adantl 
 |-  ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. CC )
13 simpll 
 |-  ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> S e. CC )
14 9 12 13 mulassd 
 |-  ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( B x. b ) x. S ) = ( B x. ( b x. S ) ) )
15 14 eqcomd 
 |-  ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( B x. ( b x. S ) ) = ( ( B x. b ) x. S ) )
16 15 oveq2d 
 |-  ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( B x. a ) + ( B x. ( b x. S ) ) ) = ( ( B x. a ) + ( ( B x. b ) x. S ) ) )
17 zmulcl 
 |-  ( ( B e. ZZ /\ a e. ZZ ) -> ( B x. a ) e. ZZ )
18 17 ad2ant2lr 
 |-  ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( B x. a ) e. ZZ )
19 zmulcl 
 |-  ( ( B e. ZZ /\ b e. ZZ ) -> ( B x. b ) e. ZZ )
20 19 ad2ant2l 
 |-  ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( B x. b ) e. ZZ )
21 18 20 jca 
 |-  ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( B x. a ) e. ZZ /\ ( B x. b ) e. ZZ ) )
22 lazlinz 
 |-  ( S e. CC -> ( ( ( B x. a ) e. ZZ /\ ( B x. b ) e. ZZ ) -> ( ( B x. a ) + ( ( B x. b ) x. S ) ) e. ( Z[]l ` S ) ) )
23 13 21 22 sylc 
 |-  ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( B x. a ) + ( ( B x. b ) x. S ) ) e. ( Z[]l ` S ) )
24 16 23 eqeltrd 
 |-  ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( B x. a ) + ( B x. ( b x. S ) ) ) e. ( Z[]l ` S ) )
25 zcn 
 |-  ( a e. ZZ -> a e. CC )
26 25 adantr 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> a e. CC )
27 26 adantl 
 |-  ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. CC )
28 simpl 
 |-  ( ( S e. CC /\ B e. ZZ ) -> S e. CC )
29 mulcl 
 |-  ( ( b e. CC /\ S e. CC ) -> ( b x. S ) e. CC )
30 11 28 29 syl2anr 
 |-  ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( b x. S ) e. CC )
31 9 27 30 adddid 
 |-  ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( B x. ( a + ( b x. S ) ) ) = ( ( B x. a ) + ( B x. ( b x. S ) ) ) )
32 1 a1i 
 |-  ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> R = ( Z[]l ` S ) )
33 24 31 32 3eltr4d 
 |-  ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( B x. ( a + ( b x. S ) ) ) e. R )
34 oveq2 
 |-  ( A = ( a + ( b x. S ) ) -> ( B x. A ) = ( B x. ( a + ( b x. S ) ) ) )
35 34 eleq1d 
 |-  ( A = ( a + ( b x. S ) ) -> ( ( B x. A ) e. R <-> ( B x. ( a + ( b x. S ) ) ) e. R ) )
36 33 35 syl5ibrcom 
 |-  ( ( ( S e. CC /\ B e. ZZ ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( A = ( a + ( b x. S ) ) -> ( B x. A ) e. R ) )
37 36 rexlimdvva 
 |-  ( ( S e. CC /\ B e. ZZ ) -> ( E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) -> ( B x. A ) e. R ) )
38 6 37 syld 
 |-  ( ( S e. CC /\ B e. ZZ ) -> ( A e. R -> ( B x. A ) e. R ) )
39 38 expimpd 
 |-  ( S e. CC -> ( ( B e. ZZ /\ A e. R ) -> ( B x. A ) e. R ) )