Metamath Proof Explorer

Theorem laznegcl

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

Ref Expression
Hypothesis laznegcl.r 
|- R = ( Z[]l ` S )
Assertion laznegcl 
|- ( S e. CC -> ( A e. R -> -u 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 negeq 
 |-  ( A = ( a + ( b x. S ) ) -> -u A = -u ( a + ( b x. S ) ) )
5 zcn 
 |-  ( a e. ZZ -> a e. CC )
6 5 adantr 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> a e. CC )
7 6 adantl 
 |-  ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. CC )
8 zcn 
 |-  ( b e. ZZ -> b e. CC )
9 8 adantl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> b e. CC )
10 simpl 
 |-  ( ( S e. CC /\ A e. ( Z[]l ` S ) ) -> S e. CC )
11 mulcl 
 |-  ( ( b e. CC /\ S e. CC ) -> ( b x. S ) e. CC )
12 9 10 11 syl2anr 
 |-  ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( b x. S ) e. CC )
13 7 12 negdid 
 |-  ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> -u ( a + ( b x. S ) ) = ( -u a + -u ( b x. S ) ) )
14 9 adantl 
 |-  ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. CC )
15 10 adantr 
 |-  ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> S e. CC )
16 14 15 mulneg1d 
 |-  ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( -u b x. S ) = -u ( b x. S ) )
17 16 eqcomd 
 |-  ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> -u ( b x. S ) = ( -u b x. S ) )
18 17 oveq2d 
 |-  ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( -u a + -u ( b x. S ) ) = ( -u a + ( -u b x. S ) ) )
19 13 18 eqtrd 
 |-  ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> -u ( a + ( b x. S ) ) = ( -u a + ( -u b x. S ) ) )
20 4 19 sylan9eqr 
 |-  ( ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ A = ( a + ( b x. S ) ) ) -> -u A = ( -u a + ( -u b x. S ) ) )
21 znegcl 
 |-  ( a e. ZZ -> -u a e. ZZ )
22 znegcl 
 |-  ( b e. ZZ -> -u b e. ZZ )
23 21 22 anim12i 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( -u a e. ZZ /\ -u b e. ZZ ) )
24 lazlinz 
 |-  ( S e. CC -> ( ( -u a e. ZZ /\ -u b e. ZZ ) -> ( -u a + ( -u b x. S ) ) e. ( Z[]l ` S ) ) )
25 24 imp 
 |-  ( ( S e. CC /\ ( -u a e. ZZ /\ -u b e. ZZ ) ) -> ( -u a + ( -u b x. S ) ) e. ( Z[]l ` S ) )
26 10 23 25 syl2an 
 |-  ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( -u a + ( -u b x. S ) ) e. ( Z[]l ` S ) )
27 26 1 eleqtrrdi 
 |-  ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( -u a + ( -u b x. S ) ) e. R )
28 27 adantr 
 |-  ( ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ A = ( a + ( b x. S ) ) ) -> ( -u a + ( -u b x. S ) ) e. R )
29 20 28 eqeltrd 
 |-  ( ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ A = ( a + ( b x. S ) ) ) -> -u A e. R )
30 29 ex 
 |-  ( ( ( S e. CC /\ A e. ( Z[]l ` S ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( A = ( a + ( b x. S ) ) -> -u A e. R ) )
31 30 rexlimdvva 
 |-  ( ( S e. CC /\ A e. ( Z[]l ` S ) ) -> ( E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) -> -u A e. R ) )
32 3 31 mpd 
 |-  ( ( S e. CC /\ A e. ( Z[]l ` S ) ) -> -u A e. R )
33 32 ex 
 |-  ( S e. CC -> ( A e. ( Z[]l ` S ) -> -u A e. R ) )
34 2 33 biimtrid 
 |-  ( S e. CC -> ( A e. R -> -u A e. R ) )