Metamath Proof Explorer

Theorem lazaddcl

Description: The extended integers are closed under addition. (Contributed by AV, 25-Oct-2026)

Ref Expression
Hypothesis laznegcl.r 
|- R = ( Z[]l ` S )
Assertion lazaddcl 
|- ( S e. CC -> ( ( A e. R /\ B e. R ) -> ( A + B ) 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 1 eleq2i 
 |-  ( B e. R <-> B e. ( Z[]l ` S ) )
4 2 3 anbi12i 
 |-  ( ( A e. R /\ B e. R ) <-> ( A e. ( Z[]l ` S ) /\ B e. ( Z[]l ` S ) ) )
5 ellazim 
 |-  ( ( S e. CC /\ A e. ( Z[]l ` S ) ) -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) )
6 5 ex 
 |-  ( S e. CC -> ( A e. ( Z[]l ` S ) -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) )
7 ellazim 
 |-  ( ( S e. CC /\ B e. ( Z[]l ` S ) ) -> E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) )
8 7 ex 
 |-  ( S e. CC -> ( B e. ( Z[]l ` S ) -> E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) ) )
9 simpl 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> S e. CC )
10 9 adantr 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> S e. CC )
11 simpl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> a e. ZZ )
12 11 adantl 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. ZZ )
13 simpl 
 |-  ( ( c e. ZZ /\ d e. ZZ ) -> c e. ZZ )
14 zaddcl 
 |-  ( ( a e. ZZ /\ c e. ZZ ) -> ( a + c ) e. ZZ )
15 12 13 14 syl2an 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( a + c ) e. ZZ )
16 simpr 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> b e. ZZ )
17 16 adantl 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. ZZ )
18 simpr 
 |-  ( ( c e. ZZ /\ d e. ZZ ) -> d e. ZZ )
19 zaddcl 
 |-  ( ( b e. ZZ /\ d e. ZZ ) -> ( b + d ) e. ZZ )
20 17 18 19 syl2an 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( b + d ) e. ZZ )
21 15 20 jca 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( a + c ) e. ZZ /\ ( b + d ) e. ZZ ) )
22 lazlinz 
 |-  ( S e. CC -> ( ( ( a + c ) e. ZZ /\ ( b + d ) e. ZZ ) -> ( ( a + c ) + ( ( b + d ) x. S ) ) e. ( Z[]l ` S ) ) )
23 10 21 22 sylc 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( a + c ) + ( ( b + d ) x. S ) ) e. ( Z[]l ` S ) )
24 zcn 
 |-  ( a e. ZZ -> a e. CC )
25 24 ad2antrl 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. CC )
26 25 adantr 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> a e. CC )
27 zcn 
 |-  ( b e. ZZ -> b e. CC )
28 27 ad2antll 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. CC )
29 28 adantr 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> b e. CC )
30 29 10 mulcld 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( b x. S ) e. CC )
31 zcn 
 |-  ( c e. ZZ -> c e. CC )
32 31 ad2antrl 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> c e. CC )
33 zcn 
 |-  ( d e. ZZ -> d e. CC )
34 33 ad2antll 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> d e. CC )
35 34 10 mulcld 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( d x. S ) e. CC )
36 26 30 32 35 add4d 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( a + ( b x. S ) ) + ( c + ( d x. S ) ) ) = ( ( a + c ) + ( ( b x. S ) + ( d x. S ) ) ) )
37 29 34 10 adddird 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( b + d ) x. S ) = ( ( b x. S ) + ( d x. S ) ) )
38 37 eqcomd 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( b x. S ) + ( d x. S ) ) = ( ( b + d ) x. S ) )
39 38 oveq2d 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( a + c ) + ( ( b x. S ) + ( d x. S ) ) ) = ( ( a + c ) + ( ( b + d ) x. S ) ) )
40 36 39 eqtrd 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( a + ( b x. S ) ) + ( c + ( d x. S ) ) ) = ( ( a + c ) + ( ( b + d ) x. S ) ) )
41 1 a1i 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> R = ( Z[]l ` S ) )
42 23 40 41 3eltr4d 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( a + ( b x. S ) ) + ( c + ( d x. S ) ) ) e. R )
43 oveq12 
 |-  ( ( A = ( a + ( b x. S ) ) /\ B = ( c + ( d x. S ) ) ) -> ( A + B ) = ( ( a + ( b x. S ) ) + ( c + ( d x. S ) ) ) )
44 43 eleq1d 
 |-  ( ( A = ( a + ( b x. S ) ) /\ B = ( c + ( d x. S ) ) ) -> ( ( A + B ) e. R <-> ( ( a + ( b x. S ) ) + ( c + ( d x. S ) ) ) e. R ) )
45 44 ancoms 
 |-  ( ( B = ( c + ( d x. S ) ) /\ A = ( a + ( b x. S ) ) ) -> ( ( A + B ) e. R <-> ( ( a + ( b x. S ) ) + ( c + ( d x. S ) ) ) e. R ) )
46 42 45 syl5ibrcom 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( B = ( c + ( d x. S ) ) /\ A = ( a + ( b x. S ) ) ) -> ( A + B ) e. R ) )
47 46 expd 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( B = ( c + ( d x. S ) ) -> ( A = ( a + ( b x. S ) ) -> ( A + B ) e. R ) ) )
48 47 rexlimdvva 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) -> ( A = ( a + ( b x. S ) ) -> ( A + B ) e. R ) ) )
49 48 com23 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( A = ( a + ( b x. S ) ) -> ( E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) -> ( A + B ) e. R ) ) )
50 49 rexlimdvva 
 |-  ( S e. CC -> ( E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) -> ( E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) -> ( A + B ) e. R ) ) )
51 50 impd 
 |-  ( S e. CC -> ( ( E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) /\ E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) ) -> ( A + B ) e. R ) )
52 6 8 51 syl2and 
 |-  ( S e. CC -> ( ( A e. ( Z[]l ` S ) /\ B e. ( Z[]l ` S ) ) -> ( A + B ) e. R ) )
53 4 52 biimtrid 
 |-  ( S e. CC -> ( ( A e. R /\ B e. R ) -> ( A + B ) e. R ) )